Bridgeland Stability Conditions

7.4. IntervalCategory: Strictness🔗

7.4.1. mono_toRightHeart_of_strictMono🔗

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

Proof: From the strict mono structure, f is a kernel of \operatorname{coker}(f). The right heart embedding preserves this kernel via toRightHeartCokernelIso. The abelian image factorization in the right heart shows f maps to a monomorphism: the image-kernel comparison is an isomorphism, and the epimorphic factor-through-image composed with it gives a mono-epi factorization.

🔗theorem
CategoryTheory.Triangulated.Slicing.IntervalCat.mono_toRightHeart_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.toRightHeart C s a
          b ⋯).map
      f)
CategoryTheory.Triangulated.Slicing.IntervalCat.mono_toRightHeart_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.toRightHeart
          C s a b ⋯).map
      f)

Something wrong, better idea? Suggest a change

7.4.2. strictMono_of_mono_toRightHeart🔗

If a morphism f in \mathcal{P}((a, b)) becomes a monomorphism in the right heart \mathcal{P}([b-1, b)), then f is a strict monomorphism in \mathcal{P}((a, b)).

Proof: In the abelian right heart, mono implies kernel-of-cokernel. The cokernel comparison isomorphism toRightHeartCokernelIso transforms this into a kernel fork for \operatorname{coker}(f) in \mathcal{P}((a,b)). Reflecting the limit through the faithful functor yields strictness.

🔗theorem
CategoryTheory.Triangulated.Slicing.IntervalCat.strictMono_of_mono_toRightHeart.{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.Mono
      ((CategoryTheory.Triangulated.Slicing.IntervalCat.toRightHeart C s
            a b ⋯).map
        f)] :
  CategoryTheory.IsStrictMono f
CategoryTheory.Triangulated.Slicing.IntervalCat.strictMono_of_mono_toRightHeart.{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.Mono
      ((CategoryTheory.Triangulated.Slicing.IntervalCat.toRightHeart
            C s a b ⋯).map
        f)] :
  CategoryTheory.IsStrictMono f

Something wrong, better idea? Suggest a change

7.4.3. toLeftHeartKernelIso🔗

The kernel of a morphism f in \mathcal{P}((a,b)), when embedded in the left heart \mathcal{P}((a, a+1]), is isomorphic to the kernel of f computed directly in the left heart.

Construction: Constructs the isomorphism by comparing the kernel in \mathcal{P}((a,b)) (which maps into the left heart) with the kernel computed in the abelian left heart, using the universal property of kernels and the fact that both represent the same limit cone.

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

Something wrong, better idea? Suggest a change

7.4.4. toLeftHeartKernelIso_hom_comp_ι🔗

The kernel inclusion in the left heart factors through toLeftHeartKernelIso: \mathrm{iso} \circ \ker.\iota(F_L(f)) = F_L(\ker.\iota(f)).

Proof: Unfolds the construction of toLeftHeartKernelIso and verifies the factoring by tracking the kernel inclusion through the comparison isomorphism.

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

Something wrong, better idea? Suggest a change

7.4.5. epi_toLeftHeart_of_strictEpi🔗

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

Proof: From the strict epi structure, g is a cokernel of \ker(g). The left heart kernel isomorphism toLeftHeartKernelIso allows comparison of the cokernel in \mathcal{P}((a,b)) with the abelian coimage in the left heart. The resulting factorization through the cokernel of the kernel inclusion is shown to be an epimorphism.

🔗theorem
CategoryTheory.Triangulated.Slicing.IntervalCat.epi_toLeftHeart_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.toLeftHeart C s a
          b ⋯).map
      g)
CategoryTheory.Triangulated.Slicing.IntervalCat.epi_toLeftHeart_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.toLeftHeart
          C s a b ⋯).map
      g)

Something wrong, better idea? Suggest a change

7.4.6. strictEpi_of_epi_toLeftHeart🔗

If a morphism g in \mathcal{P}((a, b)) becomes an epimorphism in the left heart \mathcal{P}((a, a+1]), then g is a strict epimorphism in \mathcal{P}((a, b)).

Proof: In the abelian left heart, epi implies cokernel-of-kernel. The kernel comparison isomorphism toLeftHeartKernelIso transforms this into a cokernel cofork for \ker(g) in \mathcal{P}((a,b)). Reflecting the colimit through the faithful functor yields strictness.

🔗theorem
CategoryTheory.Triangulated.Slicing.IntervalCat.strictEpi_of_epi_toLeftHeart.{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)
  [CategoryTheory.Epi
      ((CategoryTheory.Triangulated.Slicing.IntervalCat.toLeftHeart C s
            a b ⋯).map
        g)] :
  CategoryTheory.IsStrictEpi g
CategoryTheory.Triangulated.Slicing.IntervalCat.strictEpi_of_epi_toLeftHeart.{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)
  [CategoryTheory.Epi
      ((CategoryTheory.Triangulated.Slicing.IntervalCat.toLeftHeart
            C s a b ⋯).map
        g)] :
  CategoryTheory.IsStrictEpi g

Something wrong, better idea? Suggest a change