Morphisms to ⦋1⦌

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

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

• SimplexCategory.toMk₁ i = SimplexCategory.Hom.mk { toFun := fun (j : Fin ({ len := n }.len + 1)) => if j.castSucc < i then 0 else 1, monotone' := ⋯ }

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

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

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

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

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

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

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

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

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

theorem SimplexCategory.toMk₁_injective {n : ℕ} : Function.Injective toMk₁

theorem SimplexCategory.toMk₁_surjective {n : ℕ} : Function.Surjective toMk₁

theorem SimplexCategory.toMk₁_bijective {n : ℕ} : Function.Bijective toMk₁

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

• SimplexCategory.toMk₁Equiv = Equiv.ofBijective SimplexCategory.toMk₁ ⋯

@[simp]

theorem SimplexCategory.toMk₁Equiv_apply {n : ℕ} (i : Fin (n + 2)) : toMk₁Equiv i = toMk₁ i