Kernels and cokernels in owner interval categories

A thin slicing interval computes its kernels in the left adjacent abelian heart and its cokernels in the right adjacent abelian heart. The two-heart closure results ensure that these ambient objects remain in the interval; full faithfulness then transports the universal properties back.

theorem CategoryTheory.Triangulated.Slicing.intervalCat_hasKernel (C : Type u) [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [IsTriangulated C] {a b : ℝ} [Fact (a < b)] [Fact (b - a ≤ 1)] (s : Slicing C) {X Y : IntervalCat C s a b} (f : X ⟶ Y) : Limits.HasKernel f

A morphism in a thin owner interval has a kernel, computed in the left adjacent abelian heart.

instance CategoryTheory.Triangulated.Slicing.intervalCat_hasKernels (C : Type u) [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [IsTriangulated C] {a b : ℝ} [Fact (a < b)] [Fact (b - a ≤ 1)] (s : Slicing C) : Limits.HasKernels (IntervalCat C s a b)

Thin owner interval categories have all kernels.

theorem CategoryTheory.Triangulated.Slicing.intervalCat_hasCokernel (C : Type u) [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [IsTriangulated C] {a b : ℝ} [Fact (a < b)] [Fact (b - a ≤ 1)] (s : Slicing C) {X Y : IntervalCat C s a b} (f : X ⟶ Y) : Limits.HasCokernel f

A morphism in a thin owner interval has a cokernel, computed in the right adjacent abelian heart.

instance CategoryTheory.Triangulated.Slicing.intervalCat_hasCokernels (C : Type u) [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [IsTriangulated C] {a b : ℝ} [Fact (a < b)] [Fact (b - a ≤ 1)] (s : Slicing C) : Limits.HasCokernels (IntervalCat C s a b)

Thin owner interval categories have all cokernels.