Documentation

Mathlib.AlgebraicTopology.SimplicialSet.Degenerate

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

source
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
Instances For
    source
    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
    Instances For
      source
      @[simp]
      theorem SSet.degenerate_zero (X : SSet) :
      X.degenerate 0 = ∅
      source
      @[simp]
      theorem SSet.nondegenerate_zero (X : SSet) :
      X.nonDegenerate 0 = Set.univ
      source
      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
      source
      @[deprecated SSet.mem_nonDegenerate_iff_notMem_degenerate (since := "2025-05-23")]
      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

      Alias of SSet.mem_nonDegenerate_iff_notMem_degenerate.

      source
      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
      source
      @[deprecated SSet.mem_degenerate_iff_notMem_nonDegenerate (since := "2025-05-23")]
      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

      Alias of SSet.mem_degenerate_iff_notMem_nonDegenerate.

      source
      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)
      source
      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)
      source
      theorem SSet.degenerate_eq_iUnion_range_σ (X : SSet) {n : ℕ} :
      X.degenerate (n + 1) = ⋃ (i : Fin (n + 1)), Set.range (CategoryTheory.SimplicialObject.σ X i)
      source
      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
      source
      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

      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.

      source
      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₂
      source
      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₂
      source
      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₂