Faces of subintervals in the simplex category

Mathlib's SimplexCategory.subinterval j l h : ⦋l⦌ ⟶ ⦋n⦌ is the inert map onto the vertices j, …, j + l. This file records how it interacts with the coface maps SimplexCategory.δ: a face of a subinterval is again a subinterval, possibly of a face. With j = 0 the subinterval is the front face of a simplex and with j + l = n it is the back face, so these are the identities behind the Alexander–Whitney formula and its compatibility with the simplicial boundary. It also records that a subinterval of a subinterval is a subinterval and that the front face of full length is the identity, the identities behind associativity and the unit laws of the cup product.

@[simp]

theorem SimplexCategory.val_subinterval_toOrderHom_apply {n : ℕ} (j l : ℕ) (hjl : j + l ≤ n) (i : Fin (l + 1)) : ↑((Hom.toOrderHom (subinterval j l hjl)) i) = ↑i + j

theorem SimplexCategory.δ_comp_subinterval_zero {n p : ℕ} (i : Fin (p + 2)) (k : Fin (n + 2)) (hik : ↑i = ↑k) (h : 0 + (p + 1) ≤ n + 1) : CategoryTheory.CategoryStruct.comp (δ i) (subinterval 0 (p + 1) h) = CategoryTheory.CategoryStruct.comp (subinterval 0 p ⋯) (δ k)

A face of a front face is the front face of the corresponding face.

@[simp]

theorem SimplexCategory.δ_last_comp_subinterval_zero {n p : ℕ} (h : 0 + (p + 1) ≤ n) : CategoryTheory.CategoryStruct.comp (δ (Fin.last (p + 1))) (subinterval 0 (p + 1) h) = subinterval 0 p ⋯

The last face of the front (p + 1)-face is the front p-face.

@[simp]

theorem SimplexCategory.δ_zero_comp_subinterval {n j q : ℕ} (h : j + (q + 1) ≤ n) : CategoryTheory.CategoryStruct.comp (δ 0) (subinterval j (q + 1) h) = subinterval (j + 1) q ⋯

The zeroth face of the subinterval starting at j is the subinterval starting at j + 1.

theorem SimplexCategory.δ_succ_comp_subinterval {n j q : ℕ} (i : Fin (q + 1)) (k : Fin (n + 2)) (hik : j + 1 + ↑i = ↑k) (h : j + (q + 1) ≤ n + 1) : CategoryTheory.CategoryStruct.comp (δ i.succ) (subinterval j (q + 1) h) = CategoryTheory.CategoryStruct.comp (subinterval j q ⋯) (δ k)

A positive face of a subinterval is the subinterval of the corresponding face.

@[simp]

theorem SimplexCategory.subinterval_comp_δ_of_le {n j q : ℕ} (k : Fin (n + 2)) (hk : ↑k ≤ j) (h : j + q ≤ n) : CategoryTheory.CategoryStruct.comp (subinterval j q h) (δ k) = subinterval (j + 1) q ⋯

Deleting a vertex before a subinterval shifts the subinterval.

@[simp]

theorem SimplexCategory.subinterval_zero_comp_δ_of_lt {n p : ℕ} (k : Fin (n + 2)) (hk : p < ↑k) (h : 0 + p ≤ n) : CategoryTheory.CategoryStruct.comp (subinterval 0 p h) (δ k) = subinterval 0 p ⋯

Deleting a vertex after a front face does not change it.

theorem TauCeti.SimplexCategory.subinterval_comp_subinterval {n m : ℕ} (i l j j' : ℕ) (h : i + l ≤ m) (h' : j + m ≤ n) (hj' : j + i = j') : CategoryTheory.CategoryStruct.comp (SimplexCategory.subinterval i l h) (SimplexCategory.subinterval j m h') = SimplexCategory.subinterval j' l ⋯

A subinterval of a subinterval is a subinterval: the vertices i, …, i + l of the subinterval j, …, j + m are the vertices j + i, …, j + i + l.

@[simp]

theorem TauCeti.SimplexCategory.subinterval_zero_eq_id {n : ℕ} (h : 0 + n ≤ n) : SimplexCategory.subinterval 0 n h = CategoryTheory.CategoryStruct.id { len := n }

The front face of full length is the identity.