Bridgeland Stability Conditions

7.5. IntervalCategory: TwoHeartEmbedding🔗

7.5.1. gtProp_of_intervalProp🔗

If all HN phases of E lie in (a, b), then \phi^-(E) > a, i.e. E satisfies \operatorname{gtProp}(a).

Proof: The bottom HN factor has phase > a by the interval membership condition, and the zero case is trivial.

🔗theorem
CategoryTheory.Triangulated.Slicing.gtProp_of_intervalProp.{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]
  (s : CategoryTheory.Triangulated.Slicing C) {a b : ℝ} {E : C}
  (hE : CategoryTheory.Triangulated.Slicing.intervalProp C s a b E) :
  CategoryTheory.Triangulated.Slicing.gtProp C s a E
CategoryTheory.Triangulated.Slicing.gtProp_of_intervalProp.{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]
  (s :
    CategoryTheory.Triangulated.Slicing C)
  {a b : ℝ} {E : C}
  (hE :
    CategoryTheory.Triangulated.Slicing.intervalProp
      C s a b E) :
  CategoryTheory.Triangulated.Slicing.gtProp
    C s a E

Something wrong, better idea? Suggest a change

7.5.2. leProp_of_intervalProp🔗

If all HN phases of E lie in (a, b), then \phi^+(E) \le b, i.e. E satisfies \operatorname{leProp}(b).

Proof: The top HN factor has phase < b \le b by the interval membership condition.

🔗theorem
CategoryTheory.Triangulated.Slicing.leProp_of_intervalProp.{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]
  (s : CategoryTheory.Triangulated.Slicing C) {a b : ℝ} {E : C}
  (hE : CategoryTheory.Triangulated.Slicing.intervalProp C s a b E) :
  CategoryTheory.Triangulated.Slicing.leProp C s b E
CategoryTheory.Triangulated.Slicing.leProp_of_intervalProp.{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]
  (s :
    CategoryTheory.Triangulated.Slicing C)
  {a b : ℝ} {E : C}
  (hE :
    CategoryTheory.Triangulated.Slicing.intervalProp
      C s a b E) :
  CategoryTheory.Triangulated.Slicing.leProp
    C s b E

Something wrong, better idea? Suggest a change

7.5.3. intervalProp_implies_leftHeart🔗

Left heart containment (Lemma 4.3a). If b - a \le 1 and E \in \mathcal{P}((a, b)), then E lies in the heart of the t-structure induced by the slicing shifted by a. This heart is the half-open interval \mathcal{P}((a, a+1]).

Proof: Phases in (a, b) satisfy > a (giving \operatorname{gtProp}(0) after shifting) and < b \le a + 1 (giving \operatorname{leProp}(1) after shifting). These are exactly the heart membership conditions for the shifted t-structure.

🔗theorem
CategoryTheory.Triangulated.Slicing.intervalProp_implies_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 b : ℝ}
  (hab : b - a ≤ 1) {E : C}
  (hE : CategoryTheory.Triangulated.Slicing.intervalProp C s a b E) :
  (CategoryTheory.Triangulated.Slicing.toTStructure C
        (CategoryTheory.Triangulated.Slicing.phaseShift C s a)).heart
    E
CategoryTheory.Triangulated.Slicing.intervalProp_implies_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 b : ℝ} (hab : b - a ≤ 1) {E : C}
  (hE :
    CategoryTheory.Triangulated.Slicing.intervalProp
      C s a b E) :
  (CategoryTheory.Triangulated.Slicing.toTStructure
        C
        (CategoryTheory.Triangulated.Slicing.phaseShift
          C s a)).heart
    E

Something wrong, better idea? Suggest a change

7.5.4. intervalProp_implies_rightHeart🔗

Right heart containment (Lemma 4.3b). If b - a \le 1 and E \in \mathcal{P}((a, b)), then E lies in the heart of the dual t-structure induced by the slicing shifted by b - 1. This heart is the half-open interval \mathcal{P}([b-1, b)).

Proof: Phases in (a, b) satisfy \ge b - 1 (since a \le b - 1 when b - a \le 1, and all phases are > a) and < b (directly from the interval condition). Together with left heart containment, this establishes the two-heart embedding: every object in a thin interval lies in both an abelian heart controlling kernels and one controlling cokernels.

🔗theorem
CategoryTheory.Triangulated.Slicing.intervalProp_implies_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) {a b : ℝ}
  (hab : b - a ≤ 1) {E : C}
  (hE : CategoryTheory.Triangulated.Slicing.intervalProp C s a b E) :
  (CategoryTheory.Triangulated.Slicing.toTStructureGE C
        (CategoryTheory.Triangulated.Slicing.phaseShift C s
          (b - 1))).heart
    E
CategoryTheory.Triangulated.Slicing.intervalProp_implies_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)
  {a b : ℝ} (hab : b - a ≤ 1) {E : C}
  (hE :
    CategoryTheory.Triangulated.Slicing.intervalProp
      C s a b E) :
  (CategoryTheory.Triangulated.Slicing.toTStructureGE
        C
        (CategoryTheory.Triangulated.Slicing.phaseShift
          C s (b - 1))).heart
    E

Something wrong, better idea? Suggest a change

7.5.5. toLeftHeart🔗

The fully faithful embedding \mathcal{P}((a,b)) \hookrightarrow \mathcal{P}((a, a+1]) into the left abelian heart.

Construction: Maps objects by packaging the left-heart membership proof from intervalProp_implies_leftHeart, and maps morphisms by unwrapping to the underlying hom in \mathcal{C}.

🔗def
CategoryTheory.Triangulated.Slicing.IntervalCat.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]
  (s : CategoryTheory.Triangulated.Slicing C) (a b : ℝ)
  (hab : b - a ≤ 1) :
  CategoryTheory.Functor
    (CategoryTheory.Triangulated.Slicing.IntervalCat C s a b)
    (CategoryTheory.Triangulated.Slicing.toTStructure C
          (CategoryTheory.Triangulated.Slicing.phaseShift C s
            a)).heart.FullSubcategory
CategoryTheory.Triangulated.Slicing.IntervalCat.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]
  (s :
    CategoryTheory.Triangulated.Slicing C)
  (a b : ℝ) (hab : b - a ≤ 1) :
  CategoryTheory.Functor
    (CategoryTheory.Triangulated.Slicing.IntervalCat
      C s a b)
    (CategoryTheory.Triangulated.Slicing.toTStructure
          C
          (CategoryTheory.Triangulated.Slicing.phaseShift
            C s a)).heart.FullSubcategory

Something wrong, better idea? Suggest a change

7.5.6. toLeftHeart_full🔗

The left heart embedding \mathcal{P}((a,b)) \to \mathcal{P}((a, a+1]) is full.

Proof: Every morphism in the heart between objects from \mathcal{P}((a,b)) is already a morphism in \mathcal{C} between those objects.

🔗theorem
CategoryTheory.Triangulated.Slicing.IntervalCat.toLeftHeart_full.{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 b : ℝ)
  (hab : b - a ≤ 1) :
  (CategoryTheory.Triangulated.Slicing.IntervalCat.toLeftHeart C s a b
      hab).Full
CategoryTheory.Triangulated.Slicing.IntervalCat.toLeftHeart_full.{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 b : ℝ) (hab : b - a ≤ 1) :
  (CategoryTheory.Triangulated.Slicing.IntervalCat.toLeftHeart
      C s a b hab).Full

Something wrong, better idea? Suggest a change

7.5.7. toLeftHeart_faithful🔗

The left heart embedding \mathcal{P}((a,b)) \to \mathcal{P}((a, a+1]) is faithful.

Proof: Injectivity on hom-sets is immediate since the functor acts as the identity on underlying morphisms.

🔗theorem
CategoryTheory.Triangulated.Slicing.IntervalCat.toLeftHeart_faithful.{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 b : ℝ)
  (hab : b - a ≤ 1) :
  (CategoryTheory.Triangulated.Slicing.IntervalCat.toLeftHeart C s a b
      hab).Faithful
CategoryTheory.Triangulated.Slicing.IntervalCat.toLeftHeart_faithful.{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 b : ℝ) (hab : b - a ≤ 1) :
  (CategoryTheory.Triangulated.Slicing.IntervalCat.toLeftHeart
      C s a b hab).Faithful

Something wrong, better idea? Suggest a change

7.5.8. toRightHeart🔗

The fully faithful embedding \mathcal{P}((a,b)) \hookrightarrow \mathcal{P}([b-1, b)) into the right abelian heart.

Construction: Maps objects by packaging the right-heart membership proof from intervalProp_implies_rightHeart, and maps morphisms by unwrapping to the underlying hom in \mathcal{C}.

🔗def
CategoryTheory.Triangulated.Slicing.IntervalCat.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]
  (s : CategoryTheory.Triangulated.Slicing C) (a b : ℝ)
  (hab : b - a ≤ 1) :
  CategoryTheory.Functor
    (CategoryTheory.Triangulated.Slicing.IntervalCat C s a b)
    (CategoryTheory.Triangulated.Slicing.toTStructureGE C
          (CategoryTheory.Triangulated.Slicing.phaseShift C s
            (b - 1))).heart.FullSubcategory
CategoryTheory.Triangulated.Slicing.IntervalCat.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]
  (s :
    CategoryTheory.Triangulated.Slicing C)
  (a b : ℝ) (hab : b - a ≤ 1) :
  CategoryTheory.Functor
    (CategoryTheory.Triangulated.Slicing.IntervalCat
      C s a b)
    (CategoryTheory.Triangulated.Slicing.toTStructureGE
          C
          (CategoryTheory.Triangulated.Slicing.phaseShift
            C s
            (b -
              1))).heart.FullSubcategory

Something wrong, better idea? Suggest a change

7.5.9. toRightHeart_full🔗

The right heart embedding \mathcal{P}((a,b)) \to \mathcal{P}([b-1, b)) is full.

Proof: Every morphism in the heart between objects from \mathcal{P}((a,b)) is already a morphism in \mathcal{C} between those objects.

🔗theorem
CategoryTheory.Triangulated.Slicing.IntervalCat.toRightHeart_full.{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 b : ℝ)
  (hab : b - a ≤ 1) :
  (CategoryTheory.Triangulated.Slicing.IntervalCat.toRightHeart C s a b
      hab).Full
CategoryTheory.Triangulated.Slicing.IntervalCat.toRightHeart_full.{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 b : ℝ) (hab : b - a ≤ 1) :
  (CategoryTheory.Triangulated.Slicing.IntervalCat.toRightHeart
      C s a b hab).Full

Something wrong, better idea? Suggest a change

7.5.10. toRightHeart_faithful🔗

The right heart embedding \mathcal{P}((a,b)) \to \mathcal{P}([b-1, b)) is faithful.

Proof: Injectivity on hom-sets is immediate since the functor acts as the identity on underlying morphisms.

🔗theorem
CategoryTheory.Triangulated.Slicing.IntervalCat.toRightHeart_faithful.{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 b : ℝ)
  (hab : b - a ≤ 1) :
  (CategoryTheory.Triangulated.Slicing.IntervalCat.toRightHeart C s a b
      hab).Faithful
CategoryTheory.Triangulated.Slicing.IntervalCat.toRightHeart_faithful.{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 b : ℝ) (hab : b - a ≤ 1) :
  (CategoryTheory.Triangulated.Slicing.IntervalCat.toRightHeart
      C s a b hab).Faithful

Something wrong, better idea? Suggest a change

7.5.11. intervalProp_implies_rightWindow🔗

If b - a \le 1 and E \in \mathcal{P}((a, b)), then E satisfies the phase-window conditions \operatorname{geProp}(b - 1) and \operatorname{ltProp}(b), placing it in the half-open interval [b-1, b).

Proof: The \operatorname{geProp}(b-1) bound follows from \operatorname{gtProp}(a) and a \ge b - 1. The \operatorname{ltProp}(b) bound is direct from interval membership.

🔗theorem
CategoryTheory.Triangulated.Slicing.intervalProp_implies_rightWindow.{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]
  (s : CategoryTheory.Triangulated.Slicing C) {a b : ℝ}
  (hab : b - a ≤ 1) {E : C}
  (hE : CategoryTheory.Triangulated.Slicing.intervalProp C s a b E) :
  CategoryTheory.Triangulated.Slicing.geProp C s (b - 1) E ∧
    CategoryTheory.Triangulated.Slicing.ltProp C s b E
CategoryTheory.Triangulated.Slicing.intervalProp_implies_rightWindow.{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]
  (s :
    CategoryTheory.Triangulated.Slicing C)
  {a b : ℝ} (hab : b - a ≤ 1) {E : C}
  (hE :
    CategoryTheory.Triangulated.Slicing.intervalProp
      C s a b E) :
  CategoryTheory.Triangulated.Slicing.geProp
      C s (b - 1) E ∧
    CategoryTheory.Triangulated.Slicing.ltProp
      C s b E

Something wrong, better idea? Suggest a change

7.5.12. phiPlus_le_of_semistable_triangle🔗

Phase upper bound from Lemma 3.4. In a distinguished triangle K \to F \to Q \to K[1] with F \in \mathcal{P}(\phi) semistable and K, Q \in \mathcal{P}((a, b)) with b \le a + 1 and \phi \in (a, b), if K is nonzero then \phi^+(K) \le \phi.

Proof: Since F is semistable, \phi^+(F) = \phi. The result then follows from the general triangle phase bound phiPlus_triangle_le.

🔗theorem
CategoryTheory.Triangulated.Slicing.phiPlus_le_of_semistable_triangle.{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]
  (s : CategoryTheory.Triangulated.Slicing C) {φ : ℝ} {K F Q : C}
  {f₁ : K ⟶ F} {f₂ : F ⟶ Q}
  {f₃ : Q ⟶ (CategoryTheory.shiftFunctor C 1).obj K}
  (hT :
    CategoryTheory.Pretriangulated.Triangle.mk f₁ f₂ f₃ ∈
      CategoryTheory.Pretriangulated.distinguishedTriangles)
  (hPφ : s.P φ F) (hFne : ¬CategoryTheory.Limits.IsZero F)
  (hKne : ¬CategoryTheory.Limits.IsZero K) {a b : ℝ} (hab : b ≤ a + 1)
  (hKI : CategoryTheory.Triangulated.Slicing.intervalProp C s a b K)
  (hQI : CategoryTheory.Triangulated.Slicing.intervalProp C s a b Q) :
  CategoryTheory.Triangulated.Slicing.phiPlus C s K hKne ≤ φ
CategoryTheory.Triangulated.Slicing.phiPlus_le_of_semistable_triangle.{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]
  (s :
    CategoryTheory.Triangulated.Slicing C)
  {φ : ℝ} {K F Q : C} {f₁ : K ⟶ F}
  {f₂ : F ⟶ Q}
  {f₃ :
    Q ⟶
      (CategoryTheory.shiftFunctor C
            1).obj
        K}
  (hT :
    CategoryTheory.Pretriangulated.Triangle.mk
        f₁ f₂ f₃ ∈
      CategoryTheory.Pretriangulated.distinguishedTriangles)
  (hPφ : s.P φ F)
  (hFne : ¬CategoryTheory.Limits.IsZero F)
  (hKne : ¬CategoryTheory.Limits.IsZero K)
  {a b : ℝ} (hab : b ≤ a + 1)
  (hKI :
    CategoryTheory.Triangulated.Slicing.intervalProp
      C s a b K)
  (hQI :
    CategoryTheory.Triangulated.Slicing.intervalProp
      C s a b Q) :
  CategoryTheory.Triangulated.Slicing.phiPlus
      C s K hKne ≤
    φ

Something wrong, better idea? Suggest a change

7.5.13. phiMinus_ge_of_semistable_triangle🔗

Phase lower bound from Lemma 3.4. In a distinguished triangle K \to F \to Q \to K[1] with F \in \mathcal{P}(\phi) semistable and K, Q \in \mathcal{P}((a, b)) with b \le a + 1, if Q is nonzero then \phi \le \phi^-(Q).

Proof: Since F is semistable, \phi^-(F) = \phi. The result then follows from the general triangle phase bound phiMinus_triangle_le.

🔗theorem
CategoryTheory.Triangulated.Slicing.phiMinus_ge_of_semistable_triangle.{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]
  (s : CategoryTheory.Triangulated.Slicing C) {φ : ℝ} {K F Q : C}
  {f₁ : K ⟶ F} {f₂ : F ⟶ Q}
  {f₃ : Q ⟶ (CategoryTheory.shiftFunctor C 1).obj K}
  (hT :
    CategoryTheory.Pretriangulated.Triangle.mk f₁ f₂ f₃ ∈
      CategoryTheory.Pretriangulated.distinguishedTriangles)
  (hPφ : s.P φ F) (hFne : ¬CategoryTheory.Limits.IsZero F)
  (hQne : ¬CategoryTheory.Limits.IsZero Q) {a b : ℝ} (hab : b ≤ a + 1)
  (hKI : CategoryTheory.Triangulated.Slicing.intervalProp C s a b K)
  (hQI : CategoryTheory.Triangulated.Slicing.intervalProp C s a b Q) :
  φ ≤ CategoryTheory.Triangulated.Slicing.phiMinus C s Q hQne
CategoryTheory.Triangulated.Slicing.phiMinus_ge_of_semistable_triangle.{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]
  (s :
    CategoryTheory.Triangulated.Slicing C)
  {φ : ℝ} {K F Q : C} {f₁ : K ⟶ F}
  {f₂ : F ⟶ Q}
  {f₃ :
    Q ⟶
      (CategoryTheory.shiftFunctor C
            1).obj
        K}
  (hT :
    CategoryTheory.Pretriangulated.Triangle.mk
        f₁ f₂ f₃ ∈
      CategoryTheory.Pretriangulated.distinguishedTriangles)
  (hPφ : s.P φ F)
  (hFne : ¬CategoryTheory.Limits.IsZero F)
  (hQne : ¬CategoryTheory.Limits.IsZero Q)
  {a b : ℝ} (hab : b ≤ a + 1)
  (hKI :
    CategoryTheory.Triangulated.Slicing.intervalProp
      C s a b K)
  (hQI :
    CategoryTheory.Triangulated.Slicing.intervalProp
      C s a b Q) :
  φ ≤
    CategoryTheory.Triangulated.Slicing.phiMinus
      C s Q hQne

Something wrong, better idea? Suggest a change

7.5.14. phiPlus_lt_of_triangle_with_leProp🔗

Phase upper bound from one-sided containment. In a triangle K \to E \to Q \to K[1], if \phi^+(E) < b and Q satisfies \operatorname{leProp}(c) with c < b + 1, then if K is nonzero, \phi^+(K) < b.

Proof: By contradiction: if the top HN factor of K has phase \ge b, it maps to zero in both E (by hom-vanishing, since E's phases are < b) and Q[-1] (since Q[-1]'s phases are \le c - 1 < b). The coyoneda exact sequence on the inverse-rotated triangle forces the map to factor through both, giving zero, contradicting non-triviality of the factor.

🔗theorem
CategoryTheory.Triangulated.Slicing.phiPlus_lt_of_triangle_with_leProp.{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]
  (s : CategoryTheory.Triangulated.Slicing C) {K E Q : C}
  (hK : ¬CategoryTheory.Limits.IsZero K) {b : ℝ}
  (hE_lt :
    ∀ (hE : ¬CategoryTheory.Limits.IsZero E),
      CategoryTheory.Triangulated.Slicing.phiPlus C s E hE < b)
  {c : ℝ} (hQ_le : CategoryTheory.Triangulated.Slicing.leProp C s c Q)
  (hcb : c < b + 1) {f₁ : K ⟶ E} {f₂ : E ⟶ Q}
  {f₃ : Q ⟶ (CategoryTheory.shiftFunctor C 1).obj K}
  (hT :
    CategoryTheory.Pretriangulated.Triangle.mk f₁ f₂ f₃ ∈
      CategoryTheory.Pretriangulated.distinguishedTriangles) :
  CategoryTheory.Triangulated.Slicing.phiPlus C s K hK < b
CategoryTheory.Triangulated.Slicing.phiPlus_lt_of_triangle_with_leProp.{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]
  (s :
    CategoryTheory.Triangulated.Slicing C)
  {K E Q : C}
  (hK : ¬CategoryTheory.Limits.IsZero K)
  {b : ℝ}
  (hE_lt :
    ∀
      (hE :
        ¬CategoryTheory.Limits.IsZero E),
      CategoryTheory.Triangulated.Slicing.phiPlus
          C s E hE <
        b)
  {c : ℝ}
  (hQ_le :
    CategoryTheory.Triangulated.Slicing.leProp
      C s c Q)
  (hcb : c < b + 1) {f₁ : K ⟶ E}
  {f₂ : E ⟶ Q}
  {f₃ :
    Q ⟶
      (CategoryTheory.shiftFunctor C
            1).obj
        K}
  (hT :
    CategoryTheory.Pretriangulated.Triangle.mk
        f₁ f₂ f₃ ∈
      CategoryTheory.Pretriangulated.distinguishedTriangles) :
  CategoryTheory.Triangulated.Slicing.phiPlus
      C s K hK <
    b

Something wrong, better idea? Suggest a change

7.5.15. phiMinus_gt_of_triangle_with_gtProp🔗

Phase lower bound from one-sided containment (dual). In a triangle K \to E \to Q \to K[1], if \phi^-(E) > a and K satisfies \operatorname{gtProp}(c) with a < c + 1, then if Q is nonzero, a < \phi^-(Q).

Proof: Dual of phiPlus_lt_of_triangle_with_leProp. By contradiction: if the bottom HN factor of Q has phase \le a, then E \to \text{bottom factor} vanishes by hom-vanishing, and the Yoneda exact sequence forces the map to factor through K[1]. Since K[1]'s phases are > c + 1 > a, this factoring also vanishes, contradicting non-triviality.

🔗theorem
CategoryTheory.Triangulated.Slicing.phiMinus_gt_of_triangle_with_gtProp.{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]
  (s : CategoryTheory.Triangulated.Slicing C) {K E Q : C}
  (hQ : ¬CategoryTheory.Limits.IsZero Q) {a : ℝ}
  (hE_gt :
    ∀ (hE : ¬CategoryTheory.Limits.IsZero E),
      a < CategoryTheory.Triangulated.Slicing.phiMinus C s E hE)
  {c : ℝ} (hK_gt : CategoryTheory.Triangulated.Slicing.gtProp C s c K)
  (hca : a < c + 1) {f₁ : K ⟶ E} {f₂ : E ⟶ Q}
  {f₃ : Q ⟶ (CategoryTheory.shiftFunctor C 1).obj K}
  (hT :
    CategoryTheory.Pretriangulated.Triangle.mk f₁ f₂ f₃ ∈
      CategoryTheory.Pretriangulated.distinguishedTriangles) :
  a < CategoryTheory.Triangulated.Slicing.phiMinus C s Q hQ
CategoryTheory.Triangulated.Slicing.phiMinus_gt_of_triangle_with_gtProp.{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]
  (s :
    CategoryTheory.Triangulated.Slicing C)
  {K E Q : C}
  (hQ : ¬CategoryTheory.Limits.IsZero Q)
  {a : ℝ}
  (hE_gt :
    ∀
      (hE :
        ¬CategoryTheory.Limits.IsZero E),
      a <
        CategoryTheory.Triangulated.Slicing.phiMinus
          C s E hE)
  {c : ℝ}
  (hK_gt :
    CategoryTheory.Triangulated.Slicing.gtProp
      C s c K)
  (hca : a < c + 1) {f₁ : K ⟶ E}
  {f₂ : E ⟶ Q}
  {f₃ :
    Q ⟶
      (CategoryTheory.shiftFunctor C
            1).obj
        K}
  (hT :
    CategoryTheory.Pretriangulated.Triangle.mk
        f₁ f₂ f₃ ∈
      CategoryTheory.Pretriangulated.distinguishedTriangles) :
  a <
    CategoryTheory.Triangulated.Slicing.phiMinus
      C s Q hQ

Something wrong, better idea? Suggest a change

7.5.16. first_intervalProp_of_triangle🔗

Kernel/image containment in thin intervals. In a distinguished triangle K \to E \to Q \to K[1] where E \in \mathcal{P}((a,b)), Q satisfies \operatorname{leProp}(a+1), and K satisfies \operatorname{gtProp}(a), then K \in \mathcal{P}((a, b)).

Proof: The upper bound \phi^+(K) < b comes from phiPlus_lt_of_triangle_with_leProp (with c = a + 1 < b + 1). The lower bound \phi^-(K) > a comes from \operatorname{gtProp}(a). Together these place all HN phases in (a, b).

🔗theorem
CategoryTheory.Triangulated.Slicing.first_intervalProp_of_triangle.{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]
  (s : CategoryTheory.Triangulated.Slicing C) {a b : ℝ} (hab' : a < b)
  {K E Q : C}
  (hE : CategoryTheory.Triangulated.Slicing.intervalProp C s a b E)
  (hQ_le : CategoryTheory.Triangulated.Slicing.leProp C s (a + 1) Q)
  (hK_gt : CategoryTheory.Triangulated.Slicing.gtProp C s a K)
  {f₁ : K ⟶ E} {f₂ : E ⟶ Q}
  {f₃ : Q ⟶ (CategoryTheory.shiftFunctor C 1).obj K}
  (hT :
    CategoryTheory.Pretriangulated.Triangle.mk f₁ f₂ f₃ ∈
      CategoryTheory.Pretriangulated.distinguishedTriangles) :
  CategoryTheory.Triangulated.Slicing.intervalProp C s a b K
CategoryTheory.Triangulated.Slicing.first_intervalProp_of_triangle.{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]
  (s :
    CategoryTheory.Triangulated.Slicing C)
  {a b : ℝ} (hab' : a < b) {K E Q : C}
  (hE :
    CategoryTheory.Triangulated.Slicing.intervalProp
      C s a b E)
  (hQ_le :
    CategoryTheory.Triangulated.Slicing.leProp
      C s (a + 1) Q)
  (hK_gt :
    CategoryTheory.Triangulated.Slicing.gtProp
      C s a K)
  {f₁ : K ⟶ E} {f₂ : E ⟶ Q}
  {f₃ :
    Q ⟶
      (CategoryTheory.shiftFunctor C
            1).obj
        K}
  (hT :
    CategoryTheory.Pretriangulated.Triangle.mk
        f₁ f₂ f₃ ∈
      CategoryTheory.Pretriangulated.distinguishedTriangles) :
  CategoryTheory.Triangulated.Slicing.intervalProp
    C s a b K

  • Kernels: In the heart SES 0 → ker(f) → E → im(f) → 0, both ker(f) and im(f) are in the left heart, hence satisfy gtProp a and leProp (a+1).

  • Images: In the heart SES 0 → im(f) → F → coker(f) → 0, similarly.

Something wrong, better idea? Suggest a change

7.5.17. intervalProp_extension_closed🔗

The interval subcategory \mathcal{P}((a,b)) is extension-closed in the triangulated category: if A, B \in \mathcal{P}((a,b)) and A \to E \to B \to A[1] is distinguished, then E \in \mathcal{P}((a,b)).

Proof: Follows from the general extension closure for the interval property of a slicing.

🔗theorem
CategoryTheory.Triangulated.Slicing.intervalProp_extension_closed.{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]
  (s : CategoryTheory.Triangulated.Slicing C) {a b : ℝ} {A E B : C}
  (hA : CategoryTheory.Triangulated.Slicing.intervalProp C s a b A)
  (hB : CategoryTheory.Triangulated.Slicing.intervalProp C s a b B)
  {f : A ⟶ E} {g : E ⟶ B}
  {h : B ⟶ (CategoryTheory.shiftFunctor C 1).obj A}
  (hT :
    CategoryTheory.Pretriangulated.Triangle.mk f g h ∈
      CategoryTheory.Pretriangulated.distinguishedTriangles) :
  CategoryTheory.Triangulated.Slicing.intervalProp C s a b E
CategoryTheory.Triangulated.Slicing.intervalProp_extension_closed.{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]
  (s :
    CategoryTheory.Triangulated.Slicing C)
  {a b : ℝ} {A E B : C}
  (hA :
    CategoryTheory.Triangulated.Slicing.intervalProp
      C s a b A)
  (hB :
    CategoryTheory.Triangulated.Slicing.intervalProp
      C s a b B)
  {f : A ⟶ E} {g : E ⟶ B}
  {h :
    B ⟶
      (CategoryTheory.shiftFunctor C
            1).obj
        A}
  (hT :
    CategoryTheory.Pretriangulated.Triangle.mk
        f g h ∈
      CategoryTheory.Pretriangulated.distinguishedTriangles) :
  CategoryTheory.Triangulated.Slicing.intervalProp
    C s a b E

Something wrong, better idea? Suggest a change

7.5.18. phiMinus_gt_of_triangle_with_geProp🔗

Phase lower bound from non-strict one-sided containment. In a triangle K \to E \to Q \to K[1], if \phi^-(E) > a and K satisfies \operatorname{geProp}(c) (phases \ge c) with a < c + 1, then if Q is nonzero, a < \phi^-(Q).

Proof: Same strategy as phiMinus_gt_of_triangle_with_gtProp, but with the non-strict bound \operatorname{geProp} instead of \operatorname{gtProp}. The shifted filtration of K[1] has phases \ge c + 1 > a, still providing the hom-vanishing gap.

🔗theorem
CategoryTheory.Triangulated.Slicing.phiMinus_gt_of_triangle_with_geProp.{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]
  (s : CategoryTheory.Triangulated.Slicing C) {K E Q : C}
  (hQ : ¬CategoryTheory.Limits.IsZero Q) {a : ℝ}
  (hE_gt :
    ∀ (hE : ¬CategoryTheory.Limits.IsZero E),
      a < CategoryTheory.Triangulated.Slicing.phiMinus C s E hE)
  {c : ℝ} (hK_ge : CategoryTheory.Triangulated.Slicing.geProp C s c K)
  (hca : a < c + 1) {f₁ : K ⟶ E} {f₂ : E ⟶ Q}
  {f₃ : Q ⟶ (CategoryTheory.shiftFunctor C 1).obj K}
  (hT :
    CategoryTheory.Pretriangulated.Triangle.mk f₁ f₂ f₃ ∈
      CategoryTheory.Pretriangulated.distinguishedTriangles) :
  a < CategoryTheory.Triangulated.Slicing.phiMinus C s Q hQ
CategoryTheory.Triangulated.Slicing.phiMinus_gt_of_triangle_with_geProp.{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]
  (s :
    CategoryTheory.Triangulated.Slicing C)
  {K E Q : C}
  (hQ : ¬CategoryTheory.Limits.IsZero Q)
  {a : ℝ}
  (hE_gt :
    ∀
      (hE :
        ¬CategoryTheory.Limits.IsZero E),
      a <
        CategoryTheory.Triangulated.Slicing.phiMinus
          C s E hE)
  {c : ℝ}
  (hK_ge :
    CategoryTheory.Triangulated.Slicing.geProp
      C s c K)
  (hca : a < c + 1) {f₁ : K ⟶ E}
  {f₂ : E ⟶ Q}
  {f₃ :
    Q ⟶
      (CategoryTheory.shiftFunctor C
            1).obj
        K}
  (hT :
    CategoryTheory.Pretriangulated.Triangle.mk
        f₁ f₂ f₃ ∈
      CategoryTheory.Pretriangulated.distinguishedTriangles) :
  a <
    CategoryTheory.Triangulated.Slicing.phiMinus
      C s Q hQ

Something wrong, better idea? Suggest a change

7.5.19. third_intervalProp_of_triangle🔗

Cokernel/quotient containment in thin intervals (Lemma 4.3 dual). In a distinguished triangle K \to E \to Q \to K[1] where E \in \mathcal{P}((a,b)), K has \operatorname{geProp}(b-1), and Q has \operatorname{ltProp}(b), then Q \in \mathcal{P}((a, b)).

Proof: The upper bound \phi^+(Q) < b is immediate from \operatorname{ltProp}(b). The lower bound \phi^-(Q) > a comes from phiMinus_gt_of_triangle_with_geProp with c = b - 1 (so a < (b-1) + 1 = b). Together with first_intervalProp_of_triangle, this establishes the quasi-abelian structure of \mathcal{P}((a,b)).

🔗theorem
CategoryTheory.Triangulated.Slicing.third_intervalProp_of_triangle.{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]
  (s : CategoryTheory.Triangulated.Slicing C) {a b : ℝ} (hab' : a < b)
  {K E Q : C}
  (hE : CategoryTheory.Triangulated.Slicing.intervalProp C s a b E)
  (hK_ge : CategoryTheory.Triangulated.Slicing.geProp C s (b - 1) K)
  (hQ_lt : CategoryTheory.Triangulated.Slicing.ltProp C s b Q)
  {f₁ : K ⟶ E} {f₂ : E ⟶ Q}
  {f₃ : Q ⟶ (CategoryTheory.shiftFunctor C 1).obj K}
  (hT :
    CategoryTheory.Pretriangulated.Triangle.mk f₁ f₂ f₃ ∈
      CategoryTheory.Pretriangulated.distinguishedTriangles) :
  CategoryTheory.Triangulated.Slicing.intervalProp C s a b Q
CategoryTheory.Triangulated.Slicing.third_intervalProp_of_triangle.{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]
  (s :
    CategoryTheory.Triangulated.Slicing C)
  {a b : ℝ} (hab' : a < b) {K E Q : C}
  (hE :
    CategoryTheory.Triangulated.Slicing.intervalProp
      C s a b E)
  (hK_ge :
    CategoryTheory.Triangulated.Slicing.geProp
      C s (b - 1) K)
  (hQ_lt :
    CategoryTheory.Triangulated.Slicing.ltProp
      C s b Q)
  {f₁ : K ⟶ E} {f₂ : E ⟶ Q}
  {f₃ :
    Q ⟶
      (CategoryTheory.shiftFunctor C
            1).obj
        K}
  (hT :
    CategoryTheory.Pretriangulated.Triangle.mk
        f₁ f₂ f₃ ∈
      CategoryTheory.Pretriangulated.distinguishedTriangles) :
  CategoryTheory.Triangulated.Slicing.intervalProp
    C s a b Q

Something wrong, better idea? Suggest a change

7.5.20. intervalProp_of_mono_leftHeart🔗

If f : X \to Y is a monomorphism in the left heart \mathcal{P}((a, a+1]) and Y \in \mathcal{P}((a, b)), then X \in \mathcal{P}((a, b)). This is the kernel-side closure from Bridgeland Lemma 4.2.

Proof: In the abelian heart, the cokernel Q of f exists and the SES X \hookrightarrow Y \twoheadrightarrow Q lifts to a distinguished triangle. Since Q is in the heart with \operatorname{leProp}(a+1) and X has \operatorname{gtProp}(a) from heart membership, first_intervalProp_of_triangle applies.

🔗theorem
CategoryTheory.Triangulated.Slicing.intervalProp_of_mono_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]
  {a b : ℝ} [Fact (a < b)] (s : CategoryTheory.Triangulated.Slicing C)
  {X Y :
    (CategoryTheory.Triangulated.Slicing.toTStructure C
          (CategoryTheory.Triangulated.Slicing.phaseShift C s
            a)).heart.FullSubcategory}
  (hY : CategoryTheory.Triangulated.Slicing.intervalProp C s a b Y.obj)
  (f : X ⟶ Y) [CategoryTheory.Mono f] :
  CategoryTheory.Triangulated.Slicing.intervalProp C s a b X.obj
CategoryTheory.Triangulated.Slicing.intervalProp_of_mono_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]
  {a b : ℝ} [Fact (a < b)]
  (s :
    CategoryTheory.Triangulated.Slicing C)
  {X Y :
    (CategoryTheory.Triangulated.Slicing.toTStructure
          C
          (CategoryTheory.Triangulated.Slicing.phaseShift
            C s a)).heart.FullSubcategory}
  (hY :
    CategoryTheory.Triangulated.Slicing.intervalProp
      C s a b Y.obj)
  (f : X ⟶ Y) [CategoryTheory.Mono f] :
  CategoryTheory.Triangulated.Slicing.intervalProp
    C s a b X.obj

Something wrong, better idea? Suggest a change

7.5.21. intervalProp_of_epi_rightHeart🔗

If f : X \to Y is an epimorphism in the right heart \mathcal{P}([b-1, b)) and X \in \mathcal{P}((a, b)), then Y \in \mathcal{P}((a, b)). This is the cokernel-side closure from Bridgeland Lemma 4.2.

Proof: In the abelian heart, the kernel K of f exists and the SES lifts to a distinguished triangle. Since K has \operatorname{geProp}(b-1) from right heart membership and Y has \operatorname{ltProp}(b), third_intervalProp_of_triangle gives Y \in \mathcal{P}((a,b)).

🔗theorem
CategoryTheory.Triangulated.Slicing.intervalProp_of_epi_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]
  {a b : ℝ} [Fact (a < b)] (s : CategoryTheory.Triangulated.Slicing C)
  {X Y :
    (CategoryTheory.Triangulated.Slicing.toTStructureGE C
          (CategoryTheory.Triangulated.Slicing.phaseShift C s
            (b - 1))).heart.FullSubcategory}
  (hX : CategoryTheory.Triangulated.Slicing.intervalProp C s a b X.obj)
  (f : X ⟶ Y) [CategoryTheory.Epi f] :
  CategoryTheory.Triangulated.Slicing.intervalProp C s a b Y.obj
CategoryTheory.Triangulated.Slicing.intervalProp_of_epi_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]
  {a b : ℝ} [Fact (a < b)]
  (s :
    CategoryTheory.Triangulated.Slicing C)
  {X Y :
    (CategoryTheory.Triangulated.Slicing.toTStructureGE
          C
          (CategoryTheory.Triangulated.Slicing.phaseShift
            C s
            (b -
              1))).heart.FullSubcategory}
  (hX :
    CategoryTheory.Triangulated.Slicing.intervalProp
      C s a b X.obj)
  (f : X ⟶ Y) [CategoryTheory.Epi f] :
  CategoryTheory.Triangulated.Slicing.intervalProp
    C s a b Y.obj

Something wrong, better idea? Suggest a change