Commit 2025-12-05 16:31 3e37eff7

View on Github →

feat(AlgebraicTopology): horns in Δ[2] as pushouts (#31802) Horns in Δ[2] are pushouts of two copies of Δ[1]. From https://github.com/joelriou/topcat-model-category

Estimated changes

Modified Mathlib.lean

Modified Mathlib/AlgebraicTopology/SimplicialSet/Horn.lean

added theorem SSet.horn.faceSingletonComplIso_inv_ι

added def SSet.horn.faceι

added theorem SSet.horn.faceι_ι

added theorem SSet.horn.yonedaEquiv_ι

added def SSet.horn.ι

added theorem SSet.horn.ι_ι

Created Mathlib/AlgebraicTopology/SimplicialSet/HornColimits.lean

added theorem SSet.horn₂₀.isPushout

added theorem SSet.horn₂₀.sq

added theorem SSet.horn₂₁.isPushout

added theorem SSet.horn₂₁.sq

added theorem SSet.horn₂₂.isPushout

added theorem SSet.horn₂₂.sq

Modified Mathlib/AlgebraicTopology/SimplicialSet/StdSimplex.lean

added def SSet.stdSimplex.faceSingletonComplIso

added theorem SSet.stdSimplex.faceSingletonComplIso_hom_ι

added theorem SSet.stdSimplex.faceSingletonIso_one_hom_comp_ι_eq_δ

added theorem SSet.stdSimplex.faceSingletonIso_zero_hom_comp_ι_eq_δ

added theorem SSet.stdSimplex.face_singleton_compl

added def SSet.stdSimplex.finSuccAboveOrderIsoFinset

Modified Mathlib/AlgebraicTopology/SimplicialSet/Subcomplex.lean

Modified Mathlib/CategoryTheory/Limits/Shapes/Pullback/CommSq.lean

added theorem CategoryTheory.IsPullback.of_iso'

added theorem CategoryTheory.IsPushout.of_iso'