Commit 2026-03-27 09:21 8f4ffc6c

View on Github →

feat(AlgebraicTopology/SimplicialSet): the simplicial homotopy induced by a homotopy (#33683) In this PR, we show that a homotopy between morphisms of simplicial sets (given as a morphism X ⊗ Δ[1] ⟶ Y) induces a "combinatorial" simplicial homotopy.

Estimated changes

Modified Mathlib.lean

Created Mathlib/AlgebraicTopology/SimplicialSet/Homotopy.lean

added theorem SSet.Homotopy.h₀

added theorem SSet.Homotopy.h₁

added def SSet.Homotopy

added def SSet.RelativeMorphism.botEquiv

Modified Mathlib/AlgebraicTopology/SimplicialSet/Monoidal.lean

added theorem SSet.ι₀_app_snd_apply

added theorem SSet.ι₁_app_snd_apply

Modified Mathlib/AlgebraicTopology/SimplicialSet/ProdStdSimplexOne.lean

Modified Mathlib/AlgebraicTopology/SimplicialSet/RelativeMorphism.lean

Modified Mathlib/AlgebraicTopology/SimplicialSet/StdSimplex.lean

added theorem SSet.stdSimplex.yonedaEquiv_symm_app_objEquiv_symm

added theorem SSet.stdSimplex.δ_objEquiv_symm_apply

added theorem SSet.stdSimplex.σ_objEquiv_symm_apply