Simplices in Δ[1]

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

def SSet.stdSimplex.objMk₁ {n : ℕ} (i : Fin (n + 2)) : (stdSimplex.obj { len := 1 }).obj (Opposite.op { len := 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.

Equations

• SSet.stdSimplex.objMk₁ i = SSet.stdSimplex.objMk { toFun := fun (j : Fin ((Opposite.unop (Opposite.op { len := n })).len + 1)) => if j.castSucc < i then 0 else 1, monotone' := ⋯ }

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

theorem SSet.stdSimplex.objMk₁_apply_eq_zero_iff {n : ℕ} (i : Fin (n + 2)) (j : Fin (n + 1)) : (objMk₁ i) j = 0 ↔ j.castSucc < i

theorem SSet.stdSimplex.objMk₁_of_castSucc_lt {n : ℕ} (i : Fin (n + 2)) (j : Fin (n + 1)) (h : j.castSucc < i) : (objMk₁ i) j = 0

theorem SSet.stdSimplex.objMk₁_apply_eq_one_iff {n : ℕ} (i : Fin (n + 2)) (j : Fin (n + 1)) : (objMk₁ i) j = 1 ↔ i ≤ j.castSucc

theorem SSet.stdSimplex.objMk₁_of_le_castSucc {n : ℕ} (i : Fin (n + 2)) (j : Fin (n + 1)) (h : i ≤ j.castSucc) : (objMk₁ i) j = 1

theorem SSet.stdSimplex.δ_objMk₁_of_le {n : ℕ} (i : Fin (n + 3)) (j : Fin (n + 2)) (h : i ≤ j.castSucc) : (CategoryTheory.ConcreteCategory.hom (CategoryTheory.SimplicialObject.δ (stdSimplex.obj { len := 1 }) j)) (objMk₁ i) = objMk₁ (i.castPred ⋯)

theorem SSet.stdSimplex.δ_objMk₁_of_lt {n : ℕ} (i : Fin (n + 3)) (j : Fin (n + 2)) (h : j.castSucc < i) : (CategoryTheory.ConcreteCategory.hom (CategoryTheory.SimplicialObject.δ (stdSimplex.obj { len := 1 }) j)) (objMk₁ i) = objMk₁ (i.pred ⋯)

theorem SSet.stdSimplex.σ_objMk₁_of_le {n : ℕ} (i : Fin (n + 2)) (j : Fin (n + 1)) (h : i ≤ j.castSucc) : (CategoryTheory.ConcreteCategory.hom (CategoryTheory.SimplicialObject.σ (stdSimplex.obj { len := 1 }) j)) (objMk₁ i) = objMk₁ i.castSucc

theorem SSet.stdSimplex.σ_objMk₁_of_lt {n : ℕ} (i : Fin (n + 2)) (j : Fin (n + 1)) (h : j.castSucc < i) : (CategoryTheory.ConcreteCategory.hom (CategoryTheory.SimplicialObject.σ (stdSimplex.obj { len := 1 }) j)) (objMk₁ i) = objMk₁ i.succ

theorem SSet.stdSimplex.objMk₁_bijective {n : ℕ} : Function.Bijective objMk₁

theorem SSet.stdSimplex.objMk₁_injective {n : ℕ} : Function.Injective objMk₁

theorem SSet.stdSimplex.objMk₁_surjective {n : ℕ} : Function.Surjective objMk₁