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.

TODO (@joelriou)

• SSet.exists_nonDegenerate shows that any n-simplex can be written as X.map f.op y for some epimorphism f : ⦋n⦌ ⟶ ⦋m⦌ and some non-degenerate simplex y. Show that f and y are unique.

def SSet.degenerate (X : SSet) (n : ℕ) : Set (X.obj (Opposite.op (SimplexCategory.mk 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 (SimplexCategory.mk n)) | ∃ (m : ℕ) (_ : m < n) (f : SimplexCategory.mk n ⟶ SimplexCategory.mk m), x ∈ Set.range (X.map f.op)}

def SSet.nonDegenerate (X : SSet) (n : ℕ) : Set (X.obj (Opposite.op (SimplexCategory.mk 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 = ⊤

theorem SSet.mem_nonDegenerate_iff_not_mem_degenerate (X : SSet) {n : ℕ} (x : X.obj (Opposite.op (SimplexCategory.mk n))) : x ∈ X.nonDegenerate n ↔ x ∉ X.degenerate n

theorem SSet.mem_degenerate_iff_not_mem_nonDegenerate (X : SSet) {n : ℕ} (x : X.obj (Opposite.op (SimplexCategory.mk 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 (SimplexCategory.mk n))) : CategoryTheory.SimplicialObject.σ X i x ∈ X.degenerate (n + 1)

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

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

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

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