Commit 2026-04-04 14:07 0bc86d17

View on Github →

chore(AlgebraicTopology): missing API for singular homology (#36939)

Estimated changes

Modified Mathlib/Algebra/Homology/HomologicalComplex.lean

added def HomologicalComplex.dNatTrans

Modified Mathlib/AlgebraicTopology/AlternatingFaceMapComplex.lean

Modified Mathlib/AlgebraicTopology/Quasicategory/StrictSegal.lean

Modified Mathlib/AlgebraicTopology/SimplicialSet/Homotopy.lean

Modified Mathlib/AlgebraicTopology/SimplicialSet/StdSimplex.lean

deleted theorem SSet.stdSimplex.yonedaEquiv_map

deleted theorem SSet.stdSimplex.yonedaEquiv_symm_app_objEquiv_symm

modified def SSet.yonedaEquiv

added theorem SSet.yonedaEquiv_map

added theorem SSet.yonedaEquiv_symm_app

added theorem SSet.yonedaEquiv_symm_app_objEquiv_symm

added theorem SSet.yonedaEquiv_symm_stdSimplex_id

Modified Mathlib/AlgebraicTopology/SingularHomology/Basic.lean

added def AlgebraicTopology.SSet.singularChainComplexFunctorAdjunction

modified theorem AlgebraicTopology.isZero_singularHomologyFunctor_of_totallyDisconnectedSpace

added def AlgebraicTopology.singularChainComplexFunctorAdjunction

added theorem AlgebraicTopology.singularChainComplexFunctorAdjunction_unit_app

modified def AlgebraicTopology.singularHomologyFunctor

modified def AlgebraicTopology.singularHomologyFunctorZeroOfTotallyDisconnectedSpace

added theorem AlgebraicTopology.ι_singularChainComplexFunctorAdjunction_counit_app_app

Modified Mathlib/AlgebraicTopology/SingularSet.lean

added theorem sSetTopAdj_unit_app_app_down

Modified Mathlib/CategoryTheory/Limits/FunctorCategory/EpiMono.lean

Modified Mathlib/CategoryTheory/Preadditive/AdditiveFunctor.lean