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 (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.

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.

@[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 (SimplexCategory.mk n))) : x ∈ X.nonDegenerate n ↔ x ∉ X.degenerate n

theorem SSet.mem_degenerate_iff_notMem_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

theorem SSet.mono_of_nonDegenerate (X : SSet) {n : ℕ} (x : ↑(X.nonDegenerate n)) {m : SimplexCategory} (f : SimplexCategory.mk n ⟶ m) (y : X.obj (Opposite.op m)) (hy : 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 (SimplexCategory.mk n))) {m₁ m₂ : ℕ} (f₁ : SimplexCategory.mk n ⟶ SimplexCategory.mk m₁) [CategoryTheory.Epi f₁] (y₁ : ↑(X.nonDegenerate m₁)) (hy₁ : x = X.map f₁.op ↑y₁) (f₂ : SimplexCategory.mk n ⟶ SimplexCategory.mk m₂) [CategoryTheory.Epi f₂] (y₂ : ↑(X.nonDegenerate m₂)) (hy₂ : x = X.map f₂.op ↑y₂) : m₁ = m₂

theorem SSet.unique_nonDegenerate_simplex (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)) (hy₁ : x = X.map f₁.op ↑y₁) (f₂ : SimplexCategory.mk n ⟶ SimplexCategory.mk m) (y₂ : ↑(X.nonDegenerate m)) (hy₂ : x = X.map f₂.op ↑y₂) : y₁ = y₂

theorem SSet.unique_nonDegenerate_map (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)) (hy₁ : x = X.map f₁.op ↑y₁) (f₂ : SimplexCategory.mk n ⟶ SimplexCategory.mk m) (y₂ : ↑(X.nonDegenerate m)) (hy₂ : x = X.map f₂.op ↑y₂) : f₁ = f₂

theorem SSet.Subcomplex.mem_degenerate_iff {X : SSet} (A : X.Subcomplex) {n : ℕ} (x : ↑(A.obj (Opposite.op (SimplexCategory.mk 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 (SimplexCategory.mk 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 (SimplexCategory.mk n)) → ↑x ∈ B.obj (Opposite.op (SimplexCategory.mk n))

theorem SSet.Subcomplex.eq_top_iff_contains_nonDegenerate {X : SSet} (A : X.Subcomplex) : A = ⊤ ↔ ∀ (n : ℕ), X.nonDegenerate n ⊆ A.obj (Opposite.op (SimplexCategory.mk 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 (SimplexCategory.mk n)) = A.obj (Opposite.op (SimplexCategory.mk 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 (SimplexCategory.mk n))} (hx : x ∈ X.degenerate n) (f : X ⟶ Y) : f.app (Opposite.op (SimplexCategory.mk n)) x ∈ Y.degenerate n

theorem SSet.degenerate_le_preimage {X Y : SSet} (f : X ⟶ Y) (n : ℕ) : X.degenerate n ⊆ f.app (Opposite.op (SimplexCategory.mk n)) ⁻¹' Y.degenerate n

theorem SSet.image_degenerate_le {X Y : SSet} (f : X ⟶ Y) (n : ℕ) : f.app (Opposite.op (SimplexCategory.mk 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 (SimplexCategory.mk n))) : f.app (Opposite.op (SimplexCategory.mk 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 (SimplexCategory.mk n))) : f.app (Opposite.op (SimplexCategory.mk 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.

@[simp]

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

@[simp]

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

theorem SSet.degenerate_iff_of_mono {X : SSet} {n : ℕ} {Y : SSet} (f : X ⟶ Y) [CategoryTheory.Mono f] (x : X.obj (Opposite.op (SimplexCategory.mk n))) : f.app (Opposite.op (SimplexCategory.mk 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 (SimplexCategory.mk n))) : f.app (Opposite.op (SimplexCategory.mk n)) x ∈ Y.nonDegenerate n ↔ x ∈ X.nonDegenerate n