Documentation

Mathlib.AlgebraicTopology.SimplexCategory.ToMkOne

Morphisms to ⦋1⦌ #

We define a bijective map SimplexCategory.toMk₁ : Fin (n + 2) → ⦋n⦌ ⟶ ⦋1⦌. This is used in the file Mathlib.AlgebraicTopology.SimplicialSet.StdSimplexOne in the study of simplices in the simplicial set Δ[1].

source
def SimplexCategory.toMk₁ {n : ℕ} (i : Fin (n + 2)) :
{ len := n } ⟶ { len := 1 }

Given i : Fin (n + 2), this is the morphism ⦋n⦌ ⟶ ⦋1⦌ in the simplex category which corresponds to the monotone map Fin (n + 1) → Fin 2 which takes i times the value 0.

Equations
Instances For
    source
    theorem SimplexCategory.toMk₁_apply {n : ℕ} (i : Fin (n + 2)) (j : Fin (n + 1)) :
    (CategoryTheory.ConcreteCategory.hom (toMk₁ i)) j = if j.castSucc < i then 0 else 1
    source
    theorem SimplexCategory.toMk₁_apply_eq_zero_iff {n : ℕ} (i : Fin (n + 2)) (j : Fin (n + 1)) :
    (CategoryTheory.ConcreteCategory.hom (toMk₁ i)) j = 0 ↔ j.castSucc < i
    source
    theorem SimplexCategory.toMk₁_of_castSucc_lt {n : ℕ} (i : Fin (n + 2)) (j : Fin (n + 1)) (h : j.castSucc < i) :
    (CategoryTheory.ConcreteCategory.hom (toMk₁ i)) j = 0
    source
    theorem SimplexCategory.toMk₁_apply_eq_one_iff {n : ℕ} (i : Fin (n + 2)) (j : Fin (n + 1)) :
    (CategoryTheory.ConcreteCategory.hom (toMk₁ i)) j = 1 ↔ i ≤ j.castSucc
    source
    theorem SimplexCategory.toMk₁_of_le_castSucc {n : ℕ} (i : Fin (n + 2)) (j : Fin (n + 1)) (h : i ≤ j.castSucc) :
    (CategoryTheory.ConcreteCategory.hom (toMk₁ i)) j = 1
    source
    theorem SimplexCategory.δ_comp_toMk₁_of_le {n : ℕ} (i : Fin (n + 3)) (j : Fin (n + 2)) (h : i ≤ j.castSucc) :
    CategoryTheory.CategoryStruct.comp (δ j) (toMk₁ i) = toMk₁ (i.castPred ⋯)
    source
    theorem SimplexCategory.δ_comp_toMk₁_of_lt {n : ℕ} (i : Fin (n + 3)) (j : Fin (n + 2)) (h : j.castSucc < i) :
    CategoryTheory.CategoryStruct.comp (δ j) (toMk₁ i) = toMk₁ (i.pred ⋯)
    source
    theorem SimplexCategory.σ_comp_toMk₁_of_le {n : ℕ} (i : Fin (n + 2)) (j : Fin (n + 1)) (h : i ≤ j.castSucc) :
    CategoryTheory.CategoryStruct.comp (σ j) (toMk₁ i) = toMk₁ i.castSucc
    source
    theorem SimplexCategory.σ_comp_toMk₁_of_lt {n : ℕ} (i : Fin (n + 2)) (j : Fin (n + 1)) (h : j.castSucc < i) :
    CategoryTheory.CategoryStruct.comp (σ j) (toMk₁ i) = toMk₁ i.succ
    source
    theorem SimplexCategory.toMk₁_injective {n : ℕ} :
    Function.Injective toMk₁
    source
    theorem SimplexCategory.toMk₁_surjective {n : ℕ} :
    Function.Surjective toMk₁
    source
    theorem SimplexCategory.toMk₁_bijective {n : ℕ} :
    Function.Bijective toMk₁
    source
    noncomputable def SimplexCategory.toMk₁Equiv {n : ℕ} :
    Fin (n + 2) ≃ ({ len := n } ⟶ { len := 1 })

    The bijection Fin (n + 2) ≃ (⦋n⦌ ⟶ ⦋1⦌) which sends i : Fin (n + 2) to the morphism ⦋n⦌ ⟶ ⦋1⦌ in the simplex category which corresponds to the monotone map Fin (n + 1) → Fin 2 which takes i times the value 0.

    Equations
    Instances For
      source
      @[simp]
      theorem SimplexCategory.toMk₁Equiv_apply {n : ℕ} (i : Fin (n + 2)) :
      toMk₁Equiv i = toMk₁ i