Degenerate simplices

Given a simplicial set X and n : ℕ, we define the sets X.degenerate n and X.nonDegenerate n of degenerate or non-degenerate simplices of dimension n.

Any simplex x : X _⦋n⦌ can be written in a unique way as X.map f.op y for an epimorphism f : ⦋n⦌ ⟶ ⦋m⦌ and a non-degenerate m-simplex y (see lemmas exists_nonDegenerate, unique_nonDegenerate_dim, unique_nonDegenerate_simplex and unique_nonDegenerate_map).

def SSet.degenerate (X : SSet) (n : ℕ) : Set (X.obj (Opposite.op { len := n }))

An n-simplex of a simplicial set X is degenerate if it is in the range of X.map f.op for some morphism f : [n] ⟶ [m] with m < n.

Equations

• X.degenerate n = {x : X.obj (Opposite.op { len := n }) | ∃ (m : ℕ) (_ : m < n) (f : { len := n } ⟶ { len := m }), x ∈ Set.range ⇑(CategoryTheory.ConcreteCategory.hom (X.map f.op))}

def SSet.nonDegenerate (X : SSet) (n : ℕ) : Set (X.obj (Opposite.op { len := n }))

The set of n-dimensional non-degenerate simplices in a simplicial set X is the complement of X.degenerate n.

Equations

• X.nonDegenerate n = (X.degenerate n)ᶜ

@[simp]

theorem SSet.degenerate_zero (X : SSet) : X.degenerate 0 = ∅

@[simp]

theorem SSet.nondegenerate_zero (X : SSet) : X.nonDegenerate 0 = Set.univ

theorem SSet.mem_nonDegenerate_iff_notMem_degenerate (X : SSet) {n : ℕ} (x : X.obj (Opposite.op { len := n })) : x ∈ X.nonDegenerate n ↔ x ∉ X.degenerate n

theorem SSet.mem_degenerate_iff_notMem_nonDegenerate (X : SSet) {n : ℕ} (x : X.obj (Opposite.op { len := n })) : x ∈ X.degenerate n ↔ x ∉ X.nonDegenerate n

theorem SSet.σ_mem_degenerate (X : SSet) {n : ℕ} (i : Fin (n + 1)) (x : X.obj (Opposite.op { len := n })) : (CategoryTheory.ConcreteCategory.hom (CategoryTheory.SimplicialObject.σ X i)) x ∈ X.degenerate (n + 1)

theorem SSet.mem_degenerate_iff (X : SSet) {n : ℕ} (x : X.obj (Opposite.op { len := n })) : x ∈ X.degenerate n ↔ ∃ (m : ℕ) (_ : m < n) (f : { len := n } ⟶ { len := m }) (_ : CategoryTheory.Epi f), x ∈ Set.range ⇑(CategoryTheory.ConcreteCategory.hom (X.map f.op))

theorem SSet.opObjEquiv_mem_degenerate_iff (X : SSet) {n : ℕ} (x : X.op.obj (Opposite.op { len := n })) : opObjEquiv x ∈ X.degenerate n ↔ x ∈ X.op.degenerate n

theorem SSet.opObjEquiv_mem_nonDegenerate_iff (X : SSet) {n : ℕ} (x : X.op.obj (Opposite.op { len := n })) : opObjEquiv x ∈ X.nonDegenerate n ↔ x ∈ X.op.nonDegenerate n

theorem SSet.degenerate_eq_iUnion_range_σ (X : SSet) {n : ℕ} : X.degenerate (n + 1) = ⋃ (i : Fin (n + 1)), Set.range ⇑(CategoryTheory.ConcreteCategory.hom (CategoryTheory.SimplicialObject.σ X i))

theorem SSet.exists_nonDegenerate (X : SSet) {n : ℕ} (x : X.obj (Opposite.op { len := n })) : ∃ (m : ℕ) (f : { len := n } ⟶ { len := m }) (_ : CategoryTheory.Epi f) (y : ↑(X.nonDegenerate m)), x = (CategoryTheory.ConcreteCategory.hom (X.map f.op)) ↑y

theorem SSet.isIso_of_nonDegenerate (X : SSet) {n : ℕ} (x : ↑(X.nonDegenerate n)) {m : SimplexCategory} (f : { len := n } ⟶ m) [CategoryTheory.Epi f] (y : X.obj (Opposite.op m)) (hy : (CategoryTheory.ConcreteCategory.hom (X.map f.op)) y = ↑x) : CategoryTheory.IsIso f

theorem SSet.mono_of_nonDegenerate (X : SSet) {n : ℕ} (x : ↑(X.nonDegenerate n)) {m : SimplexCategory} (f : { len := n } ⟶ m) (y : X.obj (Opposite.op m)) (hy : (CategoryTheory.ConcreteCategory.hom (X.map f.op)) y = ↑x) : CategoryTheory.Mono f

Auxiliary definitions and lemmas for the lemmas unique_nonDegenerate_dim, unique_nonDegenerate_simplex and unique_nonDegenerate_map which assert the uniqueness of the decomposition obtained in the lemma exists_nonDegenerate.

The following lemmas unique_nonDegenerate_dim, unique_nonDegenerate_simplex and unique_nonDegenerate_map assert the uniqueness of the decomposition obtained in the lemma exists_nonDegenerate.

theorem SSet.unique_nonDegenerate_dim (X : SSet) {n : ℕ} (x : X.obj (Opposite.op { len := n })) {m₁ m₂ : ℕ} (f₁ : { len := n } ⟶ { len := m₁ }) [CategoryTheory.Epi f₁] (y₁ : ↑(X.nonDegenerate m₁)) (hy₁ : x = (CategoryTheory.ConcreteCategory.hom (X.map f₁.op)) ↑y₁) (f₂ : { len := n } ⟶ { len := m₂ }) [CategoryTheory.Epi f₂] (y₂ : ↑(X.nonDegenerate m₂)) (hy₂ : x = (CategoryTheory.ConcreteCategory.hom (X.map f₂.op)) ↑y₂) : m₁ = m₂

theorem SSet.unique_nonDegenerate_simplex (X : SSet) {n : ℕ} (x : X.obj (Opposite.op { len := n })) {m : ℕ} (f₁ : { len := n } ⟶ { len := m }) [CategoryTheory.Epi f₁] (y₁ : ↑(X.nonDegenerate m)) (hy₁ : x = (CategoryTheory.ConcreteCategory.hom (X.map f₁.op)) ↑y₁) (f₂ : { len := n } ⟶ { len := m }) (y₂ : ↑(X.nonDegenerate m)) (hy₂ : x = (CategoryTheory.ConcreteCategory.hom (X.map f₂.op)) ↑y₂) : y₁ = y₂

theorem SSet.unique_nonDegenerate_map (X : SSet) {n : ℕ} (x : X.obj (Opposite.op { len := n })) {m : ℕ} (f₁ : { len := n } ⟶ { len := m }) [CategoryTheory.Epi f₁] (y₁ : ↑(X.nonDegenerate m)) (hy₁ : x = (CategoryTheory.ConcreteCategory.hom (X.map f₁.op)) ↑y₁) (f₂ : { len := n } ⟶ { len := m }) (y₂ : ↑(X.nonDegenerate m)) (hy₂ : x = (CategoryTheory.ConcreteCategory.hom (X.map f₂.op)) ↑y₂) : f₁ = f₂

theorem SSet.Subcomplex.mem_degenerate_iff {X : SSet} (A : X.Subcomplex) {n : ℕ} (x : ↑(A.obj (Opposite.op { len := n }))) : x ∈ A.toSSet.degenerate n ↔ ↑x ∈ X.degenerate n

theorem SSet.Subcomplex.mem_nonDegenerate_iff {X : SSet} (A : X.Subcomplex) {n : ℕ} (x : ↑(A.obj (Opposite.op { len := n }))) : x ∈ A.toSSet.nonDegenerate n ↔ ↑x ∈ X.nonDegenerate n

theorem SSet.Subcomplex.le_iff_contains_nonDegenerate {X : SSet} (A B : X.Subcomplex) : A ≤ B ↔ ∀ (n : ℕ) (x : ↑(X.nonDegenerate n)), ↑x ∈ A.obj (Opposite.op { len := n }) → ↑x ∈ B.obj (Opposite.op { len := n })

theorem SSet.Subcomplex.eq_top_iff_contains_nonDegenerate {X : SSet} (A : X.Subcomplex) : A = ⊤ ↔ ∀ (n : ℕ), X.nonDegenerate n ⊆ A.obj (Opposite.op { len := n })

theorem SSet.Subcomplex.degenerate_eq_top_iff {X : SSet} (A : X.Subcomplex) (n : ℕ) : A.toSSet.degenerate n = ⊤ ↔ X.degenerate n ⊓ A.obj (Opposite.op { len := n }) = A.obj (Opposite.op { len := n })

theorem SSet.Subcomplex.iSup_ofSimplex_nonDegenerate_eq_top (X : SSet) : ⨆ (x : (p : ℕ) × ↑(X.nonDegenerate p)), ofSimplex ↑x.snd = ⊤

theorem SSet.degenerate_app_apply {X Y : SSet} {n : ℕ} {x : X.obj (Opposite.op { len := n })} (hx : x ∈ X.degenerate n) (f : X ⟶ Y) : (CategoryTheory.ConcreteCategory.hom (f.app (Opposite.op { len := n }))) x ∈ Y.degenerate n

theorem SSet.degenerate_le_preimage {X Y : SSet} (f : X ⟶ Y) (n : ℕ) : X.degenerate n ⊆ ⇑(CategoryTheory.ConcreteCategory.hom (f.app (Opposite.op { len := n }))) ⁻¹' Y.degenerate n

theorem SSet.image_degenerate_le {X Y : SSet} (f : X ⟶ Y) (n : ℕ) : ⇑(CategoryTheory.ConcreteCategory.hom (f.app (Opposite.op { len := n }))) '' X.degenerate n ⊆ Y.degenerate n

theorem SSet.degenerate_iff_of_isIso {X Y : SSet} (f : X ⟶ Y) [CategoryTheory.IsIso f] {n : ℕ} (x : X.obj (Opposite.op { len := n })) : (CategoryTheory.ConcreteCategory.hom (f.app (Opposite.op { len := n }))) x ∈ Y.degenerate n ↔ x ∈ X.degenerate n

theorem SSet.nonDegenerate_iff_of_isIso {X Y : SSet} (f : X ⟶ Y) [CategoryTheory.IsIso f] {n : ℕ} (x : X.obj (Opposite.op { len := n })) : (CategoryTheory.ConcreteCategory.hom (f.app (Opposite.op { len := n }))) x ∈ Y.nonDegenerate n ↔ x ∈ X.nonDegenerate n

def SSet.nonDegenerateEquivOfIso {X Y : SSet} (e : X ≅ Y) {n : ℕ} : ↑(X.nonDegenerate n) ≃ ↑(Y.nonDegenerate n)

The bijection on nondegenerate simplices induced by an isomorphism of simplicial sets.

Equations

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

@[simp]

theorem SSet.nonDegenerateEquivOfIso_symm_apply_coe {X Y : SSet} (e : X ≅ Y) {n : ℕ} (x✝ : ↑(Y.nonDegenerate n)) : ↑((nonDegenerateEquivOfIso e).symm x✝) = (CategoryTheory.ConcreteCategory.hom (e.inv.app (Opposite.op { len := n }))) ↑x✝

@[simp]

theorem SSet.nonDegenerateEquivOfIso_apply_coe {X Y : SSet} (e : X ≅ Y) {n : ℕ} (x✝ : ↑(X.nonDegenerate n)) : ↑((nonDegenerateEquivOfIso e) x✝) = (CategoryTheory.ConcreteCategory.hom (e.hom.app (Opposite.op { len := n }))) ↑x✝

theorem SSet.degenerate_iff_of_mono {X : SSet} {n : ℕ} {Y : SSet} (f : X ⟶ Y) [CategoryTheory.Mono f] (x : X.obj (Opposite.op { len := n })) : (CategoryTheory.ConcreteCategory.hom (f.app (Opposite.op { len := n }))) x ∈ Y.degenerate n ↔ x ∈ X.degenerate n

theorem SSet.nonDegenerate_iff_of_mono {X : SSet} {n : ℕ} {Y : SSet} (f : X ⟶ Y) [CategoryTheory.Mono f] (x : X.obj (Opposite.op { len := n })) : (CategoryTheory.ConcreteCategory.hom (f.app (Opposite.op { len := n }))) x ∈ Y.nonDegenerate n ↔ x ∈ X.nonDegenerate n