Documentation Verification Report

Normalized

📁 Source: Mathlib/AlgebraicTopology/DoldKan/Normalized.lean

Statistics

Metric	Count
Definitions `N₁_iso_normalizedMooreComplex_comp_toKaroubi`, `PInftyToNormalizedMooreComplex`, `splitMonoInclusionOfMooreComplexMap`	3
Theorems `inclusionOfMooreComplexMap`, `PInftyToNormalizedMooreComplex_comp_inclusionOfMooreComplexMap`, `PInftyToNormalizedMooreComplex_comp_inclusionOfMooreComplexMap_assoc`, `PInftyToNormalizedMooreComplex_f`, `PInftyToNormalizedMooreComplex_naturality`, `PInftyToNormalizedMooreComplex_naturality_assoc`, `PInfty_comp_PInftyToNormalizedMooreComplex`, `PInfty_comp_PInftyToNormalizedMooreComplex_assoc`, `factors_normalizedMooreComplex_PInfty`, `inclusionOfMooreComplexMap_comp_PInfty`, `inclusionOfMooreComplexMap_comp_PInfty_assoc`, `instMonoChainComplexNatInclusionOfMooreComplexMap`	12
Total	15

AlgebraicTopology.DoldKan

Definitions

Name	Category	Theorems
`N₁_iso_normalizedMooreComplex_comp_toKaroubi` 📖	CompOp	2 math math: `CategoryTheory.Abelian.DoldKan.comparisonN_hom_app_f`, `CategoryTheory.Abelian.DoldKan.comparisonN_inv_app_f`
`PInftyToNormalizedMooreComplex` 📖	CompOp	10 math math: `PInfty_comp_PInftyToNormalizedMooreComplex`, `homotopyEquivNormalizedMooreComplexAlternatingFaceMapComplex_inv`, `PInftyToNormalizedMooreComplex_f`, `homotopyEquivNormalizedMooreComplexAlternatingFaceMapComplex_homotopyHomInvId`, `PInftyToNormalizedMooreComplex_comp_inclusionOfMooreComplexMap`, `PInftyToNormalizedMooreComplex_naturality_assoc`, `homotopyEquivNormalizedMooreComplexAlternatingFaceMapComplex_homotopyInvHomId`, `PInftyToNormalizedMooreComplex_comp_inclusionOfMooreComplexMap_assoc`, `PInftyToNormalizedMooreComplex_naturality`, `PInfty_comp_PInftyToNormalizedMooreComplex_assoc`
`splitMonoInclusionOfMooreComplexMap` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`PInftyToNormalizedMooreComplex_comp_inclusionOfMooreComplexMap` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `ChainComplex` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive` `AddRightCancelMonoid.toAddRightCancelSemigroup` `AddCancelMonoid.toAddRightCancelMonoid` `AddCancelCommMonoid.toAddCancelMonoid` `Nat.instAddCancelCommMonoid` `Nat.instOne` `CategoryTheory.Category.toCategoryStruct` `HomologicalComplex.instCategory` `ComplexShape.down` `AddSemigroup.toAdd` `AddRightCancelSemigroup.toAddSemigroup` `AddRightCancelSemigroup.toIsRightCancelAdd` `AlgebraicTopology.AlternatingFaceMapComplex.obj` `AlgebraicTopology.NormalizedMooreComplex.obj` `CategoryTheory.Functor.obj` `CategoryTheory.SimplicialObject` `CategoryTheory.instCategorySimplicialObject` `AlgebraicTopology.alternatingFaceMapComplex` `PInftyToNormalizedMooreComplex` `AlgebraicTopology.inclusionOfMooreComplexMap` `PInfty`	—	`HomologicalComplex.hom_ext` `AddRightCancelSemigroup.toIsRightCancelAdd` `factors_normalizedMooreComplex_PInfty` `AlgebraicTopology.inclusionOfMooreComplexMap_f` `CategoryTheory.Subobject.factorThru_arrow`
`PInftyToNormalizedMooreComplex_comp_inclusionOfMooreComplexMap_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `ChainComplex` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive` `AddRightCancelMonoid.toAddRightCancelSemigroup` `AddCancelMonoid.toAddRightCancelMonoid` `AddCancelCommMonoid.toAddCancelMonoid` `Nat.instAddCancelCommMonoid` `Nat.instOne` `CategoryTheory.Category.toCategoryStruct` `HomologicalComplex.instCategory` `ComplexShape.down` `AddSemigroup.toAdd` `AddRightCancelSemigroup.toAddSemigroup` `AddRightCancelSemigroup.toIsRightCancelAdd` `AlgebraicTopology.AlternatingFaceMapComplex.obj` `AlgebraicTopology.NormalizedMooreComplex.obj` `PInftyToNormalizedMooreComplex` `CategoryTheory.Functor.obj` `CategoryTheory.SimplicialObject` `CategoryTheory.instCategorySimplicialObject` `AlgebraicTopology.alternatingFaceMapComplex` `AlgebraicTopology.inclusionOfMooreComplexMap` `PInfty`	—	`AddRightCancelSemigroup.toIsRightCancelAdd` `CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `PInftyToNormalizedMooreComplex_comp_inclusionOfMooreComplexMap`
`PInftyToNormalizedMooreComplex_f` 📖	mathematical	—	`HomologicalComplex.Hom.f` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive` `ComplexShape.down` `AddSemigroup.toAdd` `AddRightCancelSemigroup.toAddSemigroup` `AddRightCancelMonoid.toAddRightCancelSemigroup` `AddCancelMonoid.toAddRightCancelMonoid` `AddCancelCommMonoid.toAddCancelMonoid` `Nat.instAddCancelCommMonoid` `AddRightCancelSemigroup.toIsRightCancelAdd` `Nat.instOne` `AlgebraicTopology.AlternatingFaceMapComplex.obj` `AlgebraicTopology.NormalizedMooreComplex.obj` `PInftyToNormalizedMooreComplex` `CategoryTheory.Subobject.factorThru` `CategoryTheory.Functor.obj` `Opposite` `SimplexCategory` `CategoryTheory.Category.opposite` `SimplexCategory.smallCategory` `Opposite.op` `AlgebraicTopology.NormalizedMooreComplex.objX` `PInfty` `factors_normalizedMooreComplex_PInfty`	—	`AddRightCancelSemigroup.toIsRightCancelAdd`
`PInftyToNormalizedMooreComplex_naturality` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `ChainComplex` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive` `AddRightCancelMonoid.toAddRightCancelSemigroup` `AddCancelMonoid.toAddRightCancelMonoid` `AddCancelCommMonoid.toAddCancelMonoid` `Nat.instAddCancelCommMonoid` `Nat.instOne` `CategoryTheory.Category.toCategoryStruct` `HomologicalComplex.instCategory` `ComplexShape.down` `AddSemigroup.toAdd` `AddRightCancelSemigroup.toAddSemigroup` `AddRightCancelSemigroup.toIsRightCancelAdd` `AlgebraicTopology.AlternatingFaceMapComplex.obj` `AlgebraicTopology.NormalizedMooreComplex.obj` `AlgebraicTopology.AlternatingFaceMapComplex.map` `PInftyToNormalizedMooreComplex` `AlgebraicTopology.NormalizedMooreComplex.map`	—	`HomologicalComplex.hom_ext` `AddRightCancelSemigroup.toIsRightCancelAdd` `CategoryTheory.Subobject.eq_of_comp_arrow_eq` `factors_normalizedMooreComplex_PInfty` `CategoryTheory.Category.assoc` `CategoryTheory.Subobject.factorThru_arrow` `PInfty_f_naturality` `CategoryTheory.Subobject.factorThru_arrow_assoc`
`PInftyToNormalizedMooreComplex_naturality_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `ChainComplex` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive` `AddRightCancelMonoid.toAddRightCancelSemigroup` `AddCancelMonoid.toAddRightCancelMonoid` `AddCancelCommMonoid.toAddCancelMonoid` `Nat.instAddCancelCommMonoid` `Nat.instOne` `CategoryTheory.Category.toCategoryStruct` `HomologicalComplex.instCategory` `ComplexShape.down` `AddSemigroup.toAdd` `AddRightCancelSemigroup.toAddSemigroup` `AddRightCancelSemigroup.toIsRightCancelAdd` `AlgebraicTopology.AlternatingFaceMapComplex.obj` `AlgebraicTopology.AlternatingFaceMapComplex.map` `AlgebraicTopology.NormalizedMooreComplex.obj` `PInftyToNormalizedMooreComplex` `AlgebraicTopology.NormalizedMooreComplex.map`	—	`AddRightCancelSemigroup.toIsRightCancelAdd` `CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `PInftyToNormalizedMooreComplex_naturality`
`PInfty_comp_PInftyToNormalizedMooreComplex` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `ChainComplex` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive` `AddRightCancelMonoid.toAddRightCancelSemigroup` `AddCancelMonoid.toAddRightCancelMonoid` `AddCancelCommMonoid.toAddCancelMonoid` `Nat.instAddCancelCommMonoid` `Nat.instOne` `CategoryTheory.Category.toCategoryStruct` `HomologicalComplex.instCategory` `ComplexShape.down` `AddSemigroup.toAdd` `AddRightCancelSemigroup.toAddSemigroup` `AddRightCancelSemigroup.toIsRightCancelAdd` `AlgebraicTopology.AlternatingFaceMapComplex.obj` `AlgebraicTopology.NormalizedMooreComplex.obj` `PInfty` `PInftyToNormalizedMooreComplex`	—	`HomologicalComplex.hom_ext` `AddRightCancelSemigroup.toIsRightCancelAdd` `CategoryTheory.Subobject.eq_of_comp_arrow_eq` `factors_normalizedMooreComplex_PInfty` `CategoryTheory.Category.assoc` `CategoryTheory.Subobject.factorThru_arrow` `PInfty_f_idem`
`PInfty_comp_PInftyToNormalizedMooreComplex_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `ChainComplex` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive` `AddRightCancelMonoid.toAddRightCancelSemigroup` `AddCancelMonoid.toAddRightCancelMonoid` `AddCancelCommMonoid.toAddCancelMonoid` `Nat.instAddCancelCommMonoid` `Nat.instOne` `CategoryTheory.Category.toCategoryStruct` `HomologicalComplex.instCategory` `ComplexShape.down` `AddSemigroup.toAdd` `AddRightCancelSemigroup.toAddSemigroup` `AddRightCancelSemigroup.toIsRightCancelAdd` `AlgebraicTopology.AlternatingFaceMapComplex.obj` `PInfty` `AlgebraicTopology.NormalizedMooreComplex.obj` `PInftyToNormalizedMooreComplex`	—	`AddRightCancelSemigroup.toIsRightCancelAdd` `CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `PInfty_comp_PInftyToNormalizedMooreComplex`
`factors_normalizedMooreComplex_PInfty` 📖	mathematical	—	`CategoryTheory.Subobject.Factors` `HomologicalComplex.X` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive` `ComplexShape.down` `AddSemigroup.toAdd` `AddRightCancelSemigroup.toAddSemigroup` `AddRightCancelMonoid.toAddRightCancelSemigroup` `AddCancelMonoid.toAddRightCancelMonoid` `AddCancelCommMonoid.toAddCancelMonoid` `Nat.instAddCancelCommMonoid` `AddRightCancelSemigroup.toIsRightCancelAdd` `Nat.instOne` `AlgebraicTopology.AlternatingFaceMapComplex.obj` `CategoryTheory.Functor.obj` `Opposite` `SimplexCategory` `CategoryTheory.Category.opposite` `SimplexCategory.smallCategory` `Opposite.op` `AlgebraicTopology.NormalizedMooreComplex.objX` `HomologicalComplex.Hom.f` `PInfty`	—	`AddRightCancelSemigroup.toIsRightCancelAdd` `CategoryTheory.Subobject.top_factors` `PInfty_f` `CategoryTheory.Abelian.hasPullbacks` `AlgebraicTopology.NormalizedMooreComplex.objX.eq_2` `CategoryTheory.Subobject.finset_inf_factors` `CategoryTheory.Limits.kernelSubobject_factors` `HigherFacesVanish.of_P` `le_add_self` `Nat.instCanonicallyOrderedAdd`
`inclusionOfMooreComplexMap_comp_PInfty` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `ChainComplex` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive` `AddRightCancelMonoid.toAddRightCancelSemigroup` `AddCancelMonoid.toAddRightCancelMonoid` `AddCancelCommMonoid.toAddCancelMonoid` `Nat.instAddCancelCommMonoid` `Nat.instOne` `CategoryTheory.Category.toCategoryStruct` `HomologicalComplex.instCategory` `ComplexShape.down` `AddSemigroup.toAdd` `AddRightCancelSemigroup.toAddSemigroup` `AddRightCancelSemigroup.toIsRightCancelAdd` `CategoryTheory.Functor.obj` `CategoryTheory.SimplicialObject` `CategoryTheory.instCategorySimplicialObject` `AlgebraicTopology.normalizedMooreComplex` `AlgebraicTopology.alternatingFaceMapComplex` `AlgebraicTopology.AlternatingFaceMapComplex.obj` `AlgebraicTopology.inclusionOfMooreComplexMap` `PInfty`	—	`HomologicalComplex.hom_ext` `AddRightCancelSemigroup.toIsRightCancelAdd` `CategoryTheory.Category.comp_id` `HigherFacesVanish.comp_P_eq_self` `HigherFacesVanish.inclusionOfMooreComplexMap`
`inclusionOfMooreComplexMap_comp_PInfty_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `ChainComplex` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive` `AddRightCancelMonoid.toAddRightCancelSemigroup` `AddCancelMonoid.toAddRightCancelMonoid` `AddCancelCommMonoid.toAddCancelMonoid` `Nat.instAddCancelCommMonoid` `Nat.instOne` `CategoryTheory.Category.toCategoryStruct` `HomologicalComplex.instCategory` `ComplexShape.down` `AddSemigroup.toAdd` `AddRightCancelSemigroup.toAddSemigroup` `AddRightCancelSemigroup.toIsRightCancelAdd` `CategoryTheory.Functor.obj` `CategoryTheory.SimplicialObject` `CategoryTheory.instCategorySimplicialObject` `AlgebraicTopology.normalizedMooreComplex` `AlgebraicTopology.alternatingFaceMapComplex` `AlgebraicTopology.inclusionOfMooreComplexMap` `AlgebraicTopology.AlternatingFaceMapComplex.obj` `PInfty`	—	`AddRightCancelSemigroup.toIsRightCancelAdd` `CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `inclusionOfMooreComplexMap_comp_PInfty`
`instMonoChainComplexNatInclusionOfMooreComplexMap` 📖	mathematical	—	`CategoryTheory.Mono` `ChainComplex` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive` `AddRightCancelMonoid.toAddRightCancelSemigroup` `AddCancelMonoid.toAddRightCancelMonoid` `AddCancelCommMonoid.toAddCancelMonoid` `Nat.instAddCancelCommMonoid` `Nat.instOne` `HomologicalComplex.instCategory` `ComplexShape.down` `AddSemigroup.toAdd` `AddRightCancelSemigroup.toAddSemigroup` `AddRightCancelSemigroup.toIsRightCancelAdd` `CategoryTheory.Functor.obj` `CategoryTheory.SimplicialObject` `CategoryTheory.instCategorySimplicialObject` `AlgebraicTopology.normalizedMooreComplex` `AlgebraicTopology.alternatingFaceMapComplex` `AlgebraicTopology.inclusionOfMooreComplexMap`	—	`AddRightCancelSemigroup.toIsRightCancelAdd` `HomologicalComplex.hom_ext` `CategoryTheory.Subobject.eq_of_comp_arrow_eq` `HomologicalComplex.congr_hom`

AlgebraicTopology.DoldKan.HigherFacesVanish

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`inclusionOfMooreComplexMap` 📖	mathematical	—	`AlgebraicTopology.DoldKan.HigherFacesVanish` `CategoryTheory.Abelian.toPreadditive` `HomologicalComplex.X` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `ComplexShape.down` `AddSemigroup.toAdd` `AddRightCancelSemigroup.toAddSemigroup` `AddRightCancelMonoid.toAddRightCancelSemigroup` `AddCancelMonoid.toAddRightCancelMonoid` `AddCancelCommMonoid.toAddCancelMonoid` `Nat.instAddCancelCommMonoid` `AddRightCancelSemigroup.toIsRightCancelAdd` `Nat.instOne` `CategoryTheory.Functor.obj` `CategoryTheory.SimplicialObject` `CategoryTheory.instCategorySimplicialObject` `ChainComplex` `HomologicalComplex.instCategory` `AlgebraicTopology.normalizedMooreComplex` `HomologicalComplex.Hom.f` `AlgebraicTopology.alternatingFaceMapComplex` `AlgebraicTopology.inclusionOfMooreComplexMap`	—	`AddRightCancelSemigroup.toIsRightCancelAdd` `CategoryTheory.Abelian.hasPullbacks` `CategoryTheory.Limits.HasKernels.has_limit` `CategoryTheory.Abelian.has_kernels` `CategoryTheory.Subobject.finset_inf_arrow_factors` `CategoryTheory.Subobject.factorThru_arrow` `CategoryTheory.Category.assoc` `CategoryTheory.Limits.kernelSubobject_arrow_comp` `CategoryTheory.Limits.comp_zero`

---

← Back to Index