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 { len := 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 { len := 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_simplex {X : SSet} {n : ℕ} (x : X.obj (Opposite.op { len := n })) (hx : x ∈ X.nonDegenerate n) : (mk x hx).simplex = x

@[simp]

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

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

def SSet.N.induction {X : SSet} {motive : X.N → Sort u_1} (mk : (n : ℕ) → (x : ↑(X.nonDegenerate n)) → motive (mk ↑x ⋯)) (s : X.N) : motive s

Induction principle for the type X.N of nondegenerate simplices of a simplicial set X.

Equations

• SSet.N.induction mk s = mk s.dim ⟨s.simplex, ⋯⟩

@[simp]

theorem SSet.N.induction_mk {X : SSet} {motive : X.N → Sort u_1} (mk : (n : ℕ) → (x : ↑(X.nonDegenerate n)) → motive (mk ↑x ⋯)) {n : ℕ} (s : ↑(X.nonDegenerate n)) : induction mk (N.mk ↑s ⋯) = mk n s

theorem SSet.N.ext_iff {X : SSet} (x y : X.N) : x = y ↔ x.toS = y.toS

@[instance_reducible]

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.lt_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 : { len := x.dim } ⟶ { len := y.dim }) (_ : CategoryTheory.Mono f), (CategoryTheory.ConcreteCategory.hom (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_reducible]

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

theorem SSet.N.iSup_subcomplex_eq_top (X : SSet) : ⨆ (s : X.N), s.subcomplex = ⊤

theorem SSet.N.subcomplex_le_iff {X : SSet} {A B : X.Subcomplex} : A ≤ B ↔ ∀ (s : X.N), s.subcomplex ≤ A → s.subcomplex ≤ B

def SSet.N.opEquiv {X : SSet} : X.op.N ≃o X.N

The bijection X.op.N ≃ X.N.

Equations

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

theorem SSet.N.opEquiv_apply {X : SSet} (x : X.op.N) : opEquiv x = mk (opObjEquiv x.simplex) ⋯

theorem SSet.N.opEquiv_symm_apply {X : SSet} (y : X.N) : (RelIso.symm opEquiv) y = mk (opObjEquiv.symm y.simplex) ⋯

def SSet.N.orderIsoOfIso {X Y : SSet} (e : X ≅ Y) : X.N ≃o Y.N

The bijection X.N ≃ Y.N on nondegenerate simplices of simplicial sets that is induced by an isomorphism X ≅ Y.

Equations

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

theorem SSet.N.orderIsoOfIso_apply {X Y : SSet} (e : X ≅ Y) (x : X.N) : (orderIsoOfIso e) x = mk ((CategoryTheory.ConcreteCategory.hom (e.hom.app (Opposite.op { len := x.dim }))) x.simplex) ⋯

theorem SSet.N.orderIsoOfIso_symm_apply {X Y : SSet} (e : X ≅ Y) (y : Y.N) : (RelIso.symm (orderIsoOfIso e)) y = mk ((CategoryTheory.ConcreteCategory.hom (e.inv.app (Opposite.op { len := y.dim }))) y.simplex) ⋯

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.eq_iff_ofSimplex_eq {X : SSet} {n m : ℕ} (x : X.obj (Opposite.op { len := n })) (y : X.obj (Opposite.op { len := m })) (hx : x ∈ X.nonDegenerate n) (hy : y ∈ X.nonDegenerate m) : { dim := n, simplex := x } = { dim := m, simplex := y } ↔ Subcomplex.ofSimplex x = Subcomplex.ofSimplex y

theorem SSet.S.subcomplex_map_le {X : SSet} (x y : X.S) (f : { len := x.dim } ⟶ { len := y.dim }) (hf : (CategoryTheory.ConcreteCategory.hom (X.map f.op)) y.simplex = x.simplex) : x.subcomplex ≤ y.subcomplex

theorem SSet.S.subcomplex_eq_of_epi {X : SSet} (x y : X.S) (f : { len := x.dim } ⟶ { len := y.dim }) [CategoryTheory.Epi f] (hf : (CategoryTheory.ConcreteCategory.hom (X.map f.op)) y.simplex = x.simplex) : x.subcomplex = y.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

theorem SSet.S.existsUnique_toNπ {X : SSet} {x : X.S} {y : X.N} (hy : x.toN = y) : ∃! f : { len := x.dim } ⟶ { len := y.dim }, CategoryTheory.Epi f ∧ (CategoryTheory.ConcreteCategory.hom (X.map f.op)) y.simplex = x.simplex

noncomputable def SSet.S.toNπ {X : SSet} (x : X.S) : { len := x.dim } ⟶ { len := x.toN.dim }

Given a simplex x : X.S of a simplicial set X, this is the unique (epi)morphism f : ⦋x.dim⦌ ⟶ ⦋x.toN.dim⦌ such that x.simplex is X.map f.op x.toN.simplex where x.toN : X.N is the unique nondegenerate simplex of X which generates the same subcomplex as x.

Equations

• x.toNπ = ⋯.choose

instance SSet.S.instEpiSimplexCategoryToNπ {X : SSet} (x : X.S) : CategoryTheory.Epi x.toNπ

@[simp]

theorem SSet.S.map_toNπ_op_apply {X : SSet} (x : X.S) : (CategoryTheory.ConcreteCategory.hom (X.map x.toNπ.op)) x.toN.simplex = x.simplex

theorem SSet.S.dim_toN_le {X : SSet} (x : X.S) : x.toN.dim ≤ x.dim