Documentation

Mathlib.AlgebraicTopology.SimplicialSet.StdSimplexOne

Simplices in Δ[1] #

We define a bijection SSet.stdSimplex.objMk₁ between Fin (n + 2) and Δ[1] _⦋n⦌ for any n : ℕ.

source
🔸 coverage
def SSet.stdSimplex.objMk₁ {n : ℕ} (i : Fin (n + 2)) :
(stdSimplex.obj (SimplexCategory.mk 1)).obj (Opposite.op (SimplexCategory.mk n))

Given i : Fin (n + 2), this is the n-simplex of Δ[1] which corresponds to the monotone map Fin (n + 1) → Fin 2 which takes i times the value 0.

Instances For
    source
    📐 coverage
    theorem SSet.stdSimplex.objMk₁_apply {n : ℕ} (i : Fin (n + 2)) (j : Fin (n + 1)) :
    (objMk₁ i) j = if j.castSucc < i then 0 else 1
    source
    📐 coverage
    theorem SSet.stdSimplex.objMk₁_apply_eq_zero_iff {n : ℕ} (i : Fin (n + 2)) (j : Fin (n + 1)) :
    (objMk₁ i) j = 0 ↔ j.castSucc < i
    source
    📐 coverage
    theorem SSet.stdSimplex.objMk₁_of_castSucc_lt {n : ℕ} (i : Fin (n + 2)) (j : Fin (n + 1)) (h : j.castSucc < i) :
    (objMk₁ i) j = 0
    source
    📐 coverage
    theorem SSet.stdSimplex.objMk₁_apply_eq_one_iff {n : ℕ} (i : Fin (n + 2)) (j : Fin (n + 1)) :
    (objMk₁ i) j = 1 ↔ i ≤ j.castSucc
    source
    📐 coverage
    theorem SSet.stdSimplex.objMk₁_of_le_castSucc {n : ℕ} (i : Fin (n + 2)) (j : Fin (n + 1)) (h : i ≤ j.castSucc) :
    (objMk₁ i) j = 1
    source
    📐 coverage
    theorem SSet.stdSimplex.δ_objMk₁_of_le {n : ℕ} (i : Fin (n + 3)) (j : Fin (n + 2)) (h : i ≤ j.castSucc) :
    CategoryTheory.SimplicialObject.δ (stdSimplex.obj (SimplexCategory.mk 1)) j (objMk₁ i) = objMk₁ (i.castPred ⋯)
    source
    📐 coverage
    theorem SSet.stdSimplex.δ_objMk₁_of_lt {n : ℕ} (i : Fin (n + 3)) (j : Fin (n + 2)) (h : j.castSucc < i) :
    CategoryTheory.SimplicialObject.δ (stdSimplex.obj (SimplexCategory.mk 1)) j (objMk₁ i) = objMk₁ (i.pred ⋯)
    source
    📐 coverage
    theorem SSet.stdSimplex.σ_objMk₁_of_le {n : ℕ} (i : Fin (n + 2)) (j : Fin (n + 1)) (h : i ≤ j.castSucc) :
    CategoryTheory.SimplicialObject.σ (stdSimplex.obj (SimplexCategory.mk 1)) j (objMk₁ i) = objMk₁ i.castSucc
    source
    📐 coverage
    theorem SSet.stdSimplex.σ_objMk₁_of_lt {n : ℕ} (i : Fin (n + 2)) (j : Fin (n + 1)) (h : j.castSucc < i) :
    CategoryTheory.SimplicialObject.σ (stdSimplex.obj (SimplexCategory.mk 1)) j (objMk₁ i) = objMk₁ i.succ
    source
    📐 coverage
    theorem SSet.stdSimplex.objMk₁_bijective {n : ℕ} :
    Function.Bijective objMk₁
    source
    📐 coverage
    theorem SSet.stdSimplex.objMk₁_injective {n : ℕ} :
    Function.Injective objMk₁
    source
    📐 coverage
    theorem SSet.stdSimplex.objMk₁_surjective {n : ℕ} :
    Function.Surjective objMk₁