The partially ordered type of non degenerate simplices of a simplicial set

In this file, we introduce the partially ordered type X.N of non degenerate simplices of a simplicial set X. We obtain an embedding X.orderEmbeddingN : X.N ↪o X.Subcomplex which sends a non degenerate simplex to the subcomplex of X it generates.

Given an arbitrary simplex x : X.S, we show that there is a unique non degenerate x.toN : X.N such that x.toN.subcomplex = x.subcomplex.

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

The type of non degenerate simplices of a simplicial set.

• mk' :: (
• dim : ℕ
• simplex : X.obj (Opposite.op (SimplexCategory.mk self.dim))
• nonDegenerate : self.simplex ∈ X.nonDegenerate self.dim
• )

theorem SSet.N.mk'_surjective {X : SSet} (s : X.N) : ∃ (t : X.S) (ht : t.simplex ∈ X.nonDegenerate t.dim), s = { toS := t, nonDegenerate := ht }

def SSet.N.mk {X : SSet} {n : ℕ} (x : X.obj (Opposite.op (SimplexCategory.mk n))) (hx : x ∈ X.nonDegenerate n) : X.N

Constructor for the type of non degenerate simplices of a simplicial set.

Equations

• SSet.N.mk x hx = { dim := n, simplex := x, nonDegenerate := hx }

@[simp]

theorem SSet.N.mk_dim {X : SSet} {n : ℕ} (x : X.obj (Opposite.op (SimplexCategory.mk n))) (hx : x ∈ X.nonDegenerate n) : (mk x hx).dim = n

@[simp]

theorem SSet.N.mk_simplex {X : SSet} {n : ℕ} (x : X.obj (Opposite.op (SimplexCategory.mk n))) (hx : x ∈ X.nonDegenerate n) : (mk x hx).simplex = x

theorem SSet.N.mk_surjective {X : SSet} (x : X.N) : ∃ (n : ℕ) (y : ↑(X.nonDegenerate n)), x = mk ↑y ⋯

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

Equations

• SSet.N.instPreorder = Preorder.lift SSet.N.toS

theorem SSet.N.le_iff {X : SSet} {x y : X.N} : x ≤ y ↔ x.subcomplex ≤ y.subcomplex

theorem SSet.N.le_iff_exists_mono {X : SSet} {x y : X.N} : x ≤ y ↔ ∃ (f : SimplexCategory.mk x.dim ⟶ SimplexCategory.mk y.dim) (_ : CategoryTheory.Mono f), X.map f.op y.simplex = x.simplex

theorem SSet.N.dim_le_of_le {X : SSet} {x y : X.N} (h : x ≤ y) : x.dim ≤ y.dim

theorem SSet.N.dim_lt_of_lt {X : SSet} {x y : X.N} (h : x < y) : x.dim < y.dim

instance SSet.N.instPartialOrder {X : SSet} : PartialOrder X.N

Equations

• SSet.N.instPartialOrder = { toPreorder := SSet.N.instPreorder, le_antisymm := ⋯ }

theorem SSet.N.subcomplex_injective {X : SSet} {x y : X.N} (h : x.subcomplex = y.subcomplex) : x = y

theorem SSet.N.subcomplex_injective_iff {X : SSet} {x y : X.N} : x.subcomplex = y.subcomplex ↔ x = y

theorem SSet.N.eq_iff {X : SSet} {x y : X.N} : x = y ↔ x.subcomplex = y.subcomplex

@[reducible, inline]

abbrev SSet.N.cast {X : SSet} (s : X.N) {d : ℕ} (hd : s.dim = d) : X.N

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

Equations

• s.cast hd = { toS := s.cast hd, nonDegenerate := ⋯ }

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

def SSet.orderEmbeddingN (X : SSet) : X.N ↪o X.Subcomplex

The map which sends a non degenerate simplex of a simplicial set to the subcomplex it generates is an order embedding.

Equations

• X.orderEmbeddingN = { toFun := fun (x : X.N) => x.subcomplex, inj' := ⋯, map_rel_iff' := ⋯ }

@[simp]

theorem SSet.orderEmbeddingN_apply (X : SSet) (x : X.N) : X.orderEmbeddingN x = x.subcomplex

theorem SSet.S.existsUnique_n {X : SSet} (x : X.S) : ∃! y : X.N, y.subcomplex = x.subcomplex

noncomputable def SSet.S.toN {X : SSet} (x : X.S) : X.N

This is the non degenerate simplex of a simplicial set which generates the same subcomplex as a given simplex.

Equations

• x.toN = ⋯.choose

@[simp]

theorem SSet.S.subcomplex_toN {X : SSet} (x : X.S) : x.toN.subcomplex = x.subcomplex

theorem SSet.S.toN_eq_iff {X : SSet} {x : X.S} {y : X.N} : x.toN = y ↔ y.subcomplex = x.subcomplex