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_reducible]

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

Equations

• SimplexCategory.Truncated.instDecidableEqHom a b = decidable_of_iff (SimplexCategory.Hom.toOrderHom a.hom = SimplexCategory.Hom.toOrderHom b.hom) ⋯

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 ⋯).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 : { len := n }.len ≤ m := by decide) (hn' : { len := n + 1 }.len ≤ m := by decide) : { obj := { len := n }, property := hn } ⟶ { obj := { len := n + 1 }, property := hn' }

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

Equations

• SimplexCategory.Truncated.δ m i hn hn' = SimplexCategory.Truncated.Hom.tr (SimplexCategory.δ i) hn hn'

@[reducible, inline]

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

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

Equations

• SimplexCategory.Truncated.σ m i hn hn' = SimplexCategory.Truncated.Hom.tr (SimplexCategory.σ i) hn hn'

@[reducible, inline]

abbrev SimplexCategory.Truncated.δ₂ {n : ℕ} (i : Fin (n + 2)) (hn : { len := n }.len ≤ 2 := by decide) (hn' : { len := n + 1 }.len ≤ 2 := by decide) : { obj := { len := n }, property := hn } ⟶ { obj := { len := 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 : { len := n + 1 }.len ≤ 2 := by decide) (hn' : { len := n }.len ≤ 2 := by decide) : { obj := { len := n + 1 }, property := hn } ⟶ { obj := { len := 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 : { len := n }.len ≤ 2 := by decide) (hn' : { len := n + 1 }.len ≤ 2 := by decide) : CategoryTheory.CategoryStruct.comp (δ₂ 0 hn hn') (σ₂ 0 hn' hn) = CategoryTheory.CategoryStruct.id { obj := { len := n }, property := hn }

@[simp]

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

@[simp]

theorem SimplexCategory.Truncated.δ₂_one_comp_σ₂_zero_assoc {n : ℕ} (hn : { len := n }.len ≤ 2 := by decide) (hn' : { len := n + 1 }.len ≤ 2 := by decide) {Z : CategoryTheory.ObjectProperty.FullSubcategory fun (a : SimplexCategory) => a.len ≤ 2} (h : { obj := { len := 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 : { len := n + 1 }.len ≤ 2 := by decide) (hn' : { len := n + 1 + 1 }.len ≤ 2 := by decide) : CategoryTheory.CategoryStruct.comp (δ₂ 1 hn hn') (σ₂ 1 hn' hn) = CategoryTheory.CategoryStruct.id { obj := { len := n + 1 }, property := hn }

@[simp]

theorem SimplexCategory.Truncated.δ₂_one_comp_σ₂_one_assoc {n : ℕ} (hn : { len := n + 1 }.len ≤ 2 := by decide) (hn' : { len := n + 1 + 1 }.len ≤ 2 := by decide) {Z : CategoryTheory.ObjectProperty.FullSubcategory fun (a : SimplexCategory) => a.len ≤ 2} (h : { obj := { len := 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 := { len := 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 := { len := 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 := { len := 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 ({ len := 0 }.const { len := 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 ({ len := 0 }.const { len := 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 := { len := 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)

theorem SimplexCategory.Truncated.mono_iff {d : ℕ} {a b : Truncated d} {f : a ⟶ b} : CategoryTheory.Mono f ↔ CategoryTheory.Mono f.hom

A morphism in Truncated d is a monomorphism if and only if it is a monomorphism in SimplexCategory.

theorem SimplexCategory.Truncated.epi_iff {d : ℕ} {a b : Truncated d} {f : a ⟶ b} : CategoryTheory.Epi f ↔ CategoryTheory.Epi f.hom

A morphism in Truncated d is an epimorphism if and only if it is an epimorphism in SimplexCategory.

instance SimplexCategory.Truncated.instSplitEpiCategory {d : ℕ} : CategoryTheory.SplitEpiCategory (Truncated d)

instance SimplexCategory.Truncated.instEpiFullSubcategoryLeNatLenHomMk {d : ℕ} {a b : Truncated d} (g : a.obj ⟶ b.obj) [hg : CategoryTheory.Epi g] : CategoryTheory.Epi (CategoryTheory.ObjectProperty.homMk g)

instance SimplexCategory.Truncated.instMonoFullSubcategoryLeNatLenHomMk {d : ℕ} {a b : Truncated d} (g : a.obj ⟶ b.obj) [hg : CategoryTheory.Mono g] : CategoryTheory.Mono (CategoryTheory.ObjectProperty.homMk g)

instance SimplexCategory.Truncated.instStrongEpiCategory {d : ℕ} : CategoryTheory.StrongEpiCategory (Truncated d)

instance SimplexCategory.Truncated.instHasStrongEpiMonoFactorisations {d : ℕ} : CategoryTheory.Limits.HasStrongEpiMonoFactorisations (Truncated d)