Commit 2026-04-13 14:38 a21ec021

View on Github →

feat(AlgebraicTopology): simplicial homology (#37656) This PRs add some API for simplicial homology, the homology of simplicial sets.

Estimated changes

Modified Mathlib.lean

Created Mathlib/AlgebraicTopology/SimplicialSet/Homology/Basic.lean

added theorem SSet.chainComplex_hom_ext

added theorem SSet.homologyMap_comp

added theorem SSet.homologyMap_id

added theorem SSet.ιChainComplex_d

added theorem SSet.ι_chainComplexMap_f

Renamed Mathlib/AlgebraicTopology/SingularHomology/HomotopyInvariance.lean to Mathlib/AlgebraicTopology/SimplicialSet/Homology/HomotopyInvariance.lean

deleted theorem CategoryTheory.SimplicialObject.Homotopy.congr_homologyMap_singularChainComplexFunctor

added theorem CategoryTheory.SimplicialObject.Homotopy.congr_sSetHomologyMap

added theorem SSet.Homotopy.congr_homologyMap

deleted theorem SSet.Homotopy.congr_homologyMap_singularChainComplexFunctor

Modified Mathlib/AlgebraicTopology/SingularHomology/Basic.lean

deleted def AlgebraicTopology.SSet.singularChainComplexFunctor

deleted def AlgebraicTopology.SSet.singularChainComplexFunctorAdjunction

Modified Mathlib/AlgebraicTopology/SingularHomology/HomotopyInvarianceTopCat.lean