Commit 2025-10-29 00:03 91235951

View on Github →

feat(AlgebraicTopology/SimplicialSet): pairings of non degenerate simplices, following Sean Moss (#28332) In this PR, we introduce the notion of pairing for a subcomplex of a simplicial set. Following the work of Sean Moss, Another approach to the Kan-Quillen model structure, this is an essential tool in the study of (inner) anodyne extensions.

Estimated changes

Modified Mathlib.lean

Created Mathlib/AlgebraicTopology/SimplicialSet/AnodyneExtensions/IsUniquelyCodimOneFace.lean

added theorem SSet.S.IsUniquelyCodimOneFace.cast

added theorem SSet.S.IsUniquelyCodimOneFace.dim_eq

added theorem SSet.S.IsUniquelyCodimOneFace.existsUnique_δ_cast_simplex

added theorem SSet.S.IsUniquelyCodimOneFace.iff

added theorem SSet.S.IsUniquelyCodimOneFace.δ_eq_iff

added theorem SSet.S.IsUniquelyCodimOneFace.δ_index

added def SSet.S.IsUniquelyCodimOneFace

Created Mathlib/AlgebraicTopology/SimplicialSet/AnodyneExtensions/Pairing.lean

added def SSet.Subcomplex.Pairing.AncestralRel

added theorem SSet.Subcomplex.Pairing.isUniquelyCodimOneFace

added theorem SSet.Subcomplex.Pairing.wf

added structure SSet.Subcomplex.Pairing

Modified Mathlib/AlgebraicTopology/SimplicialSet/NonDegenerateSimplicesSubcomplex.lean

added theorem SSet.Subcomplex.N.le_iff

Modified docs/references.bib