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 Mathlib/AlgebraicTopology/SimplicialSet/AnodyneExtensions/Pairing.lean for the study of strong (inner) anodyne extensions.

References

• [Sean Moss, Another approach to the Kan-Quillen model structure][moss-2020]

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

• One or more equations did not get rendered due to their size.

theorem SSet.S.IsUniquelyCodimOneFace.iff {X : SSet} {d : ℕ} (x : X.obj (Opposite.op { len := d })) (y : X.obj (Opposite.op { len := d + 1 })) : { dim := d, simplex := x }.IsUniquelyCodimOneFace { dim := d + 1, simplex := y } ↔ ∃! i : Fin (d + 2), (CategoryTheory.ConcreteCategory.hom (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.ConcreteCategory.hom (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.ConcreteCategory.hom (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.ConcreteCategory.hom (CategoryTheory.SimplicialObject.δ X i)) (y.cast ⋯).simplex = (x.cast hd).simplex ↔ i = hxy.index hd

theorem SSet.S.IsUniquelyCodimOneFace.le {X : SSet} {x y : X.S} (hxy : x.IsUniquelyCodimOneFace y) : x ≤ y

theorem SSet.S.IsUniquelyCodimOneFace.unique {X : SSet} {x y : X.S} (hxy : x.IsUniquelyCodimOneFace y) {d : ℕ} (hd : x.dim = d) (f : { len := d } ⟶ { len := d + 1 }) [CategoryTheory.Mono f] (hf : (CategoryTheory.ConcreteCategory.hom (X.map f.op)) (y.cast ⋯).simplex = (x.cast hd).simplex) : f = SimplexCategory.δ (hxy.index hd)

theorem SSet.S.IsUniquelyCodimOneFace.op {X : SSet} {x y : X.S} (hxy : x.IsUniquelyCodimOneFace y) : (opEquiv.symm x).IsUniquelyCodimOneFace (opEquiv.symm y)

theorem SSet.S.IsUniquelyCodimOneFace.of_iso {X : SSet} {x y : X.S} (hxy : x.IsUniquelyCodimOneFace y) {Y : SSet} (e : X ≅ Y) : { dim := x.dim, simplex := (CategoryTheory.ConcreteCategory.hom (e.hom.app (Opposite.op { len := x.dim }))) x.simplex }.IsUniquelyCodimOneFace { dim := y.dim, simplex := (CategoryTheory.ConcreteCategory.hom (e.hom.app (Opposite.op { len := y.dim }))) y.simplex }

theorem SSet.S.IsUniquelyCodimOneFace.iff_of_iso {X Y : SSet} (e : X ≅ Y) (x y : X.S) : { dim := x.dim, simplex := (CategoryTheory.ConcreteCategory.hom (e.hom.app (Opposite.op { len := x.dim }))) x.simplex }.IsUniquelyCodimOneFace { dim := y.dim, simplex := (CategoryTheory.ConcreteCategory.hom (e.hom.app (Opposite.op { len := y.dim }))) y.simplex } ↔ x.IsUniquelyCodimOneFace y