HomotopyInvarianceTopCat

📁 Source: Mathlib/AlgebraicTopology/SingularHomology/HomotopyInvarianceTopCat.lean

Statistics

Metric	Count
Definitions singularChainComplexFunctorObjMap	1
Theorems congr_homologyMap_singularChainComplexFunctor	1
Total	2

TopCat.Homotopy

Definitions

Name	Category	Theorems
singularChainComplexFunctorObjMap 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
congr_homologyMap_singularChainComplexFunctor 📖	mathematical	CategoryTheory.Limits.HasCoproducts	HomologicalComplex.homologyMap CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ComplexShape.down AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid AddRightCancelSemigroup.toIsRightCancelAdd Nat.instOne CategoryTheory.Functor.obj TopCat TopCat.instCategory ChainComplex HomologicalComplex.instCategory CategoryTheory.Functor CategoryTheory.Functor.category AlgebraicTopology.singularChainComplexFunctor CategoryTheory.Functor.map CategoryTheory.CategoryWithHomology.hasHomology HomologicalComplex.sc	—	Homotopy.homologyMap_eq AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.CategoryWithHomology.hasHomology

---

← Back to Index