Documentation Verification Report

Homotopies

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

Statistics

Metric	Count
Definitions `Hσ`, `c`, `homotopyHσToZero`, `hσ`, `hσ'`, `natTransHσ`	6
Theorems `Hσ_eq_zero`, `c_mk`, `cs_down_0_not_rel_left`, `hσ'_eq`, `hσ'_eq'`, `hσ'_eq_zero`, `hσ'_naturality`, `map_Hσ`, `map_hσ'`	9
Total	15

AlgebraicTopology.DoldKan

Definitions

Name	Category	Theorems
`Hσ` 📖	CompOp	7 math math: `map_Hσ`, `HigherFacesVanish.comp_Hσ_eq_zero`, `P_succ`, `Hσ_eq_zero`, `Q_succ`, `HigherFacesVanish.comp_Hσ_eq`, `HigherFacesVanish.induction`
`c` 📖	CompOp	2 math math: `cs_down_0_not_rel_left`, `c_mk`
`homotopyHσToZero` 📖	CompOp	—
`hσ` 📖	CompOp	—
`hσ'` 📖	CompOp	5 math math: `hσ'_eq`, `hσ'_eq_zero`, `map_hσ'`, `hσ'_naturality`, `hσ'_eq'`
`natTransHσ` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`Hσ_eq_zero` 📖	mathematical	—	`HomologicalComplex.Hom.f` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `ComplexShape.down` `AddSemigroup.toAdd` `AddRightCancelSemigroup.toAddSemigroup` `AddRightCancelMonoid.toAddRightCancelSemigroup` `AddCancelMonoid.toAddRightCancelMonoid` `AddCancelCommMonoid.toAddCancelMonoid` `Nat.instAddCancelCommMonoid` `AddRightCancelSemigroup.toIsRightCancelAdd` `Nat.instOne` `AlgebraicTopology.AlternatingFaceMapComplex.obj` `Hσ` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `HomologicalComplex.X` `CategoryTheory.Limits.HasZeroMorphisms.zero`	—	`AddRightCancelSemigroup.toIsRightCancelAdd` `Homotopy.nullHomotopicMap'_f_of_not_rel_left` `cs_down_0_not_rel_left` `hσ'_eq` `pow_zero` `one_zsmul` `CategoryTheory.Category.comp_id` `AlgebraicTopology.AlternatingFaceMapComplex.d_squared` `ChainComplex.of_d` `AlgebraicTopology.AlternatingFaceMapComplex.objD.eq_1` `Fin.sum_univ_two` `pow_one` `one_smul` `neg_smul` `CategoryTheory.Preadditive.comp_add` `CategoryTheory.Preadditive.comp_neg` `add_neg_eq_zero` `CategoryTheory.SimplicialObject.δ_comp_σ_succ` `CategoryTheory.SimplicialObject.δ_comp_σ_self'` `Fin.castSucc_zero'` `hσ'_eq_zero` `CategoryTheory.Limits.zero_comp`
`c_mk` 📖	mathematical	—	`ComplexShape.Rel` `c`	—	`AddRightCancelSemigroup.toIsRightCancelAdd`
`cs_down_0_not_rel_left` 📖	mathematical	—	`ComplexShape.Rel` `c`	—	`le_refl`
`hσ'_eq` 📖	mathematical	`ComplexShape.Rel` `c`	`hσ'` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `Opposite` `SimplexCategory` `CategoryTheory.Category.opposite` `SimplexCategory.smallCategory` `Opposite.op` `HomologicalComplex.X` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `ComplexShape.down` `AddSemigroup.toAdd` `AddRightCancelSemigroup.toAddSemigroup` `AddRightCancelMonoid.toAddRightCancelSemigroup` `AddCancelMonoid.toAddRightCancelMonoid` `AddCancelCommMonoid.toAddCancelMonoid` `Nat.instAddCancelCommMonoid` `AddRightCancelSemigroup.toIsRightCancelAdd` `Nat.instOne` `AlgebraicTopology.AlternatingFaceMapComplex.obj` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `SubNegMonoid.toZSMul` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `CategoryTheory.Preadditive.homGroup` `Monoid.toNatPow` `Int.instMonoid` `CategoryTheory.SimplicialObject.σ` `CategoryTheory.eqToHom`	—	—
`hσ'_eq'` 📖	mathematical	—	`hσ'` `Nat.instOne` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `Opposite` `SimplexCategory` `CategoryTheory.Category.opposite` `SimplexCategory.smallCategory` `Opposite.op` `SubNegMonoid.toZSMul` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `CategoryTheory.Preadditive.homGroup` `Monoid.toNatPow` `Int.instMonoid` `CategoryTheory.SimplicialObject.σ`	—	`AddRightCancelSemigroup.toIsRightCancelAdd` `hσ'_eq` `CategoryTheory.eqToHom_refl` `CategoryTheory.Category.comp_id`
`hσ'_eq_zero` 📖	mathematical	`ComplexShape.Rel` `c`	`hσ'` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `HomologicalComplex.X` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `ComplexShape.down` `AddSemigroup.toAdd` `AddRightCancelSemigroup.toAddSemigroup` `AddRightCancelMonoid.toAddRightCancelSemigroup` `AddCancelMonoid.toAddRightCancelMonoid` `AddCancelCommMonoid.toAddCancelMonoid` `Nat.instAddCancelCommMonoid` `AddRightCancelSemigroup.toIsRightCancelAdd` `Nat.instOne` `AlgebraicTopology.AlternatingFaceMapComplex.obj` `CategoryTheory.Limits.HasZeroMorphisms.zero`	—	`AddRightCancelSemigroup.toIsRightCancelAdd` `CategoryTheory.Limits.zero_comp`
`hσ'_naturality` 📖	mathematical	`ComplexShape.Rel` `c`	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `Opposite` `SimplexCategory` `CategoryTheory.Category.opposite` `SimplexCategory.smallCategory` `Opposite.op` `HomologicalComplex.X` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `ComplexShape.down` `AddSemigroup.toAdd` `AddRightCancelSemigroup.toAddSemigroup` `AddRightCancelMonoid.toAddRightCancelSemigroup` `AddCancelMonoid.toAddRightCancelMonoid` `AddCancelCommMonoid.toAddCancelMonoid` `Nat.instAddCancelCommMonoid` `AddRightCancelSemigroup.toIsRightCancelAdd` `Nat.instOne` `AlgebraicTopology.AlternatingFaceMapComplex.obj` `CategoryTheory.NatTrans.app` `hσ'`	—	`AddRightCancelSemigroup.toIsRightCancelAdd` `CategoryTheory.Category.comp_id` `CategoryTheory.Limits.zero_comp` `CategoryTheory.Limits.comp_zero` `CategoryTheory.Linear.comp_smul` `CategoryTheory.Linear.smul_comp` `CategoryTheory.SimplicialObject.σ_naturality`
`map_Hσ` 📖	mathematical	—	`HomologicalComplex.Hom.f` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `ComplexShape.down` `AddSemigroup.toAdd` `AddRightCancelSemigroup.toAddSemigroup` `AddRightCancelMonoid.toAddRightCancelSemigroup` `AddCancelMonoid.toAddRightCancelMonoid` `AddCancelCommMonoid.toAddCancelMonoid` `Nat.instAddCancelCommMonoid` `AddRightCancelSemigroup.toIsRightCancelAdd` `Nat.instOne` `AlgebraicTopology.AlternatingFaceMapComplex.obj` `CategoryTheory.Functor.obj` `CategoryTheory.SimplicialObject` `CategoryTheory.instCategorySimplicialObject` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.SimplicialObject.whiskering` `Hσ` `CategoryTheory.Functor.map` `HomologicalComplex.X`	—	`AddRightCancelSemigroup.toIsRightCancelAdd` `CategoryTheory.Functor.preservesZeroMorphisms_of_additive` `HomologicalComplex.congr_hom` `Homotopy.map_nullHomotopicMap'` `CategoryTheory.Functor.congr_obj` `AlgebraicTopology.map_alternatingFaceMapComplex`
`map_hσ'` 📖	mathematical	`ComplexShape.Rel` `c`	`hσ'` `CategoryTheory.Functor.obj` `CategoryTheory.SimplicialObject` `CategoryTheory.instCategorySimplicialObject` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.SimplicialObject.whiskering` `CategoryTheory.Functor.map` `HomologicalComplex.X` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `ComplexShape.down` `AddSemigroup.toAdd` `AddRightCancelSemigroup.toAddSemigroup` `AddRightCancelMonoid.toAddRightCancelSemigroup` `AddCancelMonoid.toAddRightCancelMonoid` `AddCancelCommMonoid.toAddCancelMonoid` `Nat.instAddCancelCommMonoid` `AddRightCancelSemigroup.toIsRightCancelAdd` `Nat.instOne` `AlgebraicTopology.AlternatingFaceMapComplex.obj`	—	`AddRightCancelSemigroup.toIsRightCancelAdd` `CategoryTheory.Limits.zero_comp` `CategoryTheory.Functor.map_zero` `CategoryTheory.Functor.preservesZeroMorphisms_of_additive` `CategoryTheory.Functor.map_comp` `CategoryTheory.Functor.map_zsmul` `CategoryTheory.eqToHom_map`

---

← Back to Index