Comparison isomorphisms for owner interval limits

The canonical kernel and cokernel selected in a thin interval agree with the objects computed in the corresponding adjacent abelian hearts. These comparison isomorphisms are the bridge from the preabelian existence layer to strictness and quasi-abelianity.

noncomputable def CategoryTheory.Triangulated.Slicing.IntervalCat.toLeftHeartKernelIso (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) : let t := toTStructure C (phaseShift C s a); have FL := toLeftHeart C s a b ⋯; FL.obj (Limits.kernel f) ≅ Limits.kernel (FL.map f)

The canonical interval kernel agrees with the kernel computed in the left adjacent abelian heart.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def CategoryTheory.Triangulated.Slicing.IntervalCat.toRightHeartCokernelIso (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) : let t := toDualTStructure C (phaseShift C s (b - 1)); have FR := toRightHeart C s a b ⋯; FR.obj (Limits.cokernel f) ≅ Limits.cokernel (FR.map f)

The canonical interval cokernel agrees with the cokernel computed in the right adjacent abelian heart.

Equations

• One or more equations did not get rendered due to their size.

theorem CategoryTheory.Triangulated.Slicing.IntervalCat.toLeftHeartKernelIso_hom_comp_ι (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) : let t := toTStructure C (phaseShift C s a); let FL := toLeftHeart C s a b ⋯; CategoryStruct.comp (toLeftHeartKernelIso C s f).hom (Limits.kernel.ι (FL.map f)) = FL.map (Limits.kernel.ι f)

The left-heart kernel comparison commutes with the canonical kernel inclusions.

theorem CategoryTheory.Triangulated.Slicing.IntervalCat.toRightHeartCokernelIso_π_comp_hom (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) : let t := toDualTStructure C (phaseShift C s (b - 1)); let FR := toRightHeart C s a b ⋯; CategoryStruct.comp (FR.map (Limits.cokernel.π f)) (toRightHeartCokernelIso C s f).hom = Limits.cokernel.π (FR.map f)

The right-heart cokernel comparison commutes with the canonical cokernel projections.