The type of nondegenerate simplices not in a subcomplex

In this file, given a subcomplex A of a simplicial set X, we introduce the type A.N of nondegenerate simplices of X that are not in A.

structure SSet.Subcomplex.N {X : SSet} (A : X.Subcomplex) extends X.N : Type u

The type of nondegenerate simplices which do not belong to a given subcomplex of a simplicial set.

• mk' :: (
• dim : ℕ
• simplex : X.obj (Opposite.op { len := self.dim })
• nonDegenerate : self.simplex ∈ X.nonDegenerate self.dim
• notMem : self.simplex ∉ A.obj (Opposite.op { len := self.dim })
• )

theorem SSet.Subcomplex.N.mk'_surjective {X : SSet} {A : X.Subcomplex} (s : A.N) : ∃ (t : X.N) (ht : t.simplex ∉ A.obj (Opposite.op { len := t.dim })), s = { toN := t, notMem := ht }

def SSet.Subcomplex.N.mk {X : SSet} {A : X.Subcomplex} {n : ℕ} (x : X.obj (Opposite.op { len := n })) (hx : x ∈ X.nonDegenerate n) (hx' : x ∉ A.obj (Opposite.op { len := n })) : A.N

Constructor for the type of nondegenerate simplices which do not belong to a given subcomplex of a simplicial set.

Equations

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

@[simp]

theorem SSet.Subcomplex.N.mk_simplex {X : SSet} {A : X.Subcomplex} {n : ℕ} (x : X.obj (Opposite.op { len := n })) (hx : x ∈ X.nonDegenerate n) (hx' : x ∉ A.obj (Opposite.op { len := n })) : (mk x hx hx').simplex = x

@[simp]

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

theorem SSet.Subcomplex.N.mk_surjective {X : SSet} {A : X.Subcomplex} (s : A.N) : ∃ (n : ℕ) (x : X.obj (Opposite.op { len := n })) (hx : x ∈ X.nonDegenerate n) (hx' : x ∉ A.obj (Opposite.op { len := n })), s = mk x hx hx'

theorem SSet.Subcomplex.N.ext_iff {X : SSet} {A : X.Subcomplex} (x y : A.N) : x = y ↔ x.toN = y.toN

theorem SSet.Subcomplex.N.cases {X : SSet} (A : X.Subcomplex) {motive : X.N → Prop} (mem : ∀ (s : X.N), s.subcomplex ≤ A → motive s) (notMem : ∀ (s : A.N), motive s.toN) (s : X.N) : motive s

theorem SSet.Subcomplex.N.eq_iff_sMk_eq {X : SSet} {A : X.Subcomplex} (x y : A.N) : x = y ↔ { dim := x.dim, simplex := x.simplex } = { dim := y.dim, simplex := y.simplex }

@[implicit_reducible]

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

Equations

• SSet.Subcomplex.N.instPartialOrder = PartialOrder.lift SSet.Subcomplex.N.toN ⋯

theorem SSet.Subcomplex.N.le_iff {X : SSet} {A : X.Subcomplex} {x y : A.N} : x ≤ y ↔ x.toN ≤ y.toN

theorem SSet.Subcomplex.N.lt_iff {X : SSet} {A : X.Subcomplex} {x y : A.N} : x < y ↔ x.toN < y.toN

@[reducible, inline]

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

When A is a subcomplex of a simplicial set X, and s : A.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 = { toN := s.cast hd, notMem := ⋯ }

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

theorem SSet.Subcomplex.existsN {X : SSet} {n : ℕ} (s : X.obj (Opposite.op { len := n })) {A : X.Subcomplex} (hs : s ∉ A.obj (Opposite.op { len := n })) : ∃ (x : A.N) (f : { len := n } ⟶ { len := x.dim }), CategoryTheory.Epi f ∧ X.map f.op x.simplex = s