Basic

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

Statistics

Metric	Count
Definitions singularChainComplexFunctor, singularChainComplexFunctor, singularChainComplexFunctorIsoOfTotallyDisconnectedSpace, singularHomologyFunctor, singularHomologyFunctorZeroOfTotallyDisconnectedSpace	5
Theorems isZero_singularHomologyFunctor_of_totallyDisconnectedSpace, singularChainComplexFunctor_exactAt_of_totallyDisconnectedSpace	2
Total	7

AlgebraicTopology

Definitions

Name	Category	Theorems
singularChainComplexFunctor 📖	CompOp	1 math math: singularChainComplexFunctor_exactAt_of_totallyDisconnectedSpace
singularChainComplexFunctorIsoOfTotallyDisconnectedSpace 📖	CompOp	—
singularHomologyFunctor 📖	CompOp	1 math math: isZero_singularHomologyFunctor_of_totallyDisconnectedSpace
singularHomologyFunctorZeroOfTotallyDisconnectedSpace 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isZero_singularHomologyFunctor_of_totallyDisconnectedSpace 📖	mathematical	CategoryTheory.Limits.HasCoproducts	CategoryTheory.Limits.IsZero CategoryTheory.Functor.obj TopCat TopCat.instCategory CategoryTheory.Functor CategoryTheory.Functor.category singularHomologyFunctor	—	CategoryTheory.Limits.hasCoproducts_shrink CategoryTheory.Limits.IsInitial.isZero HomologicalComplex.ExactAt.isZero_homology AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.CategoryWithHomology.hasHomology singularChainComplexFunctor_exactAt_of_totallyDisconnectedSpace
singularChainComplexFunctor_exactAt_of_totallyDisconnectedSpace 📖	mathematical	CategoryTheory.Limits.HasCoproducts	HomologicalComplex.ExactAt 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 singularChainComplexFunctor	—	CategoryTheory.Limits.hasCoproducts_shrink CategoryTheory.Limits.IsInitial.isZero HomologicalComplex.ExactAt.of_iso AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.Limits.hasColimitOfHasColimitsOfShape ChainComplex.alternatingConst_exactAt

AlgebraicTopology.SSet

Definitions

Name	Category	Theorems
singularChainComplexFunctor 📖	CompOp	—

---

← Back to Index