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).
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)}
Instances For
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)ᶜ
Instances For
theorem
SSet.mem_nonDegenerate_iff_notMem_degenerate
(X : SSet)
{n : ℕ}
(x : X.obj (Opposite.op (SimplexCategory.mk n)))
:
@[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)))
:
theorem
SSet.mem_degenerate_iff_notMem_nonDegenerate
(X : SSet)
{n : ℕ}
(x : X.obj (Opposite.op (SimplexCategory.mk n)))
:
@[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)))
:
theorem
SSet.σ_mem_degenerate
(X : SSet)
{n : ℕ}
(i : Fin (n + 1))
(x : X.obj (Opposite.op (SimplexCategory.mk n)))
:
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.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)
:
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)
:
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₂)
:
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₂)
:
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₂)
:
theorem
SSet.Subcomplex.mem_degenerate_iff
{X : SSet}
(A : X.Subcomplex)
{n : ℕ}
(x : ↑(A.obj (Opposite.op (SimplexCategory.mk n))))
:
theorem
SSet.Subcomplex.mem_nonDegenerate_iff
{X : SSet}
(A : X.Subcomplex)
{n : ℕ}
(x : ↑(A.obj (Opposite.op (SimplexCategory.mk 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.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.degenerate_app_apply
{X Y : SSet}
{n : ℕ}
{x : X.obj (Opposite.op (SimplexCategory.mk n))}
(hx : x ∈ X.degenerate n)
(f : X ⟶ Y)
:
theorem
SSet.degenerate_iff_of_isIso
{X Y : SSet}
(f : X ⟶ Y)
[CategoryTheory.IsIso f]
{n : ℕ}
(x : X.obj (Opposite.op (SimplexCategory.mk 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)))
:
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.
Instances For
@[simp]
theorem
SSet.nonDegenerateEquivOfIso_apply_coe
{X Y : SSet}
(e : X ≅ Y)
{n : ℕ}
(x✝ : ↑(X.nonDegenerate n))
:
@[simp]
theorem
SSet.nonDegenerateEquivOfIso_symm_apply_coe
{X Y : SSet}
(e : X ≅ Y)
{n : ℕ}
(x✝ : ↑(Y.nonDegenerate n))
:
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)))
:
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)))
: