Bridgeland Stability Conditions

9.3. Slicing: ExtensionClosure🔗

9.3.1. leProp_of_triangle🔗

Extension-closure of \mathcal{P}(\le t). If A \to E \to B \to A[1] is a distinguished triangle and both A and B have all HN phases \le t, then E also has all HN phases \le t.

Proof: By contradiction: suppose \phi^+(E) > t. Then the first HN factor F^+ of E has phase > t. By Hom-vanishing, \operatorname{Hom}(F^+, A) = 0 and \operatorname{Hom}(F^+, B) = 0. The coYoneda exact sequence on the triangle then gives \operatorname{Hom}(F^+, E) = 0, contradicting the fact that F^+ is a nonzero factor of E.

🔗theorem
CategoryTheory.Triangulated.Slicing.leProp_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 E B : C} (t : ℝ)
  (hA : CategoryTheory.Triangulated.Slicing.leProp C s t A)
  (hB : CategoryTheory.Triangulated.Slicing.leProp C s t 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.leProp C s t E
CategoryTheory.Triangulated.Slicing.leProp_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 E B : C} (t : ℝ)
  (hA :
    CategoryTheory.Triangulated.Slicing.leProp
      C s t A)
  (hB :
    CategoryTheory.Triangulated.Slicing.leProp
      C s t 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.leProp
    C s t E

Something wrong, better idea? Suggest a change

9.3.2. ltProp_of_triangle🔗

Extension-closure of \mathcal{P}(< t). If A \to E \to B \to A[1] is a distinguished triangle and both A and B have all HN phases < t, then E also has all HN phases < t.

Proof: By contradiction: if \phi^+(E) \ge t, then Hom-vanishing kills all maps from the top HN factor of E to both A and B, and coYoneda exactness forces it to map trivially to E, contradicting non-triviality. The argument mirrors leProp_of_triangle with strict inequalities.

🔗theorem
CategoryTheory.Triangulated.Slicing.ltProp_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 E B : C} (t : ℝ)
  (hA : CategoryTheory.Triangulated.Slicing.ltProp C s t A)
  (hB : CategoryTheory.Triangulated.Slicing.ltProp C s t 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.ltProp C s t E
CategoryTheory.Triangulated.Slicing.ltProp_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 E B : C} (t : ℝ)
  (hA :
    CategoryTheory.Triangulated.Slicing.ltProp
      C s t A)
  (hB :
    CategoryTheory.Triangulated.Slicing.ltProp
      C s t 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.ltProp
    C s t E

Something wrong, better idea? Suggest a change

9.3.3. gtProp_of_triangle🔗

Extension-closure of \mathcal{P}(> t). If A \to E \to B \to A[1] is a distinguished triangle and both A and B have all HN phases > t, then E also has all HN phases > t.

Proof: By contradiction: suppose \phi^-(E) \le t. Then the last HN factor F^- of E has phase \le t. By Hom-vanishing, \operatorname{Hom}(A, F^-) = 0 and \operatorname{Hom}(B, F^-) = 0. The Yoneda exact sequence on the triangle gives \operatorname{Hom}(E, F^-) = 0, contradicting the non-triviality of F^-.

🔗theorem
CategoryTheory.Triangulated.Slicing.gtProp_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 E B : C} (t : ℝ)
  (hA : CategoryTheory.Triangulated.Slicing.gtProp C s t A)
  (hB : CategoryTheory.Triangulated.Slicing.gtProp C s t 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.gtProp C s t E
CategoryTheory.Triangulated.Slicing.gtProp_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 E B : C} (t : ℝ)
  (hA :
    CategoryTheory.Triangulated.Slicing.gtProp
      C s t A)
  (hB :
    CategoryTheory.Triangulated.Slicing.gtProp
      C s t 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.gtProp
    C s t E

Something wrong, better idea? Suggest a change

9.3.4. phiPlus_lt_of_triangle🔗

If A \to E \to B \to A[1] is a distinguished triangle and \phi^+(A) < t, \phi^+(B) < t for any nonzero A, B, then \phi^+(E) < t for the nonzero middle term.

Proof: By contradiction: if \phi^+(E) \ge t, then the top HN factor of E has phase \ge t, placing it above both \phi^+(A) and \phi^+(B). CoYoneda exactness forces all maps from this factor to E to vanish, contradicting non-triviality.

🔗theorem
CategoryTheory.Triangulated.Slicing.phiPlus_lt_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 E B : C}
  (hE : ¬CategoryTheory.Limits.IsZero E) {t : ℝ}
  (hA_lt :
    ∀ (hA : ¬CategoryTheory.Limits.IsZero A),
      CategoryTheory.Triangulated.Slicing.phiPlus C s A hA < t)
  (hB_lt :
    ∀ (hB : ¬CategoryTheory.Limits.IsZero B),
      CategoryTheory.Triangulated.Slicing.phiPlus C s B hB < t)
  {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.phiPlus C s E hE < t
CategoryTheory.Triangulated.Slicing.phiPlus_lt_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 E B : C}
  (hE : ¬CategoryTheory.Limits.IsZero E)
  {t : ℝ}
  (hA_lt :
    ∀
      (hA :
        ¬CategoryTheory.Limits.IsZero A),
      CategoryTheory.Triangulated.Slicing.phiPlus
          C s A hA <
        t)
  (hB_lt :
    ∀
      (hB :
        ¬CategoryTheory.Limits.IsZero B),
      CategoryTheory.Triangulated.Slicing.phiPlus
          C s B hB <
        t)
  {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.phiPlus
      C s E hE <
    t

Something wrong, better idea? Suggest a change

9.3.5. phiMinus_gt_of_triangle🔗

If A \to E \to B \to A[1] is a distinguished triangle and \phi^-(A) > t, \phi^-(B) > t for any nonzero A, B, then \phi^-(E) > t for the nonzero middle term.

Proof: By contradiction: if \phi^-(E) \le t, the last HN factor of E has phase \le t, below both \phi^-(A) and \phi^-(B). Yoneda exactness forces all maps from E to this factor to vanish, contradicting non-triviality.

🔗theorem
CategoryTheory.Triangulated.Slicing.phiMinus_gt_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 E B : C}
  (hE : ¬CategoryTheory.Limits.IsZero E) {t : ℝ}
  (hA_gt :
    ∀ (hA : ¬CategoryTheory.Limits.IsZero A),
      t < CategoryTheory.Triangulated.Slicing.phiMinus C s A hA)
  (hB_gt :
    ∀ (hB : ¬CategoryTheory.Limits.IsZero B),
      t < CategoryTheory.Triangulated.Slicing.phiMinus C s B hB)
  {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) :
  t < CategoryTheory.Triangulated.Slicing.phiMinus C s E hE
CategoryTheory.Triangulated.Slicing.phiMinus_gt_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 E B : C}
  (hE : ¬CategoryTheory.Limits.IsZero E)
  {t : ℝ}
  (hA_gt :
    ∀
      (hA :
        ¬CategoryTheory.Limits.IsZero A),
      t <
        CategoryTheory.Triangulated.Slicing.phiMinus
          C s A hA)
  (hB_gt :
    ∀
      (hB :
        ¬CategoryTheory.Limits.IsZero B),
      t <
        CategoryTheory.Triangulated.Slicing.phiMinus
          C s B hB)
  {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) :
  t <
    CategoryTheory.Triangulated.Slicing.phiMinus
      C s E hE

Something wrong, better idea? Suggest a change

9.3.6. intervalProp_of_triangle🔗

Extension-closure of \mathcal{P}((a,b)). If A \to E \to B \to A[1] is a distinguished triangle and both A and B have all HN phases in the open interval (a, b), then so does E.

Proof: Combines phiPlus_lt_of_triangle to get \phi^+(E) < b and phiMinus_gt_of_triangle to get \phi^-(E) > a. Then all phases of E lie in (a, b) by the phase range lemma.

🔗theorem
CategoryTheory.Triangulated.Slicing.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 E B : C} {a b : ℝ}
  (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_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 E B : C} {a b : ℝ}
  (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

9.3.7. phiPlus_triangle_le🔗

[Lemma 3.4] φ⁺(A) ≤ φ⁺(E)

Lemma 3.4 (left inequality). In a distinguished triangle A \to E \to B \to A[1] where the phases of A and B lie in an interval (a, b) with b \le a + 1, one has \phi^+(A) \le \phi^+(E).

Proof: By contradiction: if \phi^+(A) > \phi^+(E), then the top factor A^+ of A has all maps to E vanishing (phase gap). By the coYoneda exact sequence on the inverse rotation, maps A^+ \to A factor through B[-1]. The width condition b \le a + 1 ensures that the shifted phases of B[-1] are below \phi(A^+), so \operatorname{Hom}(A^+, B[-1]) = 0 as well, giving A^+ = 0, a contradiction.

🔗theorem
CategoryTheory.Triangulated.Slicing.phiPlus_triangle_le.{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 E B : C}
  (hA : ¬CategoryTheory.Limits.IsZero A)
  (hE : ¬CategoryTheory.Limits.IsZero E) {a b : ℝ} (hab : b ≤ a + 1)
  (hA_int : CategoryTheory.Triangulated.Slicing.intervalProp C s a b A)
  (hB_int : 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.phiPlus C s A hA ≤
    CategoryTheory.Triangulated.Slicing.phiPlus C s E hE
CategoryTheory.Triangulated.Slicing.phiPlus_triangle_le.{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 E B : C}
  (hA : ¬CategoryTheory.Limits.IsZero A)
  (hE : ¬CategoryTheory.Limits.IsZero E)
  {a b : ℝ} (hab : b ≤ a + 1)
  (hA_int :
    CategoryTheory.Triangulated.Slicing.intervalProp
      C s a b A)
  (hB_int :
    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.phiPlus
      C s A hA ≤
    CategoryTheory.Triangulated.Slicing.phiPlus
      C s E hE

Something wrong, better idea? Suggest a change

9.3.8. phiMinus_triangle_le🔗

[Lemma 3.4] φ⁻(E) ≤ φ⁻(B)

Lemma 3.4 (right inequality). In a distinguished triangle A \to E \to B \to A[1] where the phases of A and B lie in an interval (a, b) with b \le a + 1, one has \phi^-(E) \le \phi^-(B).

Proof: By contradiction: if \phi^-(E) > \phi^-(B), then maps E \to B^- vanish by Hom-vanishing. By the Yoneda exact sequence, maps B \to B^- factor through A[1]. The width condition ensures the shifted phases of A[1] are above \phi(B^-), so \operatorname{Hom}(A[1], B^-) = 0, giving B^- = 0, a contradiction.

🔗theorem
CategoryTheory.Triangulated.Slicing.phiMinus_triangle_le.{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 E B : C}
  (hB : ¬CategoryTheory.Limits.IsZero B)
  (hE : ¬CategoryTheory.Limits.IsZero E) {a b : ℝ} (hab : b ≤ a + 1)
  (hA_int : CategoryTheory.Triangulated.Slicing.intervalProp C s a b A)
  (hB_int : 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.phiMinus C s E hE ≤
    CategoryTheory.Triangulated.Slicing.phiMinus C s B hB
CategoryTheory.Triangulated.Slicing.phiMinus_triangle_le.{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 E B : C}
  (hB : ¬CategoryTheory.Limits.IsZero B)
  (hE : ¬CategoryTheory.Limits.IsZero E)
  {a b : ℝ} (hab : b ≤ a + 1)
  (hA_int :
    CategoryTheory.Triangulated.Slicing.intervalProp
      C s a b A)
  (hB_int :
    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.phiMinus
      C s E hE ≤
    CategoryTheory.Triangulated.Slicing.phiMinus
      C s B hB

Something wrong, better idea? Suggest a change

9.3.9. phiMinus_triangle_le'🔗

Variant of Lemma 3.4 (phiMinus_triangle_le) where the hypothesis B \in \mathcal{P}((a,b)) is weakened to \phi^+(B) < b. Under the same width bound b \le a + 1 and with A \in \mathcal{P}((a,b)), one still obtains \phi^-(E) \le \phi^-(B).

Proof: Same proof strategy as phiMinus_triangle_le, using the weaker hypothesis \phi^+(B) < b (rather than full interval membership) wherever the upper phase bound of B is needed.

🔗theorem
CategoryTheory.Triangulated.Slicing.phiMinus_triangle_le'.{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 E B : C}
  (hB : ¬CategoryTheory.Limits.IsZero B)
  (hE : ¬CategoryTheory.Limits.IsZero E) {a b : ℝ} (hab : b ≤ a + 1)
  (hA_int : CategoryTheory.Triangulated.Slicing.intervalProp C s a b A)
  (hB_phiPlus_lt :
    CategoryTheory.Triangulated.Slicing.phiPlus C s B hB < 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.phiMinus C s E hE ≤
    CategoryTheory.Triangulated.Slicing.phiMinus C s B hB
CategoryTheory.Triangulated.Slicing.phiMinus_triangle_le'.{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 E B : C}
  (hB : ¬CategoryTheory.Limits.IsZero B)
  (hE : ¬CategoryTheory.Limits.IsZero E)
  {a b : ℝ} (hab : b ≤ a + 1)
  (hA_int :
    CategoryTheory.Triangulated.Slicing.intervalProp
      C s a b A)
  (hB_phiPlus_lt :
    CategoryTheory.Triangulated.Slicing.phiPlus
        C s B hB <
      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.phiMinus
      C s E hE ≤
    CategoryTheory.Triangulated.Slicing.phiMinus
      C s B hB

Something wrong, better idea? Suggest a change