Commit 2025-03-02 19:56 77e679bf

View on Github →

feat(Algebra/Homology): the constant alternating complex is homotopy equivalent to a single complex (#21569)

Estimated changes

Modified Mathlib/Algebra/Homology/AlternatingConst.lean

added def AlgebraicTopology.alternatingFaceMapComplexConst

modified def ChainComplex.alternatingConst

Modified Mathlib/AlgebraicTopology/AlternatingFaceMapComplex.lean

deleted def AlgebraicTopology.alternatingFaceMapComplexConst

Modified Mathlib/AlgebraicTopology/ExtraDegeneracy.lean

added def CategoryTheory.SimplicialObject.Augmented.ExtraDegeneracy.const

added def CategoryTheory.SimplicialObject.Augmented.ExtraDegeneracy.map

added def CategoryTheory.SimplicialObject.Augmented.ExtraDegeneracy.ofIso

added structure CategoryTheory.SimplicialObject.Augmented.ExtraDegeneracy

deleted def SimplicialObject.Augmented.ExtraDegeneracy.map

deleted def SimplicialObject.Augmented.ExtraDegeneracy.ofIso

deleted structure SimplicialObject.Augmented.ExtraDegeneracy

Modified Mathlib/AlgebraicTopology/SimplicialObject/Basic.lean

added def CategoryTheory.CosimplicialObject.Augmented.const

added def CategoryTheory.SimplicialObject.Augmented.const

Modified Mathlib/AlgebraicTopology/SingularHomology/Basic.lean