HomotopyInvariance

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

Statistics

Metric	Count
Definitions singularChainComplexFunctorObjMap, singularChainComplexFunctorObjMap, singularChainComplexFunctor_mapHomotopy_of_simplicialHomotopy	3
Theorems congr_homologyMap_singularChainComplexFunctor, singularChainComplexFunctor_map_homology_eq_of_simplicialHomotopy, congr_homologyMap_singularChainComplexFunctor	3
Total	6

CategoryTheory.SimplicialObject.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 SSet CategoryTheory.Functor.category Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory CategoryTheory.types ChainComplex HomologicalComplex.instCategory CategoryTheory.Functor AlgebraicTopology.SSet.singularChainComplexFunctor CategoryTheory.Functor.map CategoryTheory.CategoryWithHomology.hasHomology HomologicalComplex.sc	—	Homotopy.homologyMap_eq AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.CategoryWithHomology.hasHomology
singularChainComplexFunctor_map_homology_eq_of_simplicialHomotopy 📖	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 SSet CategoryTheory.Functor.category Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory CategoryTheory.types ChainComplex HomologicalComplex.instCategory CategoryTheory.Functor AlgebraicTopology.SSet.singularChainComplexFunctor CategoryTheory.Functor.map CategoryTheory.CategoryWithHomology.hasHomology HomologicalComplex.sc	—	congr_homologyMap_singularChainComplexFunctor

SSet.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 SSet CategoryTheory.Functor.category Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory CategoryTheory.types ChainComplex HomologicalComplex.instCategory CategoryTheory.Functor AlgebraicTopology.SSet.singularChainComplexFunctor CategoryTheory.Functor.map CategoryTheory.CategoryWithHomology.hasHomology HomologicalComplex.sc	—	Homotopy.homologyMap_eq AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.CategoryWithHomology.hasHomology

(root)

Definitions

Name	Category	Theorems
singularChainComplexFunctor_mapHomotopy_of_simplicialHomotopy 📖	CompOp	—

---

← Back to Index