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 (SimplexCategory.mk self.dim))
• nonDegenerate : self.simplex ∈ X.nonDegenerate self.dim
• notMem : self.simplex ∉ A.obj (Opposite.op (SimplexCategory.mk 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 (SimplexCategory.mk t.dim))), s = { toN := t, notMem := ht }

def SSet.Subcomplex.N.mk {X : SSet} {A : X.Subcomplex} {n : ℕ} (x : X.obj (Opposite.op (SimplexCategory.mk n))) (hx : x ∈ X.nonDegenerate n) (hx' : x ∉ A.obj (Opposite.op (SimplexCategory.mk 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_dim {X : SSet} {A : X.Subcomplex} {n : ℕ} (x : X.obj (Opposite.op (SimplexCategory.mk n))) (hx : x ∈ X.nonDegenerate n) (hx' : x ∉ A.obj (Opposite.op (SimplexCategory.mk n))) : (mk x hx hx').dim = n

@[simp]

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

theorem SSet.Subcomplex.N.mk_surjective {X : SSet} {A : X.Subcomplex} (s : A.N) : ∃ (n : ℕ) (x : X.obj (Opposite.op (SimplexCategory.mk n))) (hx : x ∈ X.nonDegenerate n) (hx' : x ∉ A.obj (Opposite.op (SimplexCategory.mk 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

@[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