Iterations of δ 0 and σ 0

This file introduces morphisms δ₀Iter i and σ₀Iter i in the simplex category: they are obtained as the ith iteration of δ 0 or σ 0.

def SimplexCategory.δ₀Iter (i : ℕ) {n m : ℕ} (hi : n + i = m := by lia) : { len := n } ⟶ { len := m }

If n + i = m, this is the morphism ⦋n⦌ ⟶ ⦋m⦌ in the simplex category which is obtained as the ith iteration of δ 0: it sends j : Fin (n + 1) to ⟨j.val + i, _⟩. This may also be described as the order embedding Fin.addNatOrderEmb i : Fin (n + 1) ↪o Fin (n + 1 + i) followed by the order isomorphism Fin (n + 1 + i) ≃o Fin (m + 1).

Equations

• SimplexCategory.δ₀Iter i hi = SimplexCategory.Hom.mk { toFun := fun (j : Fin ({ len := n }.len + 1)) => ⟨↑j + i, ⋯⟩, monotone' := ⋯ }

theorem SimplexCategory.δ₀Iter_apply (i : ℕ) {n m : ℕ} (j : Fin (n + 1)) (hi : n + i = m := by lia) : (CategoryTheory.ConcreteCategory.hom (δ₀Iter i hi)) j = ⟨↑j + i, ⋯⟩

@[simp]

theorem SimplexCategory.δ₀Iter_zero (n : ℕ) : δ₀Iter 0 ⋯ = CategoryTheory.CategoryStruct.id { len := n }

@[simp]

theorem SimplexCategory.δ₀Iter_one (n : ℕ) : δ₀Iter 1 ⋯ = δ 0

theorem SimplexCategory.δ₀Iter_succ (i : ℕ) {n m : ℕ} (h : n + i = m := by lia) : δ₀Iter (i + 1) ⋯ = CategoryTheory.CategoryStruct.comp (δ₀Iter i h) (δ 0)

theorem SimplexCategory.δ₀Iter_succ_assoc (i : ℕ) {n m : ℕ} (h : n + i = m := by lia) {Z : SimplexCategory} (h✝ : { len := m + 1 } ⟶ Z) : CategoryTheory.CategoryStruct.comp (δ₀Iter (i + 1) ⋯) h✝ = CategoryTheory.CategoryStruct.comp (δ₀Iter i h) (CategoryTheory.CategoryStruct.comp (δ 0) h✝)

theorem SimplexCategory.δ₀Iter_succ' (i : ℕ) {n m : ℕ} (h : n + (i + 1) = m := by lia) : δ₀Iter (i + 1) h = CategoryTheory.CategoryStruct.comp (δ 0) (δ₀Iter i ⋯)

theorem SimplexCategory.δ₀Iter_succ'_assoc (i : ℕ) {n m : ℕ} (h : n + (i + 1) = m := by lia) {Z : SimplexCategory} (h✝ : { len := m } ⟶ Z) : CategoryTheory.CategoryStruct.comp (δ₀Iter (i + 1) h) h✝ = CategoryTheory.CategoryStruct.comp (δ 0) (CategoryTheory.CategoryStruct.comp (δ₀Iter i ⋯) h✝)

theorem SimplexCategory.δ₀Iter_δ (i : ℕ) {n m : ℕ} (j : Fin (m + 2)) (hi : n + i = m := by lia) (hj : ↑j ≤ i := by grind) : CategoryTheory.CategoryStruct.comp (δ₀Iter i hi) (δ j) = δ₀Iter (i + 1) ⋯

theorem SimplexCategory.δ₀Iter_δ' {n : ℕ} (i : Fin (n + 2)) (j : ℕ) {m : ℕ} (i' : Fin (m + 2)) (h : n + j = m := by lia) (hi'' : ↑i' = ↑i + j := by grind) : CategoryTheory.CategoryStruct.comp (δ₀Iter j h) (δ i') = CategoryTheory.CategoryStruct.comp (δ i) (δ₀Iter j ⋯)

theorem SimplexCategory.δ₀Iter_δ'_assoc {n : ℕ} (i : Fin (n + 2)) (j : ℕ) {m : ℕ} (i' : Fin (m + 2)) (h : n + j = m := by lia) (hi'' : ↑i' = ↑i + j := by grind) {Z : SimplexCategory} (h✝ : { len := m + 1 } ⟶ Z) : CategoryTheory.CategoryStruct.comp (δ₀Iter j h) (CategoryTheory.CategoryStruct.comp (δ i') h✝) = CategoryTheory.CategoryStruct.comp (δ i) (CategoryTheory.CategoryStruct.comp (δ₀Iter j ⋯) h✝)

theorem SimplexCategory.δ₀Iter_σ (i : ℕ) {n m : ℕ} (j : Fin (m + 1)) (hi : n + (i + 1) = m + 1 := by lia) (hj : ↑j ≤ i := by grind) : CategoryTheory.CategoryStruct.comp (δ₀Iter (i + 1) hi) (σ j) = δ₀Iter i ⋯

theorem SimplexCategory.δ₀Iter_σ_assoc (i : ℕ) {n m : ℕ} (j : Fin (m + 1)) (hi : n + (i + 1) = m + 1 := by lia) (hj : ↑j ≤ i := by grind) {Z : SimplexCategory} (h : { len := m } ⟶ Z) : CategoryTheory.CategoryStruct.comp (δ₀Iter (i + 1) hi) (CategoryTheory.CategoryStruct.comp (σ j) h) = CategoryTheory.CategoryStruct.comp (δ₀Iter i ⋯) h

theorem SimplexCategory.δ₀Iter_σ' (i : ℕ) {n m : ℕ} (j : Fin (m + 1)) (j' : Fin (n + 1)) (hi' : n + i = m := by lia) (hj' : ↑j = ↑j' + i := by grind) : CategoryTheory.CategoryStruct.comp (δ₀Iter i ⋯) (σ j) = CategoryTheory.CategoryStruct.comp (σ j') (δ₀Iter i hi')

theorem SimplexCategory.δ₀Iter_σ'_assoc (i : ℕ) {n m : ℕ} (j : Fin (m + 1)) (j' : Fin (n + 1)) (hi' : n + i = m := by lia) (hj' : ↑j = ↑j' + i := by grind) {Z : SimplexCategory} (h : { len := m } ⟶ Z) : CategoryTheory.CategoryStruct.comp (δ₀Iter i ⋯) (CategoryTheory.CategoryStruct.comp (σ j) h) = CategoryTheory.CategoryStruct.comp (σ j') (CategoryTheory.CategoryStruct.comp (δ₀Iter i hi') h)

def SimplexCategory.σ₀Iter (i : ℕ) {n m : ℕ} (hi : n + i = m := by lia) : { len := m } ⟶ { len := n }

If n + i = m, this is the morphism ⦋m⦌ ⟶ ⦋n⦌ in the simplex category which is obtained as the ith iteration of σ 0.

Equations

• SimplexCategory.σ₀Iter i hi = SimplexCategory.Hom.mk { toFun := fun (j : Fin ({ len := m }.len + 1)) => if ↑j < i then 0 else ⟨↑j - i, ⋯⟩, monotone' := ⋯ }

theorem SimplexCategory.σ₀Iter_coe_eq_of_lt (i : ℕ) {n m : ℕ} (j : Fin (m + 1)) (hi : n + i = m := by lia) (hj : ↑j < i := by grind) : ↑((CategoryTheory.ConcreteCategory.hom (σ₀Iter i hi)) j) = 0

theorem SimplexCategory.σ₀Iter_coe_eq_of_ge (i : ℕ) {n m : ℕ} (j : Fin (m + 1)) (hi : n + i = m := by lia) (hj : i ≤ ↑j := by grind) : ↑((CategoryTheory.ConcreteCategory.hom (σ₀Iter i hi)) j) = ↑j - i

theorem SimplexCategory.σ₀Iter_coe_eq_of_le (i : ℕ) {n m : ℕ} (j : Fin (m + 1)) (hi : n + i = m := by lia) (hj : ↑j ≤ i := by grind) : ↑((CategoryTheory.ConcreteCategory.hom (σ₀Iter i hi)) j) = 0

@[simp]

theorem SimplexCategory.σ₀Iter_zero (n : ℕ) : σ₀Iter 0 ⋯ = CategoryTheory.CategoryStruct.id { len := n }

@[simp]

theorem SimplexCategory.σ₀Iter_one (n : ℕ) : σ₀Iter 1 ⋯ = σ 0

theorem SimplexCategory.σ₀Iter_succ (i : ℕ) {n m : ℕ} (h : n + (i + 1) = m) : σ₀Iter (i + 1) h = CategoryTheory.CategoryStruct.comp (σ₀Iter i ⋯) (σ 0)

theorem SimplexCategory.σ₀Iter_succ_assoc (i : ℕ) {n m : ℕ} (h : n + (i + 1) = m) {Z : SimplexCategory} (h✝ : { len := n } ⟶ Z) : CategoryTheory.CategoryStruct.comp (σ₀Iter (i + 1) h) h✝ = CategoryTheory.CategoryStruct.comp (σ₀Iter i ⋯) (CategoryTheory.CategoryStruct.comp (σ 0) h✝)

theorem SimplexCategory.σ₀Iter_succ' (i : ℕ) {n m : ℕ} (h : n + i = m := by lia) : σ₀Iter (i + 1) ⋯ = CategoryTheory.CategoryStruct.comp (σ 0) (σ₀Iter i h)

theorem SimplexCategory.σ₀Iter_succ'_assoc (i : ℕ) {n m : ℕ} (h : n + i = m := by lia) {Z : SimplexCategory} (h✝ : { len := n } ⟶ Z) : CategoryTheory.CategoryStruct.comp (σ₀Iter (i + 1) ⋯) h✝ = CategoryTheory.CategoryStruct.comp (σ 0) (CategoryTheory.CategoryStruct.comp (σ₀Iter i h) h✝)

theorem SimplexCategory.δ_σ₀Iter {n : ℕ} (i : Fin (n + 2)) (j : ℕ) {m : ℕ} (h : m + (j + 1) = n + 1 := by lia) (hi' : ↑i ≤ j + 1 := by grind) : CategoryTheory.CategoryStruct.comp (δ i) (σ₀Iter (j + 1) h) = σ₀Iter j ⋯

theorem SimplexCategory.δ_σ₀Iter_assoc {n : ℕ} (i : Fin (n + 2)) (j : ℕ) {m : ℕ} (h : m + (j + 1) = n + 1 := by lia) (hi' : ↑i ≤ j + 1 := by grind) {Z : SimplexCategory} (h✝ : { len := m } ⟶ Z) : CategoryTheory.CategoryStruct.comp (δ i) (CategoryTheory.CategoryStruct.comp (σ₀Iter (j + 1) h) h✝) = CategoryTheory.CategoryStruct.comp (σ₀Iter j ⋯) h✝

theorem SimplexCategory.δ_σ₀Iter' {n : ℕ} (i : Fin (n + 2)) (j : ℕ) {m : ℕ} (i' : Fin (m + 2)) (h : m + j = n := by lia) (hi' : j < ↑i := by grind) (hi'' : ↑i = ↑i' + j := by grind) : CategoryTheory.CategoryStruct.comp (δ i) (σ₀Iter j ⋯) = CategoryTheory.CategoryStruct.comp (σ₀Iter j ⋯) (δ i')

theorem SimplexCategory.δ_σ₀Iter'_assoc {n : ℕ} (i : Fin (n + 2)) (j : ℕ) {m : ℕ} (i' : Fin (m + 2)) (h : m + j = n := by lia) (hi' : j < ↑i := by grind) (hi'' : ↑i = ↑i' + j := by grind) {Z : SimplexCategory} (h✝ : { len := m + 1 } ⟶ Z) : CategoryTheory.CategoryStruct.comp (δ i) (CategoryTheory.CategoryStruct.comp (σ₀Iter j ⋯) h✝) = CategoryTheory.CategoryStruct.comp (σ₀Iter j ⋯) (CategoryTheory.CategoryStruct.comp (δ i') h✝)

theorem SimplexCategory.σ_σ₀Iter (i : ℕ) {n m : ℕ} (j : Fin (m + 1)) (hi : n + i = m := by lia) (hj : ↑j ≤ i := by grind) : CategoryTheory.CategoryStruct.comp (σ j) (σ₀Iter i hi) = σ₀Iter (i + 1) ⋯

theorem SimplexCategory.σ_σ₀Iter_assoc (i : ℕ) {n m : ℕ} (j : Fin (m + 1)) (hi : n + i = m := by lia) (hj : ↑j ≤ i := by grind) {Z : SimplexCategory} (h : { len := n } ⟶ Z) : CategoryTheory.CategoryStruct.comp (σ j) (CategoryTheory.CategoryStruct.comp (σ₀Iter i hi) h) = CategoryTheory.CategoryStruct.comp (σ₀Iter (i + 1) ⋯) h

theorem SimplexCategory.σ_σ₀Iter' (i : ℕ) {n m : ℕ} (j : Fin (m + 1)) (j' : Fin (n + 1)) (hi : n + i = m := by lia) (hj : ↑j = ↑j' + i := by grind) : CategoryTheory.CategoryStruct.comp (σ j) (σ₀Iter i hi) = CategoryTheory.CategoryStruct.comp (σ₀Iter i ⋯) (σ j')

theorem SimplexCategory.σ_σ₀Iter'_assoc (i : ℕ) {n m : ℕ} (j : Fin (m + 1)) (j' : Fin (n + 1)) (hi : n + i = m := by lia) (hj : ↑j = ↑j' + i := by grind) {Z : SimplexCategory} (h : { len := n } ⟶ Z) : CategoryTheory.CategoryStruct.comp (σ j) (CategoryTheory.CategoryStruct.comp (σ₀Iter i hi) h) = CategoryTheory.CategoryStruct.comp (σ₀Iter i ⋯) (CategoryTheory.CategoryStruct.comp (σ j') h)

@[simp]

theorem SimplexCategory.δ₀Iter_σ₀Iter (i : ℕ) {n m : ℕ} (hi : n + i = m := by lia) : CategoryTheory.CategoryStruct.comp (δ₀Iter i hi) (σ₀Iter i hi) = CategoryTheory.CategoryStruct.id { len := n }

@[simp]

theorem SimplexCategory.δ₀Iter_σ₀Iter_assoc (i : ℕ) {n m : ℕ} (hi : n + i = m := by lia) {Z : SimplexCategory} (h : { len := n } ⟶ Z) : CategoryTheory.CategoryStruct.comp (δ₀Iter i hi) (CategoryTheory.CategoryStruct.comp (σ₀Iter i hi) h) = h

instance SimplexCategory.instMonoδ₀Iter (i : ℕ) {n m : ℕ} (hi : n + i = m) : CategoryTheory.Mono (δ₀Iter i hi)

instance SimplexCategory.instEpiσ₀Iter (i : ℕ) {n m : ℕ} (hi : n + i = m) : CategoryTheory.Epi (σ₀Iter i hi)