Bridgeland Stability Conditions

9.7. Slicing: TStructureConstruction🔗

9.7.1. exists_triangle_gtProp_leProp🔗

Given an HN filtration of an object A, there exists a distinguished triangle X \to A \to Y \to X[1] with X \in \mathcal{P}(> 0) and Y \in \mathcal{P}(\le 0). Moreover, if X is nonzero, its phases are drawn from those of the original filtration with appropriate bounds.

Proof: Induction on the filtration length. If all phases are > 0, take X = A and Y = 0. If all phases are \le 0, take X = 0 and Y = A. In the mixed case, split the prefix filtration by the inductive hypothesis, then use the octahedral axiom to incorporate the remaining low-phase factor via appendFactor.

🔗theorem
CategoryTheory.Triangulated.Slicing.exists_triangle_gtProp_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] [CategoryTheory.IsTriangulated C]
  (s : CategoryTheory.Triangulated.Slicing C) (A : C)
  (F : CategoryTheory.Triangulated.HNFiltration C s.P A) :
  ∃ X Y,
    ∃ (_ : CategoryTheory.Triangulated.Slicing.gtProp C s 0 X) (_ :
      CategoryTheory.Triangulated.Slicing.leProp C s 0 Y),
      ∃ f g h,
        CategoryTheory.Pretriangulated.Triangle.mk f g h ∈
            CategoryTheory.Pretriangulated.distinguishedTriangles ∧
          (CategoryTheory.Limits.IsZero X ∨
              ∃ GX,
                ∃ (hGX : 0 < GX.n),
                  0 <
                      CategoryTheory.Triangulated.HNFiltration.phiMinus
                        C GX hGX ∧
                    (∀ (hn0 : 0 < F.n),
                        CategoryTheory.Triangulated.HNFiltration.phiPlus
                            C GX hGX ≤
                          F.φ ⟨0, hn0⟩) ∧
                      ∀ (j : Fin GX.n), ∃ i, GX.φ j = F.φ i) ∧
            (CategoryTheory.Limits.IsZero Y ∨
              ∃ GY,
                ∃ (hGY : 0 < GY.n),
                  CategoryTheory.Triangulated.HNFiltration.phiPlus C GY
                        hGY ≤
                      0 ∧
                    ∀ (j : Fin GY.n), ∃ i, GY.φ j = F.φ i)
CategoryTheory.Triangulated.Slicing.exists_triangle_gtProp_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]
  [CategoryTheory.IsTriangulated C]
  (s :
    CategoryTheory.Triangulated.Slicing C)
  (A : C)
  (F :
    CategoryTheory.Triangulated.HNFiltration
      C s.P A) :
  ∃ X Y,
    ∃ (_ :
      CategoryTheory.Triangulated.Slicing.gtProp
        C s 0 X)
      (_ :
      CategoryTheory.Triangulated.Slicing.leProp
        C s 0 Y),
      ∃ f g h,
        CategoryTheory.Pretriangulated.Triangle.mk
              f g h ∈
            CategoryTheory.Pretriangulated.distinguishedTriangles ∧
          (CategoryTheory.Limits.IsZero
                X ∨
              ∃ GX,
                ∃ (hGX : 0 < GX.n),
                  0 <
                      CategoryTheory.Triangulated.HNFiltration.phiMinus
                        C GX hGX ∧
                    (∀ (hn0 : 0 < F.n),
                        CategoryTheory.Triangulated.HNFiltration.phiPlus
                            C GX hGX ≤
                          F.φ ⟨0, hn0⟩) ∧
                      ∀ (j : Fin GX.n),
                        ∃ i,
                          GX.φ j =
                            F.φ i) ∧
            (CategoryTheory.Limits.IsZero
                Y ∨
              ∃ GY,
                ∃ (hGY : 0 < GY.n),
                  CategoryTheory.Triangulated.HNFiltration.phiPlus
                        C GY hGY ≤
                      0 ∧
                    ∀ (j : Fin GY.n),
                      ∃ i, GY.φ j = F.φ i)

Something wrong, better idea? Suggest a change

9.7.2. exists_triangle_geProp_ltProp🔗

Dual decomposition: given an HN filtration of A, there exists a distinguished triangle X \to A \to Y \to X[1] with X \in \mathcal{P}(\ge 0) and Y \in \mathcal{P}(< 0).

Proof: Same inductive strategy as exists_triangle_gtProp_leProp, using the dual half-open predicates \mathcal{P}(\ge 0) and \mathcal{P}(< 0) and splitting at the boundary between non-negative and negative phases.

🔗theorem
CategoryTheory.Triangulated.Slicing.exists_triangle_geProp_ltProp.{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 : C)
  (F : CategoryTheory.Triangulated.HNFiltration C s.P A) :
  ∃ X Y,
    ∃ (_ : CategoryTheory.Triangulated.Slicing.geProp C s 0 X) (_ :
      CategoryTheory.Triangulated.Slicing.ltProp C s 0 Y),
      ∃ f g h,
        CategoryTheory.Pretriangulated.Triangle.mk f g h ∈
          CategoryTheory.Pretriangulated.distinguishedTriangles
CategoryTheory.Triangulated.Slicing.exists_triangle_geProp_ltProp.{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 : C)
  (F :
    CategoryTheory.Triangulated.HNFiltration
      C s.P A) :
  ∃ X Y,
    ∃ (_ :
      CategoryTheory.Triangulated.Slicing.geProp
        C s 0 X)
      (_ :
      CategoryTheory.Triangulated.Slicing.ltProp
        C s 0 Y),
      ∃ f g h,
        CategoryTheory.Pretriangulated.Triangle.mk
            f g h ∈
          CategoryTheory.Pretriangulated.distinguishedTriangles

Something wrong, better idea? Suggest a change

9.7.3. toTStructure🔗

A slicing \mathcal{P} on a triangulated category determines a t-structure with the convention: \mathcal{D}^{\le n} = \mathcal{P}(> -n) and \mathcal{D}^{\ge n} = \mathcal{P}(\le 1 - n). The heart is \mathcal{P}((0, 1]).

Construction: Constructs a TStructure by setting le n to gtProp(-n) and ge n to leProp(1 - n). Shift compatibility follows from gtProp_shift and leProp_shift. Hom-vanishing at the (0, 1) boundary uses zero_of_gtProp_leProp. The existence of the decomposition triangle at level (0, 1) is provided by exists_triangle_gtProp_leProp.

🔗def
CategoryTheory.Triangulated.Slicing.toTStructure.{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) :
  CategoryTheory.Triangulated.TStructure C
CategoryTheory.Triangulated.Slicing.toTStructure.{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) :
  CategoryTheory.Triangulated.TStructure C

  • le n = gtProp(-n): objects whose HN phases are all > -n

  • ge n = leProp(1-n): objects whose HN phases are all ≤ 1-n

Something wrong, better idea? Suggest a change

9.7.4. toTStructureGE🔗

A slicing \mathcal{P} also determines the dual half-open t-structure with: \mathcal{D}^{\le n} = \mathcal{P}(\ge -n) and \mathcal{D}^{\ge n} = \mathcal{P}(< 1 - n). The heart is \mathcal{P}([0, 1)).

Construction: Constructs a TStructure by setting le n to geProp(-n) and ge n to ltProp(1 - n). The decomposition triangle uses exists_triangle_geProp_ltProp.

🔗def
CategoryTheory.Triangulated.Slicing.toTStructureGE.{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) :
  CategoryTheory.Triangulated.TStructure C
CategoryTheory.Triangulated.Slicing.toTStructureGE.{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) :
  CategoryTheory.Triangulated.TStructure C

  • le n = geProp(-n): objects whose HN phases are all ≥ -n

  • ge n = ltProp(1-n): objects whose HN phases are all < 1-n

Something wrong, better idea? Suggest a change

9.7.5. toTStructure_bounded🔗

Bounded t-structure from a slicing. The t-structure \mathcal{D}^{\le \bullet} induced by a slicing is bounded: every object lies between \mathcal{D}^{\le a} and \mathcal{D}^{\ge b} for some integers a, b.

Proof: The HN filtration axiom places every nonzero object's phases in a finite interval [\phi^-, \phi^+]. Setting a = \lceil -\phi^- \rceil + 1 and b = \lfloor 1 - \phi^+ \rfloor gives the required integer bounds.

🔗theorem
CategoryTheory.Triangulated.Slicing.toTStructure_bounded.{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) :
  (CategoryTheory.Triangulated.Slicing.toTStructure C s).IsBounded
CategoryTheory.Triangulated.Slicing.toTStructure_bounded.{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) :
  (CategoryTheory.Triangulated.Slicing.toTStructure
      C s).IsBounded

Something wrong, better idea? Suggest a change

9.7.6. toTStructureGE_bounded🔗

Bounded t-structure from the dual half-open convention. The t-structure induced by toTStructureGE is bounded.

Proof: Same strategy as toTStructure_bounded, using ceiling/floor to convert the finite phase interval into integer bounds for the \ge / < predicates.

🔗theorem
CategoryTheory.Triangulated.Slicing.toTStructureGE_bounded.{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) :
  (CategoryTheory.Triangulated.Slicing.toTStructureGE C s).IsBounded
CategoryTheory.Triangulated.Slicing.toTStructureGE_bounded.{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) :
  (CategoryTheory.Triangulated.Slicing.toTStructureGE
      C s).IsBounded

Something wrong, better idea? Suggest a change

9.7.7. toTStructure_heart_iff🔗

An object E lies in the heart of the slicing-induced t-structure if and only if E \in \mathcal{P}(> 0) \cap \mathcal{P}(\le 1), i.e. its HN phases lie in the half-open interval (0, 1].

Proof: Unfolding the heart definition: E \in \mathcal{D}^{\le 0} \cap \mathcal{D}^{\ge 0} becomes \mathrm{gtProp}(0) and \mathrm{leProp}(1) after substituting the t-structure conventions.

🔗theorem
CategoryTheory.Triangulated.Slicing.toTStructure_heart_iff.{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) (E : C) :
  (CategoryTheory.Triangulated.Slicing.toTStructure C s).heart E ↔
    CategoryTheory.Triangulated.Slicing.gtProp C s 0 E ∧
      CategoryTheory.Triangulated.Slicing.leProp C s 1 E
CategoryTheory.Triangulated.Slicing.toTStructure_heart_iff.{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)
  (E : C) :
  (CategoryTheory.Triangulated.Slicing.toTStructure
          C s).heart
      E ↔
    CategoryTheory.Triangulated.Slicing.gtProp
        C s 0 E ∧
      CategoryTheory.Triangulated.Slicing.leProp
        C s 1 E

Something wrong, better idea? Suggest a change

9.7.8. toTStructureGE_heart_iff🔗

An object E lies in the heart of toTStructureGE if and only if E \in \mathcal{P}(\ge 0) \cap \mathcal{P}(< 1), i.e. its HN phases lie in [0, 1).

Proof: Unfolding the heart definition with the dual conventions.

🔗theorem
CategoryTheory.Triangulated.Slicing.toTStructureGE_heart_iff.{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) (E : C) :
  (CategoryTheory.Triangulated.Slicing.toTStructureGE C s).heart E ↔
    CategoryTheory.Triangulated.Slicing.geProp C s 0 E ∧
      CategoryTheory.Triangulated.Slicing.ltProp C s 1 E
CategoryTheory.Triangulated.Slicing.toTStructureGE_heart_iff.{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)
  (E : C) :
  (CategoryTheory.Triangulated.Slicing.toTStructureGE
          C s).heart
      E ↔
    CategoryTheory.Triangulated.Slicing.geProp
        C s 0 E ∧
      CategoryTheory.Triangulated.Slicing.ltProp
        C s 1 E

Something wrong, better idea? Suggest a change

9.7.9. exists_split_at_cutoff🔗

Splitting at an arbitrary cutoff. Given an HN filtration of E with all phases in (a, b) and a cutoff t, there exists a distinguished triangle X \to E \to Y \to X[1] with X \in \mathcal{P}(> t), Y \in \mathcal{P}(\le t), and \phi^+(X) < b if X \ne 0.

Proof: Phase-shift by t to reduce to the t = 0 case. Apply exists_triangle_gtProp_leProp to the shifted filtration. Convert back using phaseShift_gtProp_zero and phaseShift_leProp_zero. The upper phase bound on X is recovered via unphaseShift_phiPlus and the original interval constraint.

🔗theorem
CategoryTheory.Triangulated.Slicing.exists_split_at_cutoff.{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) {E : C}
  (F : CategoryTheory.Triangulated.HNFiltration C s.P E) {a b t : ℝ}
  (hI : ∀ (i : Fin F.n), a < F.φ i ∧ F.φ i < b) (hn : 0 < F.n) :
  ∃ X Y f g h,
    CategoryTheory.Pretriangulated.Triangle.mk f g h ∈
        CategoryTheory.Pretriangulated.distinguishedTriangles ∧
      CategoryTheory.Triangulated.Slicing.gtProp C s t X ∧
        CategoryTheory.Triangulated.Slicing.leProp C s t Y ∧
          ∀ (hXne : ¬CategoryTheory.Limits.IsZero X),
            CategoryTheory.Triangulated.Slicing.phiPlus C s X hXne < b
CategoryTheory.Triangulated.Slicing.exists_split_at_cutoff.{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)
  {E : C}
  (F :
    CategoryTheory.Triangulated.HNFiltration
      C s.P E)
  {a b t : ℝ}
  (hI :
    ∀ (i : Fin F.n),
      a < F.φ i ∧ F.φ i < b)
  (hn : 0 < F.n) :
  ∃ X Y f g h,
    CategoryTheory.Pretriangulated.Triangle.mk
          f g h ∈
        CategoryTheory.Pretriangulated.distinguishedTriangles ∧
      CategoryTheory.Triangulated.Slicing.gtProp
          C s t X ∧
        CategoryTheory.Triangulated.Slicing.leProp
            C s t Y ∧
          ∀
            (hXne :
              ¬CategoryTheory.Limits.IsZero
                  X),
            CategoryTheory.Triangulated.Slicing.phiPlus
                C s X hXne <
              b

  • X ∈ s.gtProp(t) (all phases > t)

  • Y ∈ s.leProp(t) (all phases ≤ t)

  • If X is nonzero, φ⁺(X) < b (preserving the upper interval bound)

Something wrong, better idea? Suggest a change

9.7.10. exists_split_with_interval🔗

Special case of exists_split_at_cutoff with t = a: split at the lower endpoint of the interval.

Proof: Direct application of exists_split_at_cutoff with t = a.

🔗theorem
CategoryTheory.Triangulated.Slicing.exists_split_with_interval.{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) {E : C}
  (F : CategoryTheory.Triangulated.HNFiltration C s.P E) {a b : ℝ}
  (hI : ∀ (i : Fin F.n), a < F.φ i ∧ F.φ i < b) (hn : 0 < F.n) :
  ∃ X Y f g h,
    CategoryTheory.Pretriangulated.Triangle.mk f g h ∈
        CategoryTheory.Pretriangulated.distinguishedTriangles ∧
      CategoryTheory.Triangulated.Slicing.gtProp C s a X ∧
        CategoryTheory.Triangulated.Slicing.leProp C s a Y ∧
          ∀ (hXne : ¬CategoryTheory.Limits.IsZero X),
            CategoryTheory.Triangulated.Slicing.phiPlus C s X hXne < b
CategoryTheory.Triangulated.Slicing.exists_split_with_interval.{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)
  {E : C}
  (F :
    CategoryTheory.Triangulated.HNFiltration
      C s.P E)
  {a b : ℝ}
  (hI :
    ∀ (i : Fin F.n),
      a < F.φ i ∧ F.φ i < b)
  (hn : 0 < F.n) :
  ∃ X Y f g h,
    CategoryTheory.Pretriangulated.Triangle.mk
          f g h ∈
        CategoryTheory.Pretriangulated.distinguishedTriangles ∧
      CategoryTheory.Triangulated.Slicing.gtProp
          C s a X ∧
        CategoryTheory.Triangulated.Slicing.leProp
            C s a Y ∧
          ∀
            (hXne :
              ¬CategoryTheory.Limits.IsZero
                  X),
            CategoryTheory.Triangulated.Slicing.phiPlus
                C s X hXne <
              b

Something wrong, better idea? Suggest a change