Documentation Verification Report

MooreComplex

📁 Source: Mathlib/AlgebraicTopology/MooreComplex.lean

Statistics

Metric	Count
Definitions `map`, `obj`, `objD`, `objX`, `normalizedMooreComplex`	5
Theorems `d_squared`, `map_f`, `objX_add_one`, `objX_zero`, `obj_X`, `obj_d`, `normalizedMooreComplex_map`, `normalizedMooreComplex_obj`, `normalizedMooreComplex_objD`	9
Total	14

AlgebraicTopology

Definitions

Name	Category	Theorems
`normalizedMooreComplex` 📖	CompOp	15 math math: `DoldKan.HigherFacesVanish.inclusionOfMooreComplexMap`, `DoldKan.homotopyEquivNormalizedMooreComplexAlternatingFaceMapComplex_inv`, `DoldKan.homotopyEquivNormalizedMooreComplexAlternatingFaceMapComplex_homotopyHomInvId`, `DoldKan.inclusionOfMooreComplexMap_comp_PInfty_assoc`, `inclusionOfMooreComplex_app`, `DoldKan.inclusionOfMooreComplexMap_comp_PInfty`, `normalizedMooreComplex_objD`, `normalizedMooreComplex_map`, `DoldKan.instMonoChainComplexNatInclusionOfMooreComplexMap`, `DoldKan.homotopyEquivNormalizedMooreComplexAlternatingFaceMapComplex_homotopyInvHomId`, `CategoryTheory.Abelian.DoldKan.comparisonN_hom_app_f`, `inclusionOfMooreComplexMap_f`, `DoldKan.homotopyEquivNormalizedMooreComplexAlternatingFaceMapComplex_hom`, `CategoryTheory.Abelian.DoldKan.comparisonN_inv_app_f`, `normalizedMooreComplex_obj`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`normalizedMooreComplex_map` 📖	mathematical	—	`CategoryTheory.Functor.map` `CategoryTheory.SimplicialObject` `CategoryTheory.instCategorySimplicialObject` `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` `normalizedMooreComplex` `NormalizedMooreComplex.map`	—	`AddRightCancelSemigroup.toIsRightCancelAdd`
`normalizedMooreComplex_obj` 📖	mathematical	—	`CategoryTheory.Functor.obj` `CategoryTheory.SimplicialObject` `CategoryTheory.instCategorySimplicialObject` `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` `normalizedMooreComplex` `NormalizedMooreComplex.obj`	—	`AddRightCancelSemigroup.toIsRightCancelAdd`
`normalizedMooreComplex_objD` 📖	mathematical	—	`HomologicalComplex.d` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive` `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` `normalizedMooreComplex` `NormalizedMooreComplex.objD`	—	`ChainComplex.of_d` `NormalizedMooreComplex.d_squared`

AlgebraicTopology.NormalizedMooreComplex

Definitions

Name	Category	Theorems
`map` 📖	CompOp	4 math math: `AlgebraicTopology.normalizedMooreComplex_map`, `AlgebraicTopology.DoldKan.PInftyToNormalizedMooreComplex_naturality_assoc`, `map_f`, `AlgebraicTopology.DoldKan.PInftyToNormalizedMooreComplex_naturality`
`obj` 📖	CompOp	13 math math: `AlgebraicTopology.DoldKan.PInfty_comp_PInftyToNormalizedMooreComplex`, `obj_d`, `AlgebraicTopology.DoldKan.PInftyToNormalizedMooreComplex_f`, `AlgebraicTopology.DoldKan.PInftyToNormalizedMooreComplex_comp_inclusionOfMooreComplexMap`, `AlgebraicTopology.DoldKan.PInftyToNormalizedMooreComplex_naturality_assoc`, `map_f`, `obj_X`, `AlgebraicTopology.DoldKan.PInftyToNormalizedMooreComplex_comp_inclusionOfMooreComplexMap_assoc`, `AlgebraicTopology.DoldKan.PInftyToNormalizedMooreComplex_naturality`, `CategoryTheory.Abelian.DoldKan.comparisonN_hom_app_f`, `AlgebraicTopology.DoldKan.PInfty_comp_PInftyToNormalizedMooreComplex_assoc`, `CategoryTheory.Abelian.DoldKan.comparisonN_inv_app_f`, `AlgebraicTopology.normalizedMooreComplex_obj`
`objD` 📖	CompOp	2 math math: `AlgebraicTopology.normalizedMooreComplex_objD`, `d_squared`
`objX` 📖	CompOp	9 math math: `obj_d`, `AlgebraicTopology.DoldKan.PInftyToNormalizedMooreComplex_f`, `d_squared`, `map_f`, `obj_X`, `objX_add_one`, `objX_zero`, `AlgebraicTopology.inclusionOfMooreComplexMap_f`, `AlgebraicTopology.DoldKan.factors_normalizedMooreComplex_PInfty`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`d_squared` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `CategoryTheory.Subobject` `Opposite` `SimplexCategory` `CategoryTheory.Category.opposite` `SimplexCategory.smallCategory` `Opposite.op` `Preorder.smallCategory` `PartialOrder.toPreorder` `CategoryTheory.instPartialOrderSubobject` `CategoryTheory.Subobject.underlying` `objX` `objD` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Limits.HasZeroMorphisms.zero` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive`	—	`CategoryTheory.Abelian.hasPullbacks` `CategoryTheory.Limits.HasKernels.has_limit` `CategoryTheory.Abelian.has_kernels` `CategoryTheory.Subobject.factorThru_arrow_assoc` `CategoryTheory.Category.assoc` `CategoryTheory.SimplicialObject.δ_comp_δ_assoc` `CategoryTheory.Subobject.finset_inf_arrow_factors` `CategoryTheory.Subobject.factorThru_arrow` `CategoryTheory.Limits.kernelSubobject_arrow_comp_assoc` `CategoryTheory.Limits.zero_comp` `CategoryTheory.Limits.comp_zero` `CategoryTheory.Subobject.factors_of_factors_right` `CategoryTheory.Subobject.factorThru_right` `CategoryTheory.Subobject.factorThru_eq_zero` `CategoryTheory.SimplicialObject.δ_comp_δ`
`map_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` `obj` `map` `CategoryTheory.Subobject.factorThru` `CategoryTheory.Functor.obj` `CategoryTheory.Subobject` `Opposite` `SimplexCategory` `CategoryTheory.Category.opposite` `SimplexCategory.smallCategory` `Opposite.op` `Preorder.smallCategory` `PartialOrder.toPreorder` `CategoryTheory.instPartialOrderSubobject` `CategoryTheory.Subobject.underlying` `objX` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Subobject.arrow` `CategoryTheory.NatTrans.app`	—	`AddRightCancelSemigroup.toIsRightCancelAdd`
`objX_add_one` 📖	mathematical	—	`objX` `Finset.inf` `CategoryTheory.Subobject` `CategoryTheory.Functor.obj` `Opposite` `SimplexCategory` `CategoryTheory.Category.opposite` `SimplexCategory.smallCategory` `Opposite.op` `CategoryTheory.Subobject.semilatticeInf` `CategoryTheory.Abelian.hasPullbacks` `CategoryTheory.Subobject.orderTop` `Finset.univ` `Fin.fintype` `CategoryTheory.Limits.kernelSubobject` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive` `CategoryTheory.SimplicialObject.δ` `CategoryTheory.Limits.HasKernels.has_limit` `CategoryTheory.Abelian.has_kernels`	—	—
`objX_zero` 📖	mathematical	—	`objX` `Top.top` `CategoryTheory.Subobject` `CategoryTheory.Functor.obj` `Opposite` `SimplexCategory` `CategoryTheory.Category.opposite` `SimplexCategory.smallCategory` `Opposite.op` `OrderTop.toTop` `Preorder.toLE` `PartialOrder.toPreorder` `CategoryTheory.instPartialOrderSubobject` `CategoryTheory.Subobject.orderTop`	—	—
`obj_X` 📖	mathematical	—	`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` `obj` `CategoryTheory.Functor.obj` `CategoryTheory.Subobject` `Opposite` `SimplexCategory` `CategoryTheory.Category.opposite` `SimplexCategory.smallCategory` `Opposite.op` `Preorder.smallCategory` `PartialOrder.toPreorder` `CategoryTheory.instPartialOrderSubobject` `CategoryTheory.Subobject.underlying` `objX`	—	`AddRightCancelSemigroup.toIsRightCancelAdd`
`obj_d` 📖	mathematical	—	`HomologicalComplex.d` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive` `ComplexShape.down` `AddSemigroup.toAdd` `AddRightCancelSemigroup.toAddSemigroup` `AddRightCancelMonoid.toAddRightCancelSemigroup` `AddCancelMonoid.toAddRightCancelMonoid` `AddCancelCommMonoid.toAddCancelMonoid` `Nat.instAddCancelCommMonoid` `AddRightCancelSemigroup.toIsRightCancelAdd` `Nat.instOne` `obj` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `CategoryTheory.Subobject` `Opposite` `SimplexCategory` `CategoryTheory.Category.opposite` `SimplexCategory.smallCategory` `Opposite.op` `Preorder.smallCategory` `PartialOrder.toPreorder` `CategoryTheory.instPartialOrderSubobject` `CategoryTheory.Subobject.underlying` `objX` `CategoryTheory.CategoryStruct.comp` `Finset.inf` `CategoryTheory.Subobject.semilatticeInf` `CategoryTheory.Abelian.hasPullbacks` `CategoryTheory.Subobject.orderTop` `Finset.univ` `Fin.fintype` `CategoryTheory.Limits.kernelSubobject` `CategoryTheory.SimplicialObject.δ` `CategoryTheory.Limits.HasKernels.has_limit` `CategoryTheory.Abelian.has_kernels` `CategoryTheory.eqToHom` `Top.top` `OrderTop.toTop` `Preorder.toLE` `CategoryTheory.Subobject.arrow` `CategoryTheory.inv` `CategoryTheory.Subobject.factorThru` `CategoryTheory.Limits.HasZeroMorphisms.zero`	—	`AddRightCancelSemigroup.toIsRightCancelAdd`

---

← Back to Index