Simplices that are uniquely codimensional one faces

Let X be a simplicial set. If x : X _⦋d⦌ and y : X _⦋d + 1⦌, we say that x is uniquely a 1-codimensional face of y if there exists a unique i : Fin (d + 2) such that X.δ i y = x. In this file, we extend this to a predicate IsUniquelyCodimOneFace involving two terms in the type X.S of simplices of X. This is used in the file AlgebraicTopology.SimplicialSet.AnodyneExtensions.Pairing for the study of strong (inner) anodyne extensions.

References

• Sean Moss, Another approach to the Kan-Quillen model structure

def SSet.S.IsUniquelyCodimOneFace {X : SSet} (x y : X.S) : Prop

The property that a simplex is uniquely a 1-codimensional face of another simplex

Equations

• x.IsUniquelyCodimOneFace y = (y.dim = x.dim + 1 ∧ ∃! f : SimplexCategory.mk x.dim ⟶ SimplexCategory.mk y.dim, CategoryTheory.Mono f ∧ X.map f.op y.simplex = x.simplex)

theorem SSet.S.IsUniquelyCodimOneFace.iff {X : SSet} {d : ℕ} (x : X.obj (Opposite.op (SimplexCategory.mk d))) (y : X.obj (Opposite.op (SimplexCategory.mk (d + 1)))) : { dim := d, simplex := x }.IsUniquelyCodimOneFace { dim := d + 1, simplex := y } ↔ ∃! i : Fin (d + 2), CategoryTheory.SimplicialObject.δ X i y = x

theorem SSet.S.IsUniquelyCodimOneFace.dim_eq {X : SSet} {x y : X.S} (hxy : x.IsUniquelyCodimOneFace y) : y.dim = x.dim + 1

theorem SSet.S.IsUniquelyCodimOneFace.cast {X : SSet} {x y : X.S} (hxy : x.IsUniquelyCodimOneFace y) {d : ℕ} (hd : x.dim = d) : (x.cast hd).IsUniquelyCodimOneFace (y.cast ⋯)

theorem SSet.S.IsUniquelyCodimOneFace.existsUnique_δ_cast_simplex {X : SSet} {x y : X.S} (hxy : x.IsUniquelyCodimOneFace y) {d : ℕ} (hd : x.dim = d) : ∃! i : Fin (d + 2), CategoryTheory.SimplicialObject.δ X i (y.cast ⋯).simplex = (x.cast hd).simplex

noncomputable def SSet.S.IsUniquelyCodimOneFace.index {X : SSet} {x y : X.S} (hxy : x.IsUniquelyCodimOneFace y) {d : ℕ} (hd : x.dim = d) : Fin (d + 2)

When a d-dimensional simplex x is a 1-codimensional face of y, this is the only i : Fin (d + 2), such that X.δ i y = x (with an abuse of notation: see δ_index and δ_eq_iff for well typed statements).

Equations

• hxy.index hd = ⋯.choose

theorem SSet.S.IsUniquelyCodimOneFace.δ_index {X : SSet} {x y : X.S} (hxy : x.IsUniquelyCodimOneFace y) {d : ℕ} (hd : x.dim = d) : CategoryTheory.SimplicialObject.δ X (hxy.index hd) (y.cast ⋯).simplex = (x.cast hd).simplex

theorem SSet.S.IsUniquelyCodimOneFace.δ_eq_iff {X : SSet} {x y : X.S} (hxy : x.IsUniquelyCodimOneFace y) {d : ℕ} (hd : x.dim = d) (i : Fin (d + 2)) : CategoryTheory.SimplicialObject.δ X i (y.cast ⋯).simplex = (x.cast hd).simplex ↔ i = hxy.index hd