Commit 2025-02-09 17:02 c1d47161

View on Github →

feat(AlgebraicTopology): singular homology (#21559) The definition is provided by Oliver Nash, Adam Topaz, and Kevin Buzzard on Zulip.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/Homology/AlternatingConst.lean

added theorem ChainComplex.alternatingConst_exactAt

deleted theorem ChainComplex.isZero_alternatingConst_homology

Created Mathlib/AlgebraicTopology/SingularHomology/Basic.lean

added def AlgebraicTopology.SSet.singularChainComplexFunctor

added theorem AlgebraicTopology.isZero_singularHomologyFunctor_of_totallyDisconnectedSpace

added def AlgebraicTopology.singularChainComplexFunctor

added def AlgebraicTopology.singularChainComplexFunctorIsoOfTotallyDisconnectedSpace

added theorem AlgebraicTopology.singularChainComplexFunctor_exactAt_of_totallyDisconnectedSpace

added def AlgebraicTopology.singularHomologyFunctor

added def AlgebraicTopology.singularHomologyFunctorZeroOfTotallyDisconnectedSpace

Modified Mathlib/CategoryTheory/Limits/Shapes/Products.lean

added def CategoryTheory.Limits.piConst

added def CategoryTheory.Limits.piConstAdj

added def CategoryTheory.Limits.sigmaConst

added def CategoryTheory.Limits.sigmaConstAdj