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.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.

Equations

• SimplexCategory.Truncated.δ m i hn hn' = SimplexCategory.δ i

@[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.

Equations

• SimplexCategory.Truncated.σ m i hn hn' = SimplexCategory.σ i

@[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.

Equations

• SimplexCategory.Truncated.δ₂ i hn hn' = SimplexCategory.Truncated.δ 2 i hn hn'

@[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.

Equations

• SimplexCategory.Truncated.σ₂ i hn hn' = SimplexCategory.Truncated.σ 2 i hn hn'

@[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 ⋯ ⋯) (σ₂ 1 ⋯ ⋯) = CategoryTheory.CategoryStruct.comp (σ₂ 0 ⋯ ⋯) (δ₂ 0 ⋯ ⋯)

theorem SimplexCategory.Truncated.δ₂_zero_comp_σ₂_one_assoc {Z : CategoryTheory.ObjectProperty.FullSubcategory fun (a : SimplexCategory) => a.len ≤ 2} (h : { obj := mk 1, property := ⋯ } ⟶ Z) : CategoryTheory.CategoryStruct.comp (δ₂ 0 ⋯ ⋯) (CategoryTheory.CategoryStruct.comp (σ₂ 1 ⋯ ⋯) h) = CategoryTheory.CategoryStruct.comp (σ₂ 0 ⋯ ⋯) (CategoryTheory.CategoryStruct.comp (δ₂ 0 ⋯ ⋯) 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.δ₂_two_comp_σ₂_one : CategoryTheory.CategoryStruct.comp (δ₂ 2 ⋯ ⋯) (σ₂ 1 ⋯ ⋯) = CategoryTheory.CategoryStruct.id { obj := mk 1, property := ⋯ }

@[simp]

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

theorem SimplexCategory.Truncated.δ₂_two_comp_σ₂_zero : CategoryTheory.CategoryStruct.comp (δ₂ 2 ⋯ ⋯) (σ₂ 0 ⋯ ⋯) = CategoryTheory.CategoryStruct.comp (σ₂ 0 ⋯ ⋯) (δ₂ 1 ⋯ ⋯)

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