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 }

@[implicit_reducible]

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_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

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

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 }

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

@[implicit_reducible]

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

The bijection A.op.N ≃ A.N for a subcomplex A of a simplicial set..

Equations

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

theorem SSet.Subcomplex.N.opEquiv_apply {X : SSet} {A : X.Subcomplex} (x : A.op.N) : opEquiv x = { toN := SSet.N.opEquiv x.toN, notMem := ⋯ }

theorem SSet.Subcomplex.N.opEquiv_symm_apply {X : SSet} {A : X.Subcomplex} (y : A.N) : (RelIso.symm opEquiv) y = { toN := SSet.N.opEquiv.symm y.toN, notMem := ⋯ }

@[implicit_reducible]

def SSet.Subcomplex.N.orderIsoOfIso {X : SSet} {A : X.Subcomplex} {Y : SSet} {B : Y.Subcomplex} (e : X ≅ Y) (hA : B.preimage e.hom = A) : A.N ≃o B.N

The bijection A.N ≃ B.N on nondegenerate simplices not belonging to a certain subcomplex that is induced by an isomorphism X ≅ Y of simplicial sets which maps A : X.Subcomplex to B : Y.Subcomplex.

Equations

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

theorem SSet.Subcomplex.N.orderIsoOfIso_symm_apply {X : SSet} {A : X.Subcomplex} {Y : SSet} {B : Y.Subcomplex} (e : X ≅ Y) (hA : B.preimage e.hom = A) (y : B.N) : (RelIso.symm (orderIsoOfIso e hA)) y = { toN := (SSet.N.orderIsoOfIso e).symm y.toN, notMem := ⋯ }

theorem SSet.Subcomplex.N.orderIsoOfIso_apply {X : SSet} {A : X.Subcomplex} {Y : SSet} {B : Y.Subcomplex} (e : X ≅ Y) (hA : B.preimage e.hom = A) (x : A.N) : (orderIsoOfIso e hA) x = { toN := (SSet.N.orderIsoOfIso e) x.toN, notMem := ⋯ }

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 ∧ (CategoryTheory.ConcreteCategory.hom (X.map f.op)) x.simplex = s