Commit 2026-03-19 13:59 cb339e87

View on Github →

feat(AlgebraicTopology/SimplicialObject): define simplicial homotopy (#32881) This file defines the notion of a combinatorial simplicial homotopy between two morphisms of simplicial objects. A first step towards proving homotopy invariance of simplicial homotopy. See Zulip.

Estimated changes

Modified Mathlib.lean

Created Mathlib/AlgebraicTopology/SimplicialObject/ChainHomotopy.lean

added theorem CategoryTheory.SimplicialObject.Homotopy.ToChainHomotopy.hom_eq

added theorem CategoryTheory.SimplicialObject.Homotopy.ToChainHomotopy.hom_eq_zero

added theorem CategoryTheory.SimplicialObject.Homotopy.map_homology_eq

Created Mathlib/AlgebraicTopology/SimplicialObject/Homotopy.lean

added def CategoryTheory.SimplicialObject.Homotopy.postcomp

added def CategoryTheory.SimplicialObject.Homotopy.precomp

added def CategoryTheory.SimplicialObject.Homotopy.refl

added def CategoryTheory.SimplicialObject.Homotopy.whiskerRight

added structure CategoryTheory.SimplicialObject.Homotopy

Created Mathlib/AlgebraicTopology/SingularHomology/HomotopyInvariance.lean

added theorem singularChainComplexFunctor_map_homology_eq_of_simplicialHomotopy

Modified Mathlib/Data/Fintype/Card.lean

added theorem Finset.compl_eq_of_disjoint_of_card_add_eq