Properties of the truncated simplex category

We prove that for n > 0, the inclusion functor from the n-truncated simplex category to the untruncated simplex category, and the inclusion functor from the n-truncated to the m-truncated simplex category, for n ≤ m are initial.

instance SimplexCategory.Truncated.instDecidableEqHom {d : ℕ} {n m : Truncated d} : DecidableEq (n ⟶ m)

instance SimplexCategory.Truncated.initial_inclusion {n : ℕ} [NeZero n] : (inclusion n).Initial

For 0 < n, the inclusion functor from the n-truncated simplex category to the untruncated simplex category is initial.

theorem SimplexCategory.Truncated.initial_incl {n m : ℕ} [NeZero n] (hm : n ≤ m) : (incl n m hm).Initial

For 0 < n ≤ m, the inclusion functor from the n-truncated simplex category to the m-truncated simplex category is initial.

@[reducible, inline]

abbrev SimplexCategory.Truncated.δ (m : ℕ) {n : ℕ} (i : Fin (n + 2)) (hn : (mk n).len ≤ m := by decide) (hn' : (mk (n + 1)).len ≤ m := by decide) : { obj := mk n, property := hn } ⟶ { obj := mk (n + 1), property := hn' }

Abbreviation for face maps in the n-truncated simplex category.

@[reducible, inline]

abbrev SimplexCategory.Truncated.σ (m : ℕ) {n : ℕ} (i : Fin (n + 1)) (hn : (mk (n + 1)).len ≤ m := by decide) (hn' : (mk n).len ≤ m := by decide) : { obj := mk (n + 1), property := hn } ⟶ { obj := mk n, property := hn' }

Abbreviation for degeneracy maps in the n-truncated simplex category.

@[reducible, inline]

abbrev SimplexCategory.Truncated.δ₂ {n : ℕ} (i : Fin (n + 2)) (hn : (mk n).len ≤ 2 := by decide) (hn' : (mk (n + 1)).len ≤ 2 := by decide) : { obj := mk n, property := hn } ⟶ { obj := mk (n + 1), property := hn' }

Abbreviation for face maps in the 2-truncated simplex category.

@[reducible, inline]

abbrev SimplexCategory.Truncated.σ₂ {n : ℕ} (i : Fin (n + 1)) (hn : (mk (n + 1)).len ≤ 2 := by decide) (hn' : (mk n).len ≤ 2 := by decide) : { obj := mk (n + 1), property := hn } ⟶ { obj := mk n, property := hn' }

Abbreviation for face maps in the 2-truncated simplex category.

@[simp]

theorem SimplexCategory.Truncated.δ₂_zero_comp_σ₂_zero {n : ℕ} (hn : (mk n).len ≤ 2 := by decide) (hn' : (mk (n + 1)).len ≤ 2 := by decide) : CategoryTheory.CategoryStruct.comp (δ₂ 0 hn hn') (σ₂ 0 hn' hn) = CategoryTheory.CategoryStruct.id { obj := mk n, property := hn }

@[simp]

theorem SimplexCategory.Truncated.δ₂_zero_comp_σ₂_zero_assoc {n : ℕ} (hn : (mk n).len ≤ 2 := by decide) (hn' : (mk (n + 1)).len ≤ 2 := by decide) {Z : CategoryTheory.ObjectProperty.FullSubcategory fun (a : SimplexCategory) => a.len ≤ 2} (h : { obj := mk n, property := hn } ⟶ Z) : CategoryTheory.CategoryStruct.comp (δ₂ 0 hn hn') (CategoryTheory.CategoryStruct.comp (σ₂ 0 hn' hn) h) = h

theorem SimplexCategory.Truncated.δ₂_zero_comp_σ₂_one : CategoryTheory.CategoryStruct.comp (δ₂ 0 δ₂_zero_comp_σ₂_one._proof_1 δ₂_zero_comp_σ₂_one._proof_2) (σ₂ 1 δ₂_zero_comp_σ₂_one._proof_2 δ₂_zero_comp_σ₂_one._proof_1) = CategoryTheory.CategoryStruct.comp (σ₂ 0 δ₂_zero_comp_σ₂_one._proof_3 δ₂_zero_comp_σ₂_one._proof_4) (δ₂ 0 δ₂_zero_comp_σ₂_one._proof_4 δ₂_zero_comp_σ₂_one._proof_3)

theorem SimplexCategory.Truncated.δ₂_zero_comp_σ₂_one_assoc {Z : CategoryTheory.ObjectProperty.FullSubcategory fun (a : SimplexCategory) => a.len ≤ 2} (h : { obj := mk 1, property := δ₂_zero_comp_σ₂_one._proof_1 } ⟶ Z) : CategoryTheory.CategoryStruct.comp (δ₂ 0 δ₂_zero_comp_σ₂_one._proof_1 δ₂_zero_comp_σ₂_one._proof_2) (CategoryTheory.CategoryStruct.comp (σ₂ 1 δ₂_zero_comp_σ₂_one._proof_2 δ₂_zero_comp_σ₂_one._proof_1) h) = CategoryTheory.CategoryStruct.comp (σ₂ 0 δ₂_zero_comp_σ₂_one._proof_3 δ₂_zero_comp_σ₂_one._proof_4) (CategoryTheory.CategoryStruct.comp (δ₂ 0 δ₂_zero_comp_σ₂_one._proof_4 δ₂_zero_comp_σ₂_one._proof_3) h)

@[simp]

theorem SimplexCategory.Truncated.δ₂_one_comp_σ₂_zero {n : ℕ} (hn : (mk n).len ≤ 2 := by decide) (hn' : (mk (n + 1)).len ≤ 2 := by decide) : CategoryTheory.CategoryStruct.comp (δ₂ 1 hn hn') (σ₂ 0 hn' hn) = CategoryTheory.CategoryStruct.id { obj := mk n, property := hn }

@[simp]

theorem SimplexCategory.Truncated.δ₂_one_comp_σ₂_zero_assoc {n : ℕ} (hn : (mk n).len ≤ 2 := by decide) (hn' : (mk (n + 1)).len ≤ 2 := by decide) {Z : CategoryTheory.ObjectProperty.FullSubcategory fun (a : SimplexCategory) => a.len ≤ 2} (h : { obj := mk n, property := hn } ⟶ Z) : CategoryTheory.CategoryStruct.comp (δ₂ 1 hn hn') (CategoryTheory.CategoryStruct.comp (σ₂ 0 hn' hn) h) = h

@[simp]

theorem SimplexCategory.Truncated.δ₂_one_comp_σ₂_one {n : ℕ} (hn : (mk (n + 1)).len ≤ 2 := by decide) (hn' : (mk (n + 1 + 1)).len ≤ 2 := by decide) : CategoryTheory.CategoryStruct.comp (δ₂ 1 hn hn') (σ₂ 1 hn' hn) = CategoryTheory.CategoryStruct.id { obj := mk (n + 1), property := hn }

@[simp]

theorem SimplexCategory.Truncated.δ₂_one_comp_σ₂_one_assoc {n : ℕ} (hn : (mk (n + 1)).len ≤ 2 := by decide) (hn' : (mk (n + 1 + 1)).len ≤ 2 := by decide) {Z : CategoryTheory.ObjectProperty.FullSubcategory fun (a : SimplexCategory) => a.len ≤ 2} (h : { obj := mk (n + 1), property := hn } ⟶ Z) : CategoryTheory.CategoryStruct.comp (δ₂ 1 hn hn') (CategoryTheory.CategoryStruct.comp (σ₂ 1 hn' hn) h) = h

@[simp]

theorem SimplexCategory.Truncated.δ₂_two_comp_σ₂_one : CategoryTheory.CategoryStruct.comp (δ₂ 2 δ₂_zero_comp_σ₂_one._proof_1 δ₂_zero_comp_σ₂_one._proof_2) (σ₂ 1 δ₂_zero_comp_σ₂_one._proof_2 δ₂_zero_comp_σ₂_one._proof_1) = CategoryTheory.CategoryStruct.id { obj := mk 1, property := δ₂_zero_comp_σ₂_one._proof_1 }

@[simp]

theorem SimplexCategory.Truncated.δ₂_two_comp_σ₂_one_assoc {Z : CategoryTheory.ObjectProperty.FullSubcategory fun (a : SimplexCategory) => a.len ≤ 2} (h : { obj := mk 1, property := δ₂_zero_comp_σ₂_one._proof_1 } ⟶ Z) : CategoryTheory.CategoryStruct.comp (δ₂ 2 δ₂_zero_comp_σ₂_one._proof_1 δ₂_zero_comp_σ₂_one._proof_2) (CategoryTheory.CategoryStruct.comp (σ₂ 1 δ₂_zero_comp_σ₂_one._proof_2 δ₂_zero_comp_σ₂_one._proof_1) h) = h

theorem SimplexCategory.Truncated.δ₂_two_comp_σ₂_zero : CategoryTheory.CategoryStruct.comp (δ₂ 2 δ₂_zero_comp_σ₂_one._proof_1 δ₂_zero_comp_σ₂_one._proof_2) (σ₂ 0 δ₂_zero_comp_σ₂_one._proof_2 δ₂_zero_comp_σ₂_one._proof_1) = CategoryTheory.CategoryStruct.comp (σ₂ 0 δ₂_zero_comp_σ₂_one._proof_3 δ₂_zero_comp_σ₂_one._proof_4) (δ₂ 1 δ₂_zero_comp_σ₂_one._proof_4 δ₂_zero_comp_σ₂_one._proof_3)

theorem SimplexCategory.Truncated.δ₂_two_comp_σ₂_zero_assoc {Z : CategoryTheory.ObjectProperty.FullSubcategory fun (a : SimplexCategory) => a.len ≤ 2} (h : { obj := mk 1, property := δ₂_zero_comp_σ₂_one._proof_1 } ⟶ Z) : CategoryTheory.CategoryStruct.comp (δ₂ 2 δ₂_zero_comp_σ₂_one._proof_1 δ₂_zero_comp_σ₂_one._proof_2) (CategoryTheory.CategoryStruct.comp (σ₂ 0 δ₂_zero_comp_σ₂_one._proof_2 δ₂_zero_comp_σ₂_one._proof_1) h) = CategoryTheory.CategoryStruct.comp (σ₂ 0 δ₂_zero_comp_σ₂_one._proof_3 δ₂_zero_comp_σ₂_one._proof_4) (CategoryTheory.CategoryStruct.comp (δ₂ 1 δ₂_zero_comp_σ₂_one._proof_4 δ₂_zero_comp_σ₂_one._proof_3) h)

theorem SimplexCategory.Truncated.δ₂_one_eq_const : δ₂ 1 δ₂_zero_comp_σ₂_one._proof_4 δ₂_zero_comp_σ₂_one._proof_3 = Hom.tr ((mk 0).const (mk (0 + 1)) 0) δ₂_zero_comp_σ₂_one._proof_4 δ₂_zero_comp_σ₂_one._proof_3

theorem SimplexCategory.Truncated.δ₂_zero_eq_const : δ₂ 0 δ₂_zero_comp_σ₂_one._proof_4 δ₂_zero_comp_σ₂_one._proof_3 = Hom.tr ((mk 0).const (mk (0 + 1)) 1) δ₂_zero_comp_σ₂_one._proof_4 δ₂_zero_comp_σ₂_one._proof_3

theorem SimplexCategory.Truncated.δ₂_zero_comp_δ₂_two : CategoryTheory.CategoryStruct.comp (δ₂ 0 δ₂_zero_comp_σ₂_one._proof_4 δ₂_zero_comp_σ₂_one._proof_3) (δ₂ 2 δ₂_zero_comp_σ₂_one._proof_3 δ₂_zero_comp_δ₂_two._proof_1) = CategoryTheory.CategoryStruct.comp (δ₂ 1 δ₂_zero_comp_σ₂_one._proof_4 δ₂_zero_comp_σ₂_one._proof_3) (δ₂ 0 δ₂_zero_comp_σ₂_one._proof_3 δ₂_zero_comp_δ₂_two._proof_1)

theorem SimplexCategory.Truncated.δ₂_zero_comp_δ₂_two_assoc {Z : CategoryTheory.ObjectProperty.FullSubcategory fun (a : SimplexCategory) => a.len ≤ 2} (h : { obj := mk (0 + 1 + 1), property := δ₂_zero_comp_δ₂_two._proof_1 } ⟶ Z) : CategoryTheory.CategoryStruct.comp (δ₂ 0 δ₂_zero_comp_σ₂_one._proof_4 δ₂_zero_comp_σ₂_one._proof_3) (CategoryTheory.CategoryStruct.comp (δ₂ 2 δ₂_zero_comp_σ₂_one._proof_3 δ₂_zero_comp_δ₂_two._proof_1) h) = CategoryTheory.CategoryStruct.comp (δ₂ 1 δ₂_zero_comp_σ₂_one._proof_4 δ₂_zero_comp_σ₂_one._proof_3) (CategoryTheory.CategoryStruct.comp (δ₂ 0 δ₂_zero_comp_σ₂_one._proof_3 δ₂_zero_comp_δ₂_two._proof_1) h)