Documentation Verification Report

ChainHomotopy

📁 Source: Mathlib/AlgebraicTopology/SimplicialObject/ChainHomotopy.lean

Statistics

Metric	Count
Definitions `hom`, `toChainHomotopy`	2
Theorems `hom_eq`, `hom_eq_zero`, `map_homology_eq`	3
Total	5

CategoryTheory.SimplicialObject.Homotopy

Definitions

Name	Category	Theorems
`toChainHomotopy` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`map_homology_eq` 📖	mathematical	—	`CategoryTheory.Functor.map` `HomologicalComplex` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `ComplexShape.down` `AddSemigroup.toAdd` `AddRightCancelSemigroup.toAddSemigroup` `AddRightCancelMonoid.toAddRightCancelSemigroup` `AddCancelMonoid.toAddRightCancelMonoid` `AddCancelCommMonoid.toAddCancelMonoid` `Nat.instAddCancelCommMonoid` `AddRightCancelSemigroup.toIsRightCancelAdd` `Nat.instOne` `HomologicalComplex.instCategory` `HomologicalComplex.homologyFunctor` `CategoryTheory.Functor.obj` `CategoryTheory.SimplicialObject` `CategoryTheory.Functor.category` `Opposite` `SimplexCategory` `CategoryTheory.Category.opposite` `SimplexCategory.smallCategory` `ChainComplex` `AlgebraicTopology.alternatingFaceMapComplex`	—	`AddRightCancelSemigroup.toIsRightCancelAdd` `Homotopy.homologyMap_eq` `CategoryTheory.CategoryWithHomology.hasHomology`

CategoryTheory.SimplicialObject.Homotopy.ToChainHomotopy

Definitions

Name	Category	Theorems
`hom` 📖	CompOp	2 math math: `hom_eq_zero`, `hom_eq`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`hom_eq` 📖	mathematical	—	`hom` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `Opposite` `SimplexCategory` `CategoryTheory.Category.opposite` `SimplexCategory.smallCategory` `Opposite.op` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `CategoryTheory.Preadditive.homGroup` `Finset.sum` `AddCommGroup.toAddCommMonoid` `Finset.univ` `Fin.fintype` `SubNegMonoid.toZSMul` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `Monoid.toPow` `Int.instMonoid` `CategoryTheory.SimplicialObject.Homotopy.h`	—	`Finset.sum_congr` `CategoryTheory.Category.comp_id`
`hom_eq_zero` 📖	mathematical	—	`hom` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `Opposite` `SimplexCategory` `CategoryTheory.Category.opposite` `SimplexCategory.smallCategory` `Opposite.op` `CategoryTheory.Limits.HasZeroMorphisms.zero` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms`	—	—

---

← Back to Index