The preordered type of simplices of a simplicial set

In this file, we define the type X.S of simplices of a simplicial set X, where a simplex consists of the data of dim : ℕ and simplex : X _⦋dim⦌. We endow this type with a preorder defined by x ≤ y ↔ Subcomplex.ofSimplex x.simplex ≤ Subcomplex.ofSimplex y.simplex. In particular, as a preordered type, X.S is a category, but this is not what is called "the category of simplices of X" in the literature (and which is X.Elementsᵒᵖ in mathlib).

TODO (@joelriou)

• Extend the S structure to define the type of nondegenerate simplices of a simplicial set X, and also the type of nondegenerate simplices of a simplicial set X which do not belong to a given subcomplex.

structure SSet.S (X : SSet) : Type u

The type of simplices of a simplicial set X. This type X.S is in bijection with X.Elements (see SSet.S.equivElements), but X.S is not what the literature names "category of simplices of X", as the category on X.S comes from a preorder (see S.le_iff_nonempty_hom).

• dim : ℕ

  the dimension of the simplex

• simplex : X.obj (Opposite.op (SimplexCategory.mk self.dim))

  the simplex

theorem SSet.S.mk_surjective {X : SSet} (s : X.S) : ∃ (n : ℕ) (x : X.obj (Opposite.op (SimplexCategory.mk n))), s = { dim := n, simplex := x }

def SSet.S.map {X Y : SSet} (f : X ⟶ Y) (s : X.S) : Y.S

The image of a simplex by a morphism of simplicial sets.

theorem SSet.S.dim_eq_of_eq {X : SSet} {s t : X.S} (h : s = t) : s.dim = t.dim

theorem SSet.S.dim_eq_of_mk_eq {X : SSet} {n m : ℕ} {x : X.obj (Opposite.op (SimplexCategory.mk n))} {y : X.obj (Opposite.op (SimplexCategory.mk m))} (h : { dim := n, simplex := x } = { dim := m, simplex := y }) : n = m

def SSet.S.cast {X : SSet} (s : X.S) {d : ℕ} (hd : s.dim = d) : X.S

When s : X.S is such that s.dim = d, this is a term that is equal to s, but whose dimension if definitionally equal to d.

@[simp]

theorem SSet.S.cast_dim {X : SSet} (s : X.S) {d : ℕ} (hd : s.dim = d) : (s.cast hd).dim = d

theorem SSet.S.cast_eq_self {X : SSet} (s : X.S) {d : ℕ} (hd : s.dim = d) : s.cast hd = s

@[simp]

theorem SSet.S.cast_simplex_rfl {X : SSet} (s : X.S) : (s.cast ⋯).simplex = s.simplex

theorem SSet.S.ext_iff' {X : SSet} (s t : X.S) : s = t ↔ ∃ (h : s.dim = t.dim), (s.cast h).simplex = t.simplex

theorem SSet.S.ext_iff {X : SSet} {n : ℕ} (x y : X.obj (Opposite.op (SimplexCategory.mk n))) : { dim := n, simplex := x } = { dim := n, simplex := y } ↔ x = y

@[reducible, inline]

abbrev SSet.S.subcomplex {X : SSet} (s : X.S) : X.Subcomplex

The subcomplex generated by a simplex.

@[implicit_reducible]

instance SSet.S.instPreorder {X : SSet} : Preorder X.S

If s : X.S and t : X.S are simplices of a simplicial set, s ≤ t means that the subcomplex generated by s is contained in the subcomplex generated by t, see SSet.S.le_def and SSet.S.le_iff. Note that the category structure on X.S induced by this preorder is not the "category of simplices" of X (which is see X.Elementsᵒᵖ); see SSet.S.le_iff_nonempty_hom for the precise relation.

theorem SSet.S.le_def {X : SSet} {s t : X.S} : s ≤ t ↔ s.subcomplex ≤ t.subcomplex

theorem SSet.S.le_iff {X : SSet} {s t : X.S} : s ≤ t ↔ ∃ (f : SimplexCategory.mk s.dim ⟶ SimplexCategory.mk t.dim), X.map f.op t.simplex = s.simplex

theorem SSet.S.mk_map_le {X : SSet} {n m : ℕ} (x : X.obj (Opposite.op (SimplexCategory.mk n))) (f : SimplexCategory.mk m ⟶ SimplexCategory.mk n) : { dim := m, simplex := X.map f.op x } ≤ { dim := n, simplex := x }

theorem SSet.S.mk_map_eq_iff_of_mono {X : SSet} {n m : ℕ} (x : X.obj (Opposite.op (SimplexCategory.mk n))) (f : SimplexCategory.mk m ⟶ SimplexCategory.mk n) [CategoryTheory.Mono f] : { dim := m, simplex := X.map f.op x } = { dim := n, simplex := x } ↔ CategoryTheory.IsIso f

def SSet.S.equivElements {X : SSet} : X.S ≃ CategoryTheory.Functor.Elements X

The type of simplices of X : SSet.{u} identifies to the type of elements of X considered as a functor SimplexCategoryᵒᵖ ⥤ Type u. (Note that this is not an (anti)equivalence of categories, see S.le_iff_nonempty_hom.)

@[simp]

theorem SSet.S.equivElements_symm_apply_dim {X : SSet} (a✝ : CategoryTheory.Functor.Elements X) : (equivElements.symm a✝).dim = (Opposite.unop a✝.1).len

@[simp]

theorem SSet.S.equivElements_symm_apply_simplex {X : SSet} (a✝ : CategoryTheory.Functor.Elements X) : (equivElements.symm a✝).simplex = a✝.snd

@[simp]

theorem SSet.S.equivElements_apply_fst {X : SSet} (s : X.S) : (equivElements s).fst = Opposite.op (SimplexCategory.mk s.dim)

@[simp]

theorem SSet.S.equivElements_apply_snd {X : SSet} (s : X.S) : (equivElements s).snd = s.simplex

theorem SSet.S.le_iff_nonempty_hom {X : SSet} (x y : X.S) : x ≤ y ↔ Nonempty (equivElements y ⟶ equivElements x)