Bridgeland Stability Conditions

7.3. IntervalCategory: QuasiAbelian🔗

7.3.1. LeftHeart🔗

The left ambient abelian heart \mathcal{P}((a, a+1]), defined as the heart of the t-structure induced by the slicing shifted by a.

Construction: The full subcategory of the heart of (s.phaseShift C a).toTStructure.

🔗def
CategoryTheory.Triangulated.Slicing.LeftHeart.{v, u} (C : Type u)
  [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive]
  [CategoryTheory.Pretriangulated C] [CategoryTheory.IsTriangulated C]
  (s : CategoryTheory.Triangulated.Slicing C) (a : ℝ) : Type u
CategoryTheory.Triangulated.Slicing.LeftHeart.{v,
    u}
  (C : Type u)
  [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C]
  [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ),
      (CategoryTheory.shiftFunctor C
          n).Additive]
  [CategoryTheory.Pretriangulated C]
  [CategoryTheory.IsTriangulated C]
  (s :
    CategoryTheory.Triangulated.Slicing C)
  (a : ℝ) : Type u

Something wrong, better idea? Suggest a change

7.3.2. RightHeart🔗

The right ambient abelian heart \mathcal{P}([b-1, b)), defined as the heart of the dual t-structure induced by the slicing shifted by b - 1.

Construction: The full subcategory of the heart of (s.phaseShift C (b - 1)).toTStructureGE.

🔗def
CategoryTheory.Triangulated.Slicing.RightHeart.{v, u} (C : Type u)
  [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive]
  [CategoryTheory.Pretriangulated C] [CategoryTheory.IsTriangulated C]
  (s : CategoryTheory.Triangulated.Slicing C) (b : ℝ) : Type u
CategoryTheory.Triangulated.Slicing.RightHeart.{v,
    u}
  (C : Type u)
  [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C]
  [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ),
      (CategoryTheory.shiftFunctor C
          n).Additive]
  [CategoryTheory.Pretriangulated C]
  [CategoryTheory.IsTriangulated C]
  (s :
    CategoryTheory.Triangulated.Slicing C)
  (b : ℝ) : Type u

Something wrong, better idea? Suggest a change

7.3.3. intervalCat_hasKernel🔗

Every morphism f : X \to Y in the thin interval category \mathcal{P}((a, b)) with b - a \le 1 has a kernel.

Proof: Embed into the left abelian heart \mathcal{P}((a, a+1]), compute the kernel there, and show the kernel object lies in \mathcal{P}((a, b)) via first_intervalProp_of_triangle. The key is that the abelian cokernel of \ker(f_H) \hookrightarrow X_H lives in the heart with \operatorname{leProp}(a+1), and \ker(f_H) has \operatorname{gtProp}(a) from heart membership, so the triangle test applies.

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

Something wrong, better idea? Suggest a change

7.3.4. intervalCat_hasKernels🔗

The thin interval category \mathcal{P}((a, b)) with a < b and b - a \le 1 has all kernels.

Proof: Immediate from intervalCat_hasKernel applied to each morphism.

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

Something wrong, better idea? Suggest a change

7.3.5. intervalCat_hasCokernel🔗

Every morphism f : X \to Y in the thin interval category \mathcal{P}((a, b)) with b - a \le 1 has a cokernel.

Proof: Embed into the right abelian heart \mathcal{P}([b-1, b)), compute the cokernel there, and show the cokernel object lies in \mathcal{P}((a, b)) via third_intervalProp_of_triangle. The right heart gives \operatorname{geProp}(b-1) on the kernel object and \operatorname{ltProp}(b) on the cokernel, enabling the triangle test.

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

Something wrong, better idea? Suggest a change

7.3.6. intervalCat_hasCokernels🔗

The thin interval category \mathcal{P}((a, b)) with a < b and b - a \le 1 has all cokernels.

Proof: Immediate from intervalCat_hasCokernel applied to each morphism.

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

Something wrong, better idea? Suggest a change

7.3.7. toRightHeartCokernelIso🔗

The cokernel of a morphism f in \mathcal{P}((a,b)), when embedded in the right heart \mathcal{P}([b-1, b)), is isomorphic to the cokernel of f computed directly in the right heart.

Construction: Constructs the isomorphism by comparing the cokernel in \mathcal{P}((a,b)) (which maps into the right heart) with the cokernel computed in the abelian right heart, using the universal property and the fact that both satisfy the same cocone condition.

🔗def
CategoryTheory.Triangulated.Slicing.IntervalCat.toRightHeartCokernelIso.{v,
    u}
  (C : Type u) [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive]
  [CategoryTheory.Pretriangulated C] [CategoryTheory.IsTriangulated C]
  {a b : ℝ} [Fact (a < b)] [Fact (b - a ≤ 1)]
  (s : CategoryTheory.Triangulated.Slicing C)
  {X Y : CategoryTheory.Triangulated.Slicing.IntervalCat C s a b}
  (f : X ⟶ Y) :
  let t :=
    CategoryTheory.Triangulated.Slicing.toTStructureGE C
      (CategoryTheory.Triangulated.Slicing.phaseShift C s (b - 1));
  have FR :=
    CategoryTheory.Triangulated.Slicing.IntervalCat.toRightHeart C s a b
      ⋯;
  FR.obj (CategoryTheory.Limits.cokernel f) ≅
    CategoryTheory.Limits.cokernel (FR.map f)
CategoryTheory.Triangulated.Slicing.IntervalCat.toRightHeartCokernelIso.{v,
    u}
  (C : Type u)
  [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C]
  [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ),
      (CategoryTheory.shiftFunctor C
          n).Additive]
  [CategoryTheory.Pretriangulated C]
  [CategoryTheory.IsTriangulated C]
  {a b : ℝ} [Fact (a < b)]
  [Fact (b - a ≤ 1)]
  (s :
    CategoryTheory.Triangulated.Slicing C)
  {X Y :
    CategoryTheory.Triangulated.Slicing.IntervalCat
      C s a b}
  (f : X ⟶ Y) :
  let t :=
    CategoryTheory.Triangulated.Slicing.toTStructureGE
      C
      (CategoryTheory.Triangulated.Slicing.phaseShift
        C s (b - 1));
  have FR :=
    CategoryTheory.Triangulated.Slicing.IntervalCat.toRightHeart
      C s a b ⋯;
  FR.obj
      (CategoryTheory.Limits.cokernel f) ≅
    CategoryTheory.Limits.cokernel
      (FR.map f)

Something wrong, better idea? Suggest a change

7.3.8. toRightHeartCokernelIso_π_comp_hom🔗

The cokernel projection in the right heart factors through toRightHeartCokernelIso: F_R(\operatorname{coker.\pi}(f)) \circ \mathrm{iso} = \operatorname{coker.\pi}(F_R(f)).

Proof: Unfolds the construction of toRightHeartCokernelIso and verifies the factoring by tracking the cokernel projection through the comparison isomorphism.

🔗theorem
CategoryTheory.Triangulated.Slicing.IntervalCat.toRightHeartCokernelIso_π_comp_hom.{v,
    u}
  (C : Type u) [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive]
  [CategoryTheory.Pretriangulated C] [CategoryTheory.IsTriangulated C]
  {a b : ℝ} [Fact (a < b)] [Fact (b - a ≤ 1)]
  (s : CategoryTheory.Triangulated.Slicing C)
  {X Y : CategoryTheory.Triangulated.Slicing.IntervalCat C s a b}
  (f : X ⟶ Y) :
  let t :=
    CategoryTheory.Triangulated.Slicing.toTStructureGE C
      (CategoryTheory.Triangulated.Slicing.phaseShift C s (b - 1));
  let FR :=
    CategoryTheory.Triangulated.Slicing.IntervalCat.toRightHeart C s a b
      ⋯;
  CategoryTheory.CategoryStruct.comp
      (FR.map (CategoryTheory.Limits.cokernel.π f))
      (CategoryTheory.Triangulated.Slicing.IntervalCat.toRightHeartCokernelIso
          C s f).hom =
    CategoryTheory.Limits.cokernel.π (FR.map f)
CategoryTheory.Triangulated.Slicing.IntervalCat.toRightHeartCokernelIso_π_comp_hom.{v,
    u}
  (C : Type u)
  [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C]
  [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ),
      (CategoryTheory.shiftFunctor C
          n).Additive]
  [CategoryTheory.Pretriangulated C]
  [CategoryTheory.IsTriangulated C]
  {a b : ℝ} [Fact (a < b)]
  [Fact (b - a ≤ 1)]
  (s :
    CategoryTheory.Triangulated.Slicing C)
  {X Y :
    CategoryTheory.Triangulated.Slicing.IntervalCat
      C s a b}
  (f : X ⟶ Y) :
  let t :=
    CategoryTheory.Triangulated.Slicing.toTStructureGE
      C
      (CategoryTheory.Triangulated.Slicing.phaseShift
        C s (b - 1));
  let FR :=
    CategoryTheory.Triangulated.Slicing.IntervalCat.toRightHeart
      C s a b ⋯;
  CategoryTheory.CategoryStruct.comp
      (FR.map
        (CategoryTheory.Limits.cokernel.π
          f))
      (CategoryTheory.Triangulated.Slicing.IntervalCat.toRightHeartCokernelIso
          C s f).hom =
    CategoryTheory.Limits.cokernel.π
      (FR.map f)

Something wrong, better idea? Suggest a change

7.3.9. epi_toRightHeart_of_strictEpi🔗

A strict epimorphism g in \mathcal{P}((a, b)) becomes an epimorphism in the right heart \mathcal{P}([b-1, b)).

Proof: Analogous to epi_toLeftHeart_of_strictEpi but using the right heart. The cokernel of \ker(g) in the right heart is computed via a distinguished triangle from the abelian heart structure, and the resulting cokernel comparison shows g maps to an epimorphism.

🔗theorem
CategoryTheory.Triangulated.Slicing.IntervalCat.epi_toRightHeart_of_strictEpi.{v,
    u}
  (C : Type u) [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive]
  [CategoryTheory.Pretriangulated C] [CategoryTheory.IsTriangulated C]
  {a b : ℝ} [Fact (a < b)] [Fact (b - a ≤ 1)]
  (s : CategoryTheory.Triangulated.Slicing C)
  {X Y : CategoryTheory.Triangulated.Slicing.IntervalCat C s a b}
  (g : X ⟶ Y) (hg : CategoryTheory.IsStrictEpi g) :
  CategoryTheory.Epi
    ((CategoryTheory.Triangulated.Slicing.IntervalCat.toRightHeart C s a
          b ⋯).map
      g)
CategoryTheory.Triangulated.Slicing.IntervalCat.epi_toRightHeart_of_strictEpi.{v,
    u}
  (C : Type u)
  [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C]
  [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ),
      (CategoryTheory.shiftFunctor C
          n).Additive]
  [CategoryTheory.Pretriangulated C]
  [CategoryTheory.IsTriangulated C]
  {a b : ℝ} [Fact (a < b)]
  [Fact (b - a ≤ 1)]
  (s :
    CategoryTheory.Triangulated.Slicing C)
  {X Y :
    CategoryTheory.Triangulated.Slicing.IntervalCat
      C s a b}
  (g : X ⟶ Y)
  (hg : CategoryTheory.IsStrictEpi g) :
  CategoryTheory.Epi
    ((CategoryTheory.Triangulated.Slicing.IntervalCat.toRightHeart
          C s a b ⋯).map
      g)

Something wrong, better idea? Suggest a change

7.3.10. mono_toLeftHeart_of_strictMono🔗

A strict monomorphism f in \mathcal{P}((a, b)) becomes a monomorphism in the left heart \mathcal{P}((a, a+1]).

Proof: Analogous to mono_toRightHeart_of_strictMono but using the left heart. The kernel of \operatorname{coker}(f) \circ \operatorname{coker.\pi} in the left heart is computed, and the resulting kernel comparison shows f maps to a monomorphism.

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

Something wrong, better idea? Suggest a change