Bridgeland Stability Conditions

14.23. Deformation: TStructure🔗

14.23.1. chain_hom_eq_zero_of_gt_deformed🔗

Any morphism from a Q(\psi)-semistable object A to the k-th chain object of a Q-HN filtration whose phases are all strictly less than \psi is zero. This is the deformedPred analogue of chain_hom_eq_zero_of_gt.

Proof: Induction on k. Base: k = 0 is trivial since E_0 = 0. Inductive step: the coYoneda exact sequence on the k-th distinguished triangle gives that any map A \to E_{k+1} factors through A \to F_k (the k-th factor), but hom_eq_zero_of_deformedPred kills this by the phase gap.

🔗theorem
CategoryTheory.Triangulated.chain_hom_eq_zero_of_gt_deformed.{v, u, 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]
  {Λ : Type u'} [AddCommGroup Λ]
  {v : CategoryTheory.Triangulated.K₀ C →+ Λ}
  (σ : CategoryTheory.Triangulated.StabilityCondition.WithClassMap C v)
  (W : Λ →+ ℂ)
  (hW :
    CategoryTheory.Triangulated.stabSeminorm C σ (W - σ.Z) <
      ENNReal.ofReal 1)
  {ε₀ : ℝ} (hε₀ : 0 < ε₀) (hε₀2 : ε₀ < 1 / 4) (hε₀8 : ε₀ < 1 / 8)
  (hsin :
    CategoryTheory.Triangulated.stabSeminorm C σ (W - σ.Z) <
      ENNReal.ofReal (Real.sin (Real.pi * ε₀)))
  {A E : C} {ψ : ℝ}
  (hA :
    CategoryTheory.Triangulated.StabilityCondition.WithClassMap.deformedPred
      C σ W hW ε₀ ψ A)
  (F :
    CategoryTheory.Triangulated.HNFiltration C
      (CategoryTheory.Triangulated.StabilityCondition.WithClassMap.deformedPred
        C σ W hW ε₀)
      E)
  (hlt : ∀ (i : Fin F.n), F.φ i < ψ) (k : ℕ) (hk : k < F.n + 1)
  (f : A ⟶ F.chain.obj ⟨k, hk⟩) : f = 0
CategoryTheory.Triangulated.chain_hom_eq_zero_of_gt_deformed.{v,
    u, 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]
  {Λ : Type u'} [AddCommGroup Λ]
  {v :
    CategoryTheory.Triangulated.K₀ C →+ Λ}
  (σ :
    CategoryTheory.Triangulated.StabilityCondition.WithClassMap
      C v)
  (W : Λ →+ ℂ)
  (hW :
    CategoryTheory.Triangulated.stabSeminorm
        C σ (W - σ.Z) <
      ENNReal.ofReal 1)
  {ε₀ : ℝ} (hε₀ : 0 < ε₀)
  (hε₀2 : ε₀ < 1 / 4) (hε₀8 : ε₀ < 1 / 8)
  (hsin :
    CategoryTheory.Triangulated.stabSeminorm
        C σ (W - σ.Z) <
      ENNReal.ofReal
        (Real.sin (Real.pi * ε₀)))
  {A E : C} {ψ : ℝ}
  (hA :
    CategoryTheory.Triangulated.StabilityCondition.WithClassMap.deformedPred
      C σ W hW ε₀ ψ A)
  (F :
    CategoryTheory.Triangulated.HNFiltration
      C
      (CategoryTheory.Triangulated.StabilityCondition.WithClassMap.deformedPred
        C σ W hW ε₀)
      E)
  (hlt : ∀ (i : Fin F.n), F.φ i < ψ)
  (k : ℕ) (hk : k < F.n + 1)
  (f : A ⟶ F.chain.obj ⟨k, hk⟩) : f = 0

Something wrong, better idea? Suggest a change

14.23.2. hom_eq_zero_of_gt_phases_deformed🔗

A morphism from a Q(\psi)-semistable object to an HN-filtered object whose phases are all strictly less than \psi is zero.

Proof: Apply chain_hom_eq_zero_of_gt_deformed at the top of the chain, using the isomorphism E_n \cong E.

🔗theorem
CategoryTheory.Triangulated.hom_eq_zero_of_gt_phases_deformed.{v, u, 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]
  {Λ : Type u'} [AddCommGroup Λ]
  {v : CategoryTheory.Triangulated.K₀ C →+ Λ}
  (σ : CategoryTheory.Triangulated.StabilityCondition.WithClassMap C v)
  (W : Λ →+ ℂ)
  (hW :
    CategoryTheory.Triangulated.stabSeminorm C σ (W - σ.Z) <
      ENNReal.ofReal 1)
  {ε₀ : ℝ} (hε₀ : 0 < ε₀) (hε₀2 : ε₀ < 1 / 4) (hε₀8 : ε₀ < 1 / 8)
  (hsin :
    CategoryTheory.Triangulated.stabSeminorm C σ (W - σ.Z) <
      ENNReal.ofReal (Real.sin (Real.pi * ε₀)))
  {A E : C} {ψ : ℝ}
  (hA :
    CategoryTheory.Triangulated.StabilityCondition.WithClassMap.deformedPred
      C σ W hW ε₀ ψ A)
  (F :
    CategoryTheory.Triangulated.HNFiltration C
      (CategoryTheory.Triangulated.StabilityCondition.WithClassMap.deformedPred
        C σ W hW ε₀)
      E)
  (hlt : ∀ (i : Fin F.n), F.φ i < ψ) (f : A ⟶ E) : f = 0
CategoryTheory.Triangulated.hom_eq_zero_of_gt_phases_deformed.{v,
    u, 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]
  {Λ : Type u'} [AddCommGroup Λ]
  {v :
    CategoryTheory.Triangulated.K₀ C →+ Λ}
  (σ :
    CategoryTheory.Triangulated.StabilityCondition.WithClassMap
      C v)
  (W : Λ →+ ℂ)
  (hW :
    CategoryTheory.Triangulated.stabSeminorm
        C σ (W - σ.Z) <
      ENNReal.ofReal 1)
  {ε₀ : ℝ} (hε₀ : 0 < ε₀)
  (hε₀2 : ε₀ < 1 / 4) (hε₀8 : ε₀ < 1 / 8)
  (hsin :
    CategoryTheory.Triangulated.stabSeminorm
        C σ (W - σ.Z) <
      ENNReal.ofReal
        (Real.sin (Real.pi * ε₀)))
  {A E : C} {ψ : ℝ}
  (hA :
    CategoryTheory.Triangulated.StabilityCondition.WithClassMap.deformedPred
      C σ W hW ε₀ ψ A)
  (F :
    CategoryTheory.Triangulated.HNFiltration
      C
      (CategoryTheory.Triangulated.StabilityCondition.WithClassMap.deformedPred
        C σ W hW ε₀)
      E)
  (hlt : ∀ (i : Fin F.n), F.φ i < ψ)
  (f : A ⟶ E) : f = 0

Something wrong, better idea? Suggest a change

14.23.3. chain_hom_eq_zero_gap_deformed🔗

Any morphism from the k-th chain object of a Q-HN filtration F_X to an object Y admitting a filtration F_Y is zero, provided every phase of F_X is strictly greater than every phase of F_Y. This is the deformedPred analogue of chain_hom_eq_zero_gap.

Proof: Induction on k. Base: E_0 = 0. Inductive step: the Yoneda exact sequence factors the map through the k-th semistable factor of F_X, and hom_eq_zero_of_gt_phases_deformed shows this factor maps to zero into Y.

🔗theorem
CategoryTheory.Triangulated.chain_hom_eq_zero_gap_deformed.{v, u, 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]
  {Λ : Type u'} [AddCommGroup Λ]
  {v : CategoryTheory.Triangulated.K₀ C →+ Λ}
  (σ : CategoryTheory.Triangulated.StabilityCondition.WithClassMap C v)
  (W : Λ →+ ℂ)
  (hW :
    CategoryTheory.Triangulated.stabSeminorm C σ (W - σ.Z) <
      ENNReal.ofReal 1)
  {ε₀ : ℝ} (hε₀ : 0 < ε₀) (hε₀2 : ε₀ < 1 / 4) (hε₀8 : ε₀ < 1 / 8)
  (hsin :
    CategoryTheory.Triangulated.stabSeminorm C σ (W - σ.Z) <
      ENNReal.ofReal (Real.sin (Real.pi * ε₀)))
  {X Y : C}
  (Fx :
    CategoryTheory.Triangulated.HNFiltration C
      (CategoryTheory.Triangulated.StabilityCondition.WithClassMap.deformedPred
        C σ W hW ε₀)
      X)
  (Fy :
    CategoryTheory.Triangulated.HNFiltration C
      (CategoryTheory.Triangulated.StabilityCondition.WithClassMap.deformedPred
        C σ W hW ε₀)
      Y)
  (hgap : ∀ (i : Fin Fx.n) (j : Fin Fy.n), Fy.φ j < Fx.φ i) (k : ℕ)
  (hk : k < Fx.n + 1) (f : Fx.chain.obj ⟨k, hk⟩ ⟶ Y) : f = 0
CategoryTheory.Triangulated.chain_hom_eq_zero_gap_deformed.{v,
    u, 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]
  {Λ : Type u'} [AddCommGroup Λ]
  {v :
    CategoryTheory.Triangulated.K₀ C →+ Λ}
  (σ :
    CategoryTheory.Triangulated.StabilityCondition.WithClassMap
      C v)
  (W : Λ →+ ℂ)
  (hW :
    CategoryTheory.Triangulated.stabSeminorm
        C σ (W - σ.Z) <
      ENNReal.ofReal 1)
  {ε₀ : ℝ} (hε₀ : 0 < ε₀)
  (hε₀2 : ε₀ < 1 / 4) (hε₀8 : ε₀ < 1 / 8)
  (hsin :
    CategoryTheory.Triangulated.stabSeminorm
        C σ (W - σ.Z) <
      ENNReal.ofReal
        (Real.sin (Real.pi * ε₀)))
  {X Y : C}
  (Fx :
    CategoryTheory.Triangulated.HNFiltration
      C
      (CategoryTheory.Triangulated.StabilityCondition.WithClassMap.deformedPred
        C σ W hW ε₀)
      X)
  (Fy :
    CategoryTheory.Triangulated.HNFiltration
      C
      (CategoryTheory.Triangulated.StabilityCondition.WithClassMap.deformedPred
        C σ W hW ε₀)
      Y)
  (hgap :
    ∀ (i : Fin Fx.n) (j : Fin Fy.n),
      Fy.φ j < Fx.φ i)
  (k : ℕ) (hk : k < Fx.n + 1)
  (f : Fx.chain.obj ⟨k, hk⟩ ⟶ Y) : f = 0

Something wrong, better idea? Suggest a change

14.23.4. hom_eq_zero_of_phase_gap_deformed🔗

Morphisms between Q-HN filtered objects with a phase gap are zero: if every phase of F_X is strictly greater than every phase of F_Y, then \operatorname{Hom}(X, Y) = 0.

Proof: Apply chain_hom_eq_zero_gap_deformed at the top of the chain for F_X, using X_n \cong X.

🔗theorem
CategoryTheory.Triangulated.hom_eq_zero_of_phase_gap_deformed.{v, u, 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]
  {Λ : Type u'} [AddCommGroup Λ]
  {v : CategoryTheory.Triangulated.K₀ C →+ Λ}
  (σ : CategoryTheory.Triangulated.StabilityCondition.WithClassMap C v)
  (W : Λ →+ ℂ)
  (hW :
    CategoryTheory.Triangulated.stabSeminorm C σ (W - σ.Z) <
      ENNReal.ofReal 1)
  {ε₀ : ℝ} (hε₀ : 0 < ε₀) (hε₀2 : ε₀ < 1 / 4) (hε₀8 : ε₀ < 1 / 8)
  (hsin :
    CategoryTheory.Triangulated.stabSeminorm C σ (W - σ.Z) <
      ENNReal.ofReal (Real.sin (Real.pi * ε₀)))
  {X Y : C}
  (Fx :
    CategoryTheory.Triangulated.HNFiltration C
      (CategoryTheory.Triangulated.StabilityCondition.WithClassMap.deformedPred
        C σ W hW ε₀)
      X)
  (Fy :
    CategoryTheory.Triangulated.HNFiltration C
      (CategoryTheory.Triangulated.StabilityCondition.WithClassMap.deformedPred
        C σ W hW ε₀)
      Y)
  (hgap : ∀ (i : Fin Fx.n) (j : Fin Fy.n), Fy.φ j < Fx.φ i)
  (f : X ⟶ Y) : f = 0
CategoryTheory.Triangulated.hom_eq_zero_of_phase_gap_deformed.{v,
    u, 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]
  {Λ : Type u'} [AddCommGroup Λ]
  {v :
    CategoryTheory.Triangulated.K₀ C →+ Λ}
  (σ :
    CategoryTheory.Triangulated.StabilityCondition.WithClassMap
      C v)
  (W : Λ →+ ℂ)
  (hW :
    CategoryTheory.Triangulated.stabSeminorm
        C σ (W - σ.Z) <
      ENNReal.ofReal 1)
  {ε₀ : ℝ} (hε₀ : 0 < ε₀)
  (hε₀2 : ε₀ < 1 / 4) (hε₀8 : ε₀ < 1 / 8)
  (hsin :
    CategoryTheory.Triangulated.stabSeminorm
        C σ (W - σ.Z) <
      ENNReal.ofReal
        (Real.sin (Real.pi * ε₀)))
  {X Y : C}
  (Fx :
    CategoryTheory.Triangulated.HNFiltration
      C
      (CategoryTheory.Triangulated.StabilityCondition.WithClassMap.deformedPred
        C σ W hW ε₀)
      X)
  (Fy :
    CategoryTheory.Triangulated.HNFiltration
      C
      (CategoryTheory.Triangulated.StabilityCondition.WithClassMap.deformedPred
        C σ W hW ε₀)
      Y)
  (hgap :
    ∀ (i : Fin Fx.n) (j : Fin Fy.n),
      Fy.φ j < Fx.φ i)
  (f : X ⟶ Y) : f = 0

Something wrong, better idea? Suggest a change

14.23.5. hom_eq_zero_of_enveloped_interval_semistable🔗

Hom vanishing for two interval-semistable objects whose W-phases sit \varepsilon_0 away from the interval boundaries: convert both to deformedPred using the same interval as witness, then apply hom_eq_zero_of_deformedPred.

Proof: Both objects are \operatorname{ssf}-semistable with phases in (a + \varepsilon_0, b - \varepsilon_0), so each is a deformedPred object witnessed by (a, b). Apply Lemma 7.6.

🔗theorem
CategoryTheory.Triangulated.hom_eq_zero_of_enveloped_interval_semistable.{v,
    u, 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]
  {Λ : Type u'} [AddCommGroup Λ]
  {v : CategoryTheory.Triangulated.K₀ C →+ Λ}
  (σ : CategoryTheory.Triangulated.StabilityCondition.WithClassMap C v)
  (W : Λ →+ ℂ)
  (hW :
    CategoryTheory.Triangulated.stabSeminorm C σ (W - σ.Z) <
      ENNReal.ofReal 1)
  {a b ε₀ : ℝ} (hab : a < b) (hε₀ : 0 < ε₀) (hε₀2 : ε₀ < 1 / 4)
  (hε₀8 : ε₀ < 1 / 8) (hthin : b - a + 2 * ε₀ < 1)
  (hsin :
    CategoryTheory.Triangulated.stabSeminorm C σ (W - σ.Z) <
      ENNReal.ofReal (Real.sin (Real.pi * ε₀)))
  (hWindow :
    ∀ {F : C},
      CategoryTheory.Triangulated.Slicing.intervalProp C σ.slicing a b
          F →
        ¬CategoryTheory.Limits.IsZero F →
          a + ε₀ <
              CategoryTheory.Triangulated.wPhaseOf
                (W (CategoryTheory.Triangulated.cl C v F))
                ((a + b) / 2) ∧
            CategoryTheory.Triangulated.wPhaseOf
                (W (CategoryTheory.Triangulated.cl C v F))
                ((a + b) / 2) <
              b - ε₀)
  {E F : C}
  (hE_interval :
    CategoryTheory.Triangulated.Slicing.intervalProp C σ.slicing a b E)
  (hF_interval :
    CategoryTheory.Triangulated.Slicing.intervalProp C σ.slicing a b F)
  (hE :
    CategoryTheory.Triangulated.SkewedStabilityFunction.Semistable C
      (CategoryTheory.Triangulated.StabilityCondition.WithClassMap.skewedStabilityFunction_of_near
        C σ W hW hab)
      E
      (CategoryTheory.Triangulated.wPhaseOf
        (W (CategoryTheory.Triangulated.cl C v E)) ((a + b) / 2)))
  (hF :
    CategoryTheory.Triangulated.SkewedStabilityFunction.Semistable C
      (CategoryTheory.Triangulated.StabilityCondition.WithClassMap.skewedStabilityFunction_of_near
        C σ W hW hab)
      F
      (CategoryTheory.Triangulated.wPhaseOf
        (W (CategoryTheory.Triangulated.cl C v F)) ((a + b) / 2)))
  (hlt :
    CategoryTheory.Triangulated.wPhaseOf
        (W (CategoryTheory.Triangulated.cl C v F)) ((a + b) / 2) <
      CategoryTheory.Triangulated.wPhaseOf
        (W (CategoryTheory.Triangulated.cl C v E)) ((a + b) / 2))
  (f : E ⟶ F) : f = 0
CategoryTheory.Triangulated.hom_eq_zero_of_enveloped_interval_semistable.{v,
    u, 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]
  {Λ : Type u'} [AddCommGroup Λ]
  {v :
    CategoryTheory.Triangulated.K₀ C →+ Λ}
  (σ :
    CategoryTheory.Triangulated.StabilityCondition.WithClassMap
      C v)
  (W : Λ →+ ℂ)
  (hW :
    CategoryTheory.Triangulated.stabSeminorm
        C σ (W - σ.Z) <
      ENNReal.ofReal 1)
  {a b ε₀ : ℝ} (hab : a < b)
  (hε₀ : 0 < ε₀) (hε₀2 : ε₀ < 1 / 4)
  (hε₀8 : ε₀ < 1 / 8)
  (hthin : b - a + 2 * ε₀ < 1)
  (hsin :
    CategoryTheory.Triangulated.stabSeminorm
        C σ (W - σ.Z) <
      ENNReal.ofReal
        (Real.sin (Real.pi * ε₀)))
  (hWindow :
    ∀ {F : C},
      CategoryTheory.Triangulated.Slicing.intervalProp
          C σ.slicing a b F →
        ¬CategoryTheory.Limits.IsZero F →
          a + ε₀ <
              CategoryTheory.Triangulated.wPhaseOf
                (W
                  (CategoryTheory.Triangulated.cl
                    C v F))
                ((a + b) / 2) ∧
            CategoryTheory.Triangulated.wPhaseOf
                (W
                  (CategoryTheory.Triangulated.cl
                    C v F))
                ((a + b) / 2) <
              b - ε₀)
  {E F : C}
  (hE_interval :
    CategoryTheory.Triangulated.Slicing.intervalProp
      C σ.slicing a b E)
  (hF_interval :
    CategoryTheory.Triangulated.Slicing.intervalProp
      C σ.slicing a b F)
  (hE :
    CategoryTheory.Triangulated.SkewedStabilityFunction.Semistable
      C
      (CategoryTheory.Triangulated.StabilityCondition.WithClassMap.skewedStabilityFunction_of_near
        C σ W hW hab)
      E
      (CategoryTheory.Triangulated.wPhaseOf
        (W
          (CategoryTheory.Triangulated.cl
            C v E))
        ((a + b) / 2)))
  (hF :
    CategoryTheory.Triangulated.SkewedStabilityFunction.Semistable
      C
      (CategoryTheory.Triangulated.StabilityCondition.WithClassMap.skewedStabilityFunction_of_near
        C σ W hW hab)
      F
      (CategoryTheory.Triangulated.wPhaseOf
        (W
          (CategoryTheory.Triangulated.cl
            C v F))
        ((a + b) / 2)))
  (hlt :
    CategoryTheory.Triangulated.wPhaseOf
        (W
          (CategoryTheory.Triangulated.cl
            C v F))
        ((a + b) / 2) <
      CategoryTheory.Triangulated.wPhaseOf
        (W
          (CategoryTheory.Triangulated.cl
            C v E))
        ((a + b) / 2))
  (f : E ⟶ F) : f = 0

Something wrong, better idea? Suggest a change

14.23.6. exists_deformedHN_of_enveloped_interval🔗

Lemma 7.7 for the deformed slicing: if a thin interval carries strict finite length and every nonzero object has W-phase at least \varepsilon_0 away from the boundaries, then every nonzero interval object admits a Q-HN filtration with phases in (a + \varepsilon_0, b - \varepsilon_0).

Proof: Apply hn_exists_in_thin_interval with L = a + \varepsilon_0, U = b - \varepsilon_0, Hom vanishing from hom_eq_zero_of_enveloped_interval_semistable, and destabilizing bound from the window hypothesis. Retype the \operatorname{ssf}-semistable factors as deformedPred using the interval (a, b) as witness.

🔗theorem
CategoryTheory.Triangulated.exists_deformedHN_of_enveloped_interval.{v,
    u, 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]
  {Λ : Type u'} [AddCommGroup Λ]
  {v : CategoryTheory.Triangulated.K₀ C →+ Λ}
  (σ : CategoryTheory.Triangulated.StabilityCondition.WithClassMap C v)
  (W : Λ →+ ℂ)
  (hW :
    CategoryTheory.Triangulated.stabSeminorm C σ (W - σ.Z) <
      ENNReal.ofReal 1)
  {a b ε₀ : ℝ} (hab : a < b) [Fact (a < b)] [Fact (b - a ≤ 1)]
  (hFiniteLength :
    CategoryTheory.Triangulated.ThinFiniteLengthInInterval C σ a b)
  (hε₀ : 0 < ε₀) (hε₀2 : ε₀ < 1 / 4) (hε₀8 : ε₀ < 1 / 8)
  (hthin : b - a + 2 * ε₀ < 1)
  (hsin :
    CategoryTheory.Triangulated.stabSeminorm C σ (W - σ.Z) <
      ENNReal.ofReal (Real.sin (Real.pi * ε₀)))
  (hW_interval :
    ∀ {F : C},
      CategoryTheory.Triangulated.Slicing.intervalProp C σ.slicing a b
          F →
        ¬CategoryTheory.Limits.IsZero F →
          W (CategoryTheory.Triangulated.cl C v F) ≠ 0)
  (hWindow :
    ∀ {F : C},
      CategoryTheory.Triangulated.Slicing.intervalProp C σ.slicing a b
          F →
        ¬CategoryTheory.Limits.IsZero F →
          a + ε₀ <
              CategoryTheory.Triangulated.wPhaseOf
                (W (CategoryTheory.Triangulated.cl C v F))
                ((a + b) / 2) ∧
            CategoryTheory.Triangulated.wPhaseOf
                (W (CategoryTheory.Triangulated.cl C v F))
                ((a + b) / 2) <
              b - ε₀)
  {X : CategoryTheory.Triangulated.Slicing.IntervalCat C σ.slicing a b}
  (hX : ¬CategoryTheory.Limits.IsZero X) :
  ∃ G, ∀ (j : Fin G.n), a + ε₀ < G.φ j ∧ G.φ j < b - ε₀
CategoryTheory.Triangulated.exists_deformedHN_of_enveloped_interval.{v,
    u, 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]
  {Λ : Type u'} [AddCommGroup Λ]
  {v :
    CategoryTheory.Triangulated.K₀ C →+ Λ}
  (σ :
    CategoryTheory.Triangulated.StabilityCondition.WithClassMap
      C v)
  (W : Λ →+ ℂ)
  (hW :
    CategoryTheory.Triangulated.stabSeminorm
        C σ (W - σ.Z) <
      ENNReal.ofReal 1)
  {a b ε₀ : ℝ} (hab : a < b)
  [Fact (a < b)] [Fact (b - a ≤ 1)]
  (hFiniteLength :
    CategoryTheory.Triangulated.ThinFiniteLengthInInterval
      C σ a b)
  (hε₀ : 0 < ε₀) (hε₀2 : ε₀ < 1 / 4)
  (hε₀8 : ε₀ < 1 / 8)
  (hthin : b - a + 2 * ε₀ < 1)
  (hsin :
    CategoryTheory.Triangulated.stabSeminorm
        C σ (W - σ.Z) <
      ENNReal.ofReal
        (Real.sin (Real.pi * ε₀)))
  (hW_interval :
    ∀ {F : C},
      CategoryTheory.Triangulated.Slicing.intervalProp
          C σ.slicing a b F →
        ¬CategoryTheory.Limits.IsZero F →
          W
              (CategoryTheory.Triangulated.cl
                C v F) ≠
            0)
  (hWindow :
    ∀ {F : C},
      CategoryTheory.Triangulated.Slicing.intervalProp
          C σ.slicing a b F →
        ¬CategoryTheory.Limits.IsZero F →
          a + ε₀ <
              CategoryTheory.Triangulated.wPhaseOf
                (W
                  (CategoryTheory.Triangulated.cl
                    C v F))
                ((a + b) / 2) ∧
            CategoryTheory.Triangulated.wPhaseOf
                (W
                  (CategoryTheory.Triangulated.cl
                    C v F))
                ((a + b) / 2) <
              b - ε₀)
  {X :
    CategoryTheory.Triangulated.Slicing.IntervalCat
      C σ.slicing a b}
  (hX : ¬CategoryTheory.Limits.IsZero X) :
  ∃ G,
    ∀ (j : Fin G.n),
      a + ε₀ < G.φ j ∧ G.φ j < b - ε₀

Something wrong, better idea? Suggest a change

14.23.7. deformedGtGen🔗

Generators of Q(> t): Q-semistable objects with some phase \psi > t (Bridgeland Node 7.8a).

Construction: Defined as E \mapsto \exists \psi,\, t < \psi \wedge \operatorname{deformedPred}(\psi, E).

🔗def
CategoryTheory.Triangulated.StabilityCondition.WithClassMap.deformedGtGen.{v,
    u, 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]
  {Λ : Type u'} [AddCommGroup Λ]
  {v : CategoryTheory.Triangulated.K₀ C →+ Λ}
  (σ : CategoryTheory.Triangulated.StabilityCondition.WithClassMap C v)
  (W : Λ →+ ℂ)
  (hW :
    CategoryTheory.Triangulated.stabSeminorm C σ (W - σ.Z) <
      ENNReal.ofReal 1)
  (ε₀ t : ℝ) : CategoryTheory.ObjectProperty C
CategoryTheory.Triangulated.StabilityCondition.WithClassMap.deformedGtGen.{v,
    u, 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]
  {Λ : Type u'} [AddCommGroup Λ]
  {v :
    CategoryTheory.Triangulated.K₀ C →+ Λ}
  (σ :
    CategoryTheory.Triangulated.StabilityCondition.WithClassMap
      C v)
  (W : Λ →+ ℂ)
  (hW :
    CategoryTheory.Triangulated.stabSeminorm
        C σ (W - σ.Z) <
      ENNReal.ofReal 1)
  (ε₀ t : ℝ) :
  CategoryTheory.ObjectProperty C

Something wrong, better idea? Suggest a change

14.23.8. deformedLeGen🔗

Generators of Q(\le t): Q-semistable objects with some phase \psi \le t (Bridgeland Node 7.8a).

Construction: Defined as E \mapsto \exists \psi,\, \psi \le t \wedge \operatorname{deformedPred}(\psi, E).

🔗def
CategoryTheory.Triangulated.StabilityCondition.WithClassMap.deformedLeGen.{v,
    u, 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]
  {Λ : Type u'} [AddCommGroup Λ]
  {v : CategoryTheory.Triangulated.K₀ C →+ Λ}
  (σ : CategoryTheory.Triangulated.StabilityCondition.WithClassMap C v)
  (W : Λ →+ ℂ)
  (hW :
    CategoryTheory.Triangulated.stabSeminorm C σ (W - σ.Z) <
      ENNReal.ofReal 1)
  (ε₀ t : ℝ) : CategoryTheory.ObjectProperty C
CategoryTheory.Triangulated.StabilityCondition.WithClassMap.deformedLeGen.{v,
    u, 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]
  {Λ : Type u'} [AddCommGroup Λ]
  {v :
    CategoryTheory.Triangulated.K₀ C →+ Λ}
  (σ :
    CategoryTheory.Triangulated.StabilityCondition.WithClassMap
      C v)
  (W : Λ →+ ℂ)
  (hW :
    CategoryTheory.Triangulated.stabSeminorm
        C σ (W - σ.Z) <
      ENNReal.ofReal 1)
  (ε₀ t : ℝ) :
  CategoryTheory.ObjectProperty C

Something wrong, better idea? Suggest a change

14.23.9. deformedLtGen🔗

Generators of Q(< t): Q-semistable objects with some phase \psi < t (Bridgeland Node 7.8a / 7.9).

Construction: Defined as E \mapsto \exists \psi,\, \psi < t \wedge \operatorname{deformedPred}(\psi, E).

🔗def
CategoryTheory.Triangulated.StabilityCondition.WithClassMap.deformedLtGen.{v,
    u, 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]
  {Λ : Type u'} [AddCommGroup Λ]
  {v : CategoryTheory.Triangulated.K₀ C →+ Λ}
  (σ : CategoryTheory.Triangulated.StabilityCondition.WithClassMap C v)
  (W : Λ →+ ℂ)
  (hW :
    CategoryTheory.Triangulated.stabSeminorm C σ (W - σ.Z) <
      ENNReal.ofReal 1)
  (ε₀ t : ℝ) : CategoryTheory.ObjectProperty C
CategoryTheory.Triangulated.StabilityCondition.WithClassMap.deformedLtGen.{v,
    u, 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]
  {Λ : Type u'} [AddCommGroup Λ]
  {v :
    CategoryTheory.Triangulated.K₀ C →+ Λ}
  (σ :
    CategoryTheory.Triangulated.StabilityCondition.WithClassMap
      C v)
  (W : Λ →+ ℂ)
  (hW :
    CategoryTheory.Triangulated.stabSeminorm
        C σ (W - σ.Z) <
      ENNReal.ofReal 1)
  (ε₀ t : ℝ) :
  CategoryTheory.ObjectProperty C

Something wrong, better idea? Suggest a change

14.23.10. deformedGtPred🔗

Q(> t): the extension-closed subcategory generated by the Q(\psi) with \psi > t (Bridgeland p.6, Node 7.8a).

Construction: The extension closure of deformedGtGen: the smallest extension-closed subcategory containing all Q-semistable objects of phase > t.

🔗def
CategoryTheory.Triangulated.StabilityCondition.WithClassMap.deformedGtPred.{v,
    u, 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]
  {Λ : Type u'} [AddCommGroup Λ]
  {v : CategoryTheory.Triangulated.K₀ C →+ Λ}
  (σ : CategoryTheory.Triangulated.StabilityCondition.WithClassMap C v)
  (W : Λ →+ ℂ)
  (hW :
    CategoryTheory.Triangulated.stabSeminorm C σ (W - σ.Z) <
      ENNReal.ofReal 1)
  (ε₀ t : ℝ) : CategoryTheory.ObjectProperty C
CategoryTheory.Triangulated.StabilityCondition.WithClassMap.deformedGtPred.{v,
    u, 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]
  {Λ : Type u'} [AddCommGroup Λ]
  {v :
    CategoryTheory.Triangulated.K₀ C →+ Λ}
  (σ :
    CategoryTheory.Triangulated.StabilityCondition.WithClassMap
      C v)
  (W : Λ →+ ℂ)
  (hW :
    CategoryTheory.Triangulated.stabSeminorm
        C σ (W - σ.Z) <
      ENNReal.ofReal 1)
  (ε₀ t : ℝ) :
  CategoryTheory.ObjectProperty C

Something wrong, better idea? Suggest a change

14.23.11. deformedLePred🔗

Q(\le t): the extension-closed subcategory generated by the Q(\psi) with \psi \le t (Bridgeland p.6, Node 7.8a).

Construction: The extension closure of deformedLeGen: the smallest extension-closed subcategory containing all Q-semistable objects of phase \le t.

🔗def
CategoryTheory.Triangulated.StabilityCondition.WithClassMap.deformedLePred.{v,
    u, 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]
  {Λ : Type u'} [AddCommGroup Λ]
  {v : CategoryTheory.Triangulated.K₀ C →+ Λ}
  (σ : CategoryTheory.Triangulated.StabilityCondition.WithClassMap C v)
  (W : Λ →+ ℂ)
  (hW :
    CategoryTheory.Triangulated.stabSeminorm C σ (W - σ.Z) <
      ENNReal.ofReal 1)
  (ε₀ t : ℝ) : CategoryTheory.ObjectProperty C
CategoryTheory.Triangulated.StabilityCondition.WithClassMap.deformedLePred.{v,
    u, 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]
  {Λ : Type u'} [AddCommGroup Λ]
  {v :
    CategoryTheory.Triangulated.K₀ C →+ Λ}
  (σ :
    CategoryTheory.Triangulated.StabilityCondition.WithClassMap
      C v)
  (W : Λ →+ ℂ)
  (hW :
    CategoryTheory.Triangulated.stabSeminorm
        C σ (W - σ.Z) <
      ENNReal.ofReal 1)
  (ε₀ t : ℝ) :
  CategoryTheory.ObjectProperty C

Something wrong, better idea? Suggest a change

14.23.12. deformedLtPred🔗

Q(< t): the extension-closed subcategory generated by the Q(\psi) with \psi < t (Bridgeland p.6, Node 7.8a / 7.9).

Construction: The extension closure of deformedLtGen: the smallest extension-closed subcategory containing all Q-semistable objects of phase < t.

🔗def
CategoryTheory.Triangulated.StabilityCondition.WithClassMap.deformedLtPred.{v,
    u, 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]
  {Λ : Type u'} [AddCommGroup Λ]
  {v : CategoryTheory.Triangulated.K₀ C →+ Λ}
  (σ : CategoryTheory.Triangulated.StabilityCondition.WithClassMap C v)
  (W : Λ →+ ℂ)
  (hW :
    CategoryTheory.Triangulated.stabSeminorm C σ (W - σ.Z) <
      ENNReal.ofReal 1)
  (ε₀ t : ℝ) : CategoryTheory.ObjectProperty C
CategoryTheory.Triangulated.StabilityCondition.WithClassMap.deformedLtPred.{v,
    u, 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]
  {Λ : Type u'} [AddCommGroup Λ]
  {v :
    CategoryTheory.Triangulated.K₀ C →+ Λ}
  (σ :
    CategoryTheory.Triangulated.StabilityCondition.WithClassMap
      C v)
  (W : Λ →+ ℂ)
  (hW :
    CategoryTheory.Triangulated.stabSeminorm
        C σ (W - σ.Z) <
      ENNReal.ofReal 1)
  (ε₀ t : ℝ) :
  CategoryTheory.ObjectProperty C

Something wrong, better idea? Suggest a change

14.23.13. deformedLePred_mono🔗

Monotonicity of Q(\le t): if t_1 \le t_2 then Q(\le t_1) \subseteq Q(\le t_2).

Proof: If \psi \le t_1 \le t_2, then \psi \le t_2. Apply ExtensionClosure.mono.

🔗theorem
CategoryTheory.Triangulated.StabilityCondition.WithClassMap.deformedLePred_mono.{v,
    u, 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]
  {Λ : Type u'} [AddCommGroup Λ]
  {v : CategoryTheory.Triangulated.K₀ C →+ Λ}
  (σ : CategoryTheory.Triangulated.StabilityCondition.WithClassMap C v)
  (W : Λ →+ ℂ)
  (hW :
    CategoryTheory.Triangulated.stabSeminorm C σ (W - σ.Z) <
      ENNReal.ofReal 1)
  {ε₀ t₁ t₂ : ℝ} (ht : t₁ ≤ t₂) :
  CategoryTheory.Triangulated.StabilityCondition.WithClassMap.deformedLePred
      C σ W hW ε₀ t₁ ≤
    CategoryTheory.Triangulated.StabilityCondition.WithClassMap.deformedLePred
      C σ W hW ε₀ t₂
CategoryTheory.Triangulated.StabilityCondition.WithClassMap.deformedLePred_mono.{v,
    u, 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]
  {Λ : Type u'} [AddCommGroup Λ]
  {v :
    CategoryTheory.Triangulated.K₀ C →+ Λ}
  (σ :
    CategoryTheory.Triangulated.StabilityCondition.WithClassMap
      C v)
  (W : Λ →+ ℂ)
  (hW :
    CategoryTheory.Triangulated.stabSeminorm
        C σ (W - σ.Z) <
      ENNReal.ofReal 1)
  {ε₀ t₁ t₂ : ℝ} (ht : t₁ ≤ t₂) :
  CategoryTheory.Triangulated.StabilityCondition.WithClassMap.deformedLePred
      C σ W hW ε₀ t₁ ≤
    CategoryTheory.Triangulated.StabilityCondition.WithClassMap.deformedLePred
      C σ W hW ε₀ t₂

Something wrong, better idea? Suggest a change

14.23.14. deformedLtPred_mono🔗

Monotonicity of Q(< t): if t_1 \le t_2 then Q(< t_1) \subseteq Q(< t_2).

Proof: If \psi < t_1 \le t_2, then \psi < t_2. Apply ExtensionClosure.mono.

🔗theorem
CategoryTheory.Triangulated.StabilityCondition.WithClassMap.deformedLtPred_mono.{v,
    u, 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]
  {Λ : Type u'} [AddCommGroup Λ]
  {v : CategoryTheory.Triangulated.K₀ C →+ Λ}
  (σ : CategoryTheory.Triangulated.StabilityCondition.WithClassMap C v)
  (W : Λ →+ ℂ)
  (hW :
    CategoryTheory.Triangulated.stabSeminorm C σ (W - σ.Z) <
      ENNReal.ofReal 1)
  {ε₀ t₁ t₂ : ℝ} (ht : t₁ ≤ t₂) :
  CategoryTheory.Triangulated.StabilityCondition.WithClassMap.deformedLtPred
      C σ W hW ε₀ t₁ ≤
    CategoryTheory.Triangulated.StabilityCondition.WithClassMap.deformedLtPred
      C σ W hW ε₀ t₂
CategoryTheory.Triangulated.StabilityCondition.WithClassMap.deformedLtPred_mono.{v,
    u, 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]
  {Λ : Type u'} [AddCommGroup Λ]
  {v :
    CategoryTheory.Triangulated.K₀ C →+ Λ}
  (σ :
    CategoryTheory.Triangulated.StabilityCondition.WithClassMap
      C v)
  (W : Λ →+ ℂ)
  (hW :
    CategoryTheory.Triangulated.stabSeminorm
        C σ (W - σ.Z) <
      ENNReal.ofReal 1)
  {ε₀ t₁ t₂ : ℝ} (ht : t₁ ≤ t₂) :
  CategoryTheory.Triangulated.StabilityCondition.WithClassMap.deformedLtPred
      C σ W hW ε₀ t₁ ≤
    CategoryTheory.Triangulated.StabilityCondition.WithClassMap.deformedLtPred
      C σ W hW ε₀ t₂

Something wrong, better idea? Suggest a change

14.23.15. deformedLePred_of_deformedLtPred🔗

Any Q(< t)-object is in Q(\le t): \psi < t implies \psi \le t.

Proof: Immediate from ExtensionClosure.mono applied to the weakening \psi < t \implies \psi \le t.

🔗theorem
CategoryTheory.Triangulated.StabilityCondition.WithClassMap.deformedLePred_of_deformedLtPred.{v,
    u, 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]
  {Λ : Type u'} [AddCommGroup Λ]
  {v : CategoryTheory.Triangulated.K₀ C →+ Λ}
  (σ : CategoryTheory.Triangulated.StabilityCondition.WithClassMap C v)
  (W : Λ →+ ℂ)
  (hW :
    CategoryTheory.Triangulated.stabSeminorm C σ (W - σ.Z) <
      ENNReal.ofReal 1)
  {ε₀ t : ℝ} :
  CategoryTheory.Triangulated.StabilityCondition.WithClassMap.deformedLtPred
      C σ W hW ε₀ t ≤
    CategoryTheory.Triangulated.StabilityCondition.WithClassMap.deformedLePred
      C σ W hW ε₀ t
CategoryTheory.Triangulated.StabilityCondition.WithClassMap.deformedLePred_of_deformedLtPred.{v,
    u, 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]
  {Λ : Type u'} [AddCommGroup Λ]
  {v :
    CategoryTheory.Triangulated.K₀ C →+ Λ}
  (σ :
    CategoryTheory.Triangulated.StabilityCondition.WithClassMap
      C v)
  (W : Λ →+ ℂ)
  (hW :
    CategoryTheory.Triangulated.stabSeminorm
        C σ (W - σ.Z) <
      ENNReal.ofReal 1)
  {ε₀ t : ℝ} :
  CategoryTheory.Triangulated.StabilityCondition.WithClassMap.deformedLtPred
      C σ W hW ε₀ t ≤
    CategoryTheory.Triangulated.StabilityCondition.WithClassMap.deformedLePred
      C σ W hW ε₀ t

Something wrong, better idea? Suggest a change

14.23.16. deformedGtPred_anti🔗

Anti-monotonicity of Q(> t): if t_1 \le t_2 then Q(> t_2) \subseteq Q(> t_1).

Proof: If t_2 < \psi and t_1 \le t_2, then t_1 < \psi. Apply ExtensionClosure.mono.

🔗theorem
CategoryTheory.Triangulated.StabilityCondition.WithClassMap.deformedGtPred_anti.{v,
    u, 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]
  {Λ : Type u'} [AddCommGroup Λ]
  {v : CategoryTheory.Triangulated.K₀ C →+ Λ}
  (σ : CategoryTheory.Triangulated.StabilityCondition.WithClassMap C v)
  (W : Λ →+ ℂ)
  (hW :
    CategoryTheory.Triangulated.stabSeminorm C σ (W - σ.Z) <
      ENNReal.ofReal 1)
  {ε₀ t₁ t₂ : ℝ} (ht : t₁ ≤ t₂) :
  CategoryTheory.Triangulated.StabilityCondition.WithClassMap.deformedGtPred
      C σ W hW ε₀ t₂ ≤
    CategoryTheory.Triangulated.StabilityCondition.WithClassMap.deformedGtPred
      C σ W hW ε₀ t₁
CategoryTheory.Triangulated.StabilityCondition.WithClassMap.deformedGtPred_anti.{v,
    u, 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]
  {Λ : Type u'} [AddCommGroup Λ]
  {v :
    CategoryTheory.Triangulated.K₀ C →+ Λ}
  (σ :
    CategoryTheory.Triangulated.StabilityCondition.WithClassMap
      C v)
  (W : Λ →+ ℂ)
  (hW :
    CategoryTheory.Triangulated.stabSeminorm
        C σ (W - σ.Z) <
      ENNReal.ofReal 1)
  {ε₀ t₁ t₂ : ℝ} (ht : t₁ ≤ t₂) :
  CategoryTheory.Triangulated.StabilityCondition.WithClassMap.deformedGtPred
      C σ W hW ε₀ t₂ ≤
    CategoryTheory.Triangulated.StabilityCondition.WithClassMap.deformedGtPred
      C σ W hW ε₀ t₁

Something wrong, better idea? Suggest a change

14.23.17. hom_eq_zero_of_deformedGt_deformedLe🔗

Orthogonality of Q(> t) and Q(\le t) (Node 7.8b). Every morphism from a Q(> t)-object to a Q(\le t)-object is zero.

Proof: By ExtensionClosure.hom_eq_zero: it suffices to check generators. For generators A \in Q(\psi_1) with \psi_1 > t and B \in Q(\psi_2) with \psi_2 \le t, the phase gap \psi_2 < \psi_1 gives \operatorname{Hom}(A, B) = 0 by hom_eq_zero_of_deformedPred.

🔗theorem
CategoryTheory.Triangulated.StabilityCondition.WithClassMap.hom_eq_zero_of_deformedGt_deformedLe.{v,
    u, 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]
  {Λ : Type u'} [AddCommGroup Λ]
  {v : CategoryTheory.Triangulated.K₀ C →+ Λ}
  (σ : CategoryTheory.Triangulated.StabilityCondition.WithClassMap C v)
  (W : Λ →+ ℂ)
  (hW :
    CategoryTheory.Triangulated.stabSeminorm C σ (W - σ.Z) <
      ENNReal.ofReal 1)
  {ε₀ : ℝ} (hε₀ : 0 < ε₀) (hε₀2 : ε₀ < 1 / 4) (hε₀8 : ε₀ < 1 / 8)
  (hsin :
    CategoryTheory.Triangulated.stabSeminorm C σ (W - σ.Z) <
      ENNReal.ofReal (Real.sin (Real.pi * ε₀)))
  {E F : C} {t : ℝ}
  (hE :
    CategoryTheory.Triangulated.StabilityCondition.WithClassMap.deformedGtPred
      C σ W hW ε₀ t E)
  (hF :
    CategoryTheory.Triangulated.StabilityCondition.WithClassMap.deformedLePred
      C σ W hW ε₀ t F)
  (f : E ⟶ F) : f = 0
CategoryTheory.Triangulated.StabilityCondition.WithClassMap.hom_eq_zero_of_deformedGt_deformedLe.{v,
    u, 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]
  {Λ : Type u'} [AddCommGroup Λ]
  {v :
    CategoryTheory.Triangulated.K₀ C →+ Λ}
  (σ :
    CategoryTheory.Triangulated.StabilityCondition.WithClassMap
      C v)
  (W : Λ →+ ℂ)
  (hW :
    CategoryTheory.Triangulated.stabSeminorm
        C σ (W - σ.Z) <
      ENNReal.ofReal 1)
  {ε₀ : ℝ} (hε₀ : 0 < ε₀)
  (hε₀2 : ε₀ < 1 / 4) (hε₀8 : ε₀ < 1 / 8)
  (hsin :
    CategoryTheory.Triangulated.stabSeminorm
        C σ (W - σ.Z) <
      ENNReal.ofReal
        (Real.sin (Real.pi * ε₀)))
  {E F : C} {t : ℝ}
  (hE :
    CategoryTheory.Triangulated.StabilityCondition.WithClassMap.deformedGtPred
      C σ W hW ε₀ t E)
  (hF :
    CategoryTheory.Triangulated.StabilityCondition.WithClassMap.deformedLePred
      C σ W hW ε₀ t F)
  (f : E ⟶ F) : f = 0

Something wrong, better idea? Suggest a change

14.23.18. hom_eq_zero_of_deformedGt_deformedLt🔗

Orthogonality of Q(> t) and Q(< t): every morphism from a Q(> t)-object to a Q(< t)-object is zero.

Proof: Same as hom_eq_zero_of_deformedGt_deformedLe but with strict inequality on both sides.

🔗theorem
CategoryTheory.Triangulated.StabilityCondition.WithClassMap.hom_eq_zero_of_deformedGt_deformedLt.{v,
    u, 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]
  {Λ : Type u'} [AddCommGroup Λ]
  {v : CategoryTheory.Triangulated.K₀ C →+ Λ}
  (σ : CategoryTheory.Triangulated.StabilityCondition.WithClassMap C v)
  (W : Λ →+ ℂ)
  (hW :
    CategoryTheory.Triangulated.stabSeminorm C σ (W - σ.Z) <
      ENNReal.ofReal 1)
  {ε₀ : ℝ} (hε₀ : 0 < ε₀) (hε₀2 : ε₀ < 1 / 4) (hε₀8 : ε₀ < 1 / 8)
  (hsin :
    CategoryTheory.Triangulated.stabSeminorm C σ (W - σ.Z) <
      ENNReal.ofReal (Real.sin (Real.pi * ε₀)))
  {E F : C} {t : ℝ}
  (hE :
    CategoryTheory.Triangulated.StabilityCondition.WithClassMap.deformedGtPred
      C σ W hW ε₀ t E)
  (hF :
    CategoryTheory.Triangulated.StabilityCondition.WithClassMap.deformedLtPred
      C σ W hW ε₀ t F)
  (f : E ⟶ F) : f = 0
CategoryTheory.Triangulated.StabilityCondition.WithClassMap.hom_eq_zero_of_deformedGt_deformedLt.{v,
    u, 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]
  {Λ : Type u'} [AddCommGroup Λ]
  {v :
    CategoryTheory.Triangulated.K₀ C →+ Λ}
  (σ :
    CategoryTheory.Triangulated.StabilityCondition.WithClassMap
      C v)
  (W : Λ →+ ℂ)
  (hW :
    CategoryTheory.Triangulated.stabSeminorm
        C σ (W - σ.Z) <
      ENNReal.ofReal 1)
  {ε₀ : ℝ} (hε₀ : 0 < ε₀)
  (hε₀2 : ε₀ < 1 / 4) (hε₀8 : ε₀ < 1 / 8)
  (hsin :
    CategoryTheory.Triangulated.stabSeminorm
        C σ (W - σ.Z) <
      ENNReal.ofReal
        (Real.sin (Real.pi * ε₀)))
  {E F : C} {t : ℝ}
  (hE :
    CategoryTheory.Triangulated.StabilityCondition.WithClassMap.deformedGtPred
      C σ W hW ε₀ t E)
  (hF :
    CategoryTheory.Triangulated.StabilityCondition.WithClassMap.deformedLtPred
      C σ W hW ε₀ t F)
  (f : E ⟶ F) : f = 0

Something wrong, better idea? Suggest a change

14.23.19. exists_deformedGt_deformedLe_triangle_of_hn🔗

A Q-HN filtration split at cutoff t gives a distinguished triangle whose two pieces lie in Q(> t) and Q(\le t).

Proof: Apply split_hn_filtration_at_cutoff to the Q-HN filtration. The factors with phase > t generate Q(> t) via extension closure, and those with phase \le t generate Q(\le t).

🔗theorem
CategoryTheory.Triangulated.exists_deformedGt_deformedLe_triangle_of_hn.{v,
    u, 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]
  {Λ : Type u'} [AddCommGroup Λ]
  {v : CategoryTheory.Triangulated.K₀ C →+ Λ}
  (σ : CategoryTheory.Triangulated.StabilityCondition.WithClassMap C v)
  (W : Λ →+ ℂ)
  (hW :
    CategoryTheory.Triangulated.stabSeminorm C σ (W - σ.Z) <
      ENNReal.ofReal 1)
  {ε₀ : ℝ} {E : C}
  (G :
    CategoryTheory.Triangulated.HNFiltration C
      (CategoryTheory.Triangulated.StabilityCondition.WithClassMap.deformedPred
        C σ W hW ε₀)
      E)
  (t : ℝ) :
  ∃ X Y f g h,
    CategoryTheory.Pretriangulated.Triangle.mk f g h ∈
        CategoryTheory.Pretriangulated.distinguishedTriangles ∧
      CategoryTheory.Triangulated.StabilityCondition.WithClassMap.deformedGtPred
          C σ W hW ε₀ t X ∧
        CategoryTheory.Triangulated.StabilityCondition.WithClassMap.deformedLePred
          C σ W hW ε₀ t Y
CategoryTheory.Triangulated.exists_deformedGt_deformedLe_triangle_of_hn.{v,
    u, 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]
  {Λ : Type u'} [AddCommGroup Λ]
  {v :
    CategoryTheory.Triangulated.K₀ C →+ Λ}
  (σ :
    CategoryTheory.Triangulated.StabilityCondition.WithClassMap
      C v)
  (W : Λ →+ ℂ)
  (hW :
    CategoryTheory.Triangulated.stabSeminorm
        C σ (W - σ.Z) <
      ENNReal.ofReal 1)
  {ε₀ : ℝ} {E : C}
  (G :
    CategoryTheory.Triangulated.HNFiltration
      C
      (CategoryTheory.Triangulated.StabilityCondition.WithClassMap.deformedPred
        C σ W hW ε₀)
      E)
  (t : ℝ) :
  ∃ X Y f g h,
    CategoryTheory.Pretriangulated.Triangle.mk
          f g h ∈
        CategoryTheory.Pretriangulated.distinguishedTriangles ∧
      CategoryTheory.Triangulated.StabilityCondition.WithClassMap.deformedGtPred
          C σ W hW ε₀ t X ∧
        CategoryTheory.Triangulated.StabilityCondition.WithClassMap.deformedLePred
          C σ W hW ε₀ t Y

Something wrong, better idea? Suggest a change

14.23.20. exists_deformedGt_deformedLt_triangle_of_hn🔗

A Q-HN filtration split at cutoff t gives a distinguished triangle whose two pieces lie in Q(> t) and Q(< t), when no factor has phase exactly t.

Proof: Same as exists_deformedGt_deformedLe_triangle_of_hn but with strict inequality: the \le t piece has all phases < t when t is not a phase of any factor.

🔗theorem
CategoryTheory.Triangulated.exists_deformedGt_deformedLt_triangle_of_hn.{v,
    u, 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]
  {Λ : Type u'} [AddCommGroup Λ]
  {v : CategoryTheory.Triangulated.K₀ C →+ Λ}
  (σ : CategoryTheory.Triangulated.StabilityCondition.WithClassMap C v)
  (W : Λ →+ ℂ)
  (hW :
    CategoryTheory.Triangulated.stabSeminorm C σ (W - σ.Z) <
      ENNReal.ofReal 1)
  {ε₀ : ℝ} {E : C}
  (G :
    CategoryTheory.Triangulated.HNFiltration C
      (CategoryTheory.Triangulated.StabilityCondition.WithClassMap.deformedPred
        C σ W hW ε₀)
      E)
  (t δ : ℝ) (hδ : 0 < δ) :
  ∃ X Y f g h,
    CategoryTheory.Pretriangulated.Triangle.mk f g h ∈
        CategoryTheory.Pretriangulated.distinguishedTriangles ∧
      CategoryTheory.Triangulated.StabilityCondition.WithClassMap.deformedGtPred
          C σ W hW ε₀ t X ∧
        CategoryTheory.Triangulated.StabilityCondition.WithClassMap.deformedLtPred
          C σ W hW ε₀ (t + δ) Y
CategoryTheory.Triangulated.exists_deformedGt_deformedLt_triangle_of_hn.{v,
    u, 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]
  {Λ : Type u'} [AddCommGroup Λ]
  {v :
    CategoryTheory.Triangulated.K₀ C →+ Λ}
  (σ :
    CategoryTheory.Triangulated.StabilityCondition.WithClassMap
      C v)
  (W : Λ →+ ℂ)
  (hW :
    CategoryTheory.Triangulated.stabSeminorm
        C σ (W - σ.Z) <
      ENNReal.ofReal 1)
  {ε₀ : ℝ} {E : C}
  (G :
    CategoryTheory.Triangulated.HNFiltration
      C
      (CategoryTheory.Triangulated.StabilityCondition.WithClassMap.deformedPred
        C σ W hW ε₀)
      E)
  (t δ : ℝ) (hδ : 0 < δ) :
  ∃ X Y f g h,
    CategoryTheory.Pretriangulated.Triangle.mk
          f g h ∈
        CategoryTheory.Pretriangulated.distinguishedTriangles ∧
      CategoryTheory.Triangulated.StabilityCondition.WithClassMap.deformedGtPred
          C σ W hW ε₀ t X ∧
        CategoryTheory.Triangulated.StabilityCondition.WithClassMap.deformedLtPred
          C σ W hW ε₀ (t + δ) Y

Something wrong, better idea? Suggest a change

14.23.21. exists_deformedGt_deformedLe_triangle_of_enveloped_interval🔗

For any nonzero interval object E in a thin finite-length interval with the W-phase envelope condition, there exists a distinguished triangle X \to E \to Y \to X[1] with X \in Q(> t) and Y \in Q(\le t).

Proof: First construct the Q-HN filtration via exists_deformedHN_of_enveloped_interval, then apply exists_deformedGt_deformedLe_triangle_of_hn at cutoff t.

🔗theorem
CategoryTheory.Triangulated.exists_deformedGt_deformedLe_triangle_of_enveloped_interval.{v,
    u, 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]
  {Λ : Type u'} [AddCommGroup Λ]
  {v : CategoryTheory.Triangulated.K₀ C →+ Λ}
  (σ : CategoryTheory.Triangulated.StabilityCondition.WithClassMap C v)
  (W : Λ →+ ℂ)
  (hW :
    CategoryTheory.Triangulated.stabSeminorm C σ (W - σ.Z) <
      ENNReal.ofReal 1)
  {a b ε₀ : ℝ} (hab : a < b) [Fact (a < b)] [Fact (b - a ≤ 1)]
  (hFiniteLength :
    CategoryTheory.Triangulated.ThinFiniteLengthInInterval C σ a b)
  (hε₀ : 0 < ε₀) (hε₀2 : ε₀ < 1 / 4) (hε₀8 : ε₀ < 1 / 8)
  (hthin : b - a + 2 * ε₀ < 1)
  (hsin :
    CategoryTheory.Triangulated.stabSeminorm C σ (W - σ.Z) <
      ENNReal.ofReal (Real.sin (Real.pi * ε₀)))
  (hW_interval :
    ∀ {F : C},
      CategoryTheory.Triangulated.Slicing.intervalProp C σ.slicing a b
          F →
        ¬CategoryTheory.Limits.IsZero F →
          W (CategoryTheory.Triangulated.cl C v F) ≠ 0)
  (hWindow :
    ∀ {F : C},
      CategoryTheory.Triangulated.Slicing.intervalProp C σ.slicing a b
          F →
        ¬CategoryTheory.Limits.IsZero F →
          a + ε₀ <
              CategoryTheory.Triangulated.wPhaseOf
                (W (CategoryTheory.Triangulated.cl C v F))
                ((a + b) / 2) ∧
            CategoryTheory.Triangulated.wPhaseOf
                (W (CategoryTheory.Triangulated.cl C v F))
                ((a + b) / 2) <
              b - ε₀)
  {E : C}
  (hE :
    CategoryTheory.Triangulated.Slicing.intervalProp C σ.slicing a b E)
  (hEne : ¬CategoryTheory.Limits.IsZero E) (t : ℝ) :
  ∃ X Y f g h,
    CategoryTheory.Pretriangulated.Triangle.mk f g h ∈
        CategoryTheory.Pretriangulated.distinguishedTriangles ∧
      CategoryTheory.Triangulated.StabilityCondition.WithClassMap.deformedGtPred
          C σ W hW ε₀ t X ∧
        CategoryTheory.Triangulated.StabilityCondition.WithClassMap.deformedLePred
          C σ W hW ε₀ t Y
CategoryTheory.Triangulated.exists_deformedGt_deformedLe_triangle_of_enveloped_interval.{v,
    u, 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]
  {Λ : Type u'} [AddCommGroup Λ]
  {v :
    CategoryTheory.Triangulated.K₀ C →+ Λ}
  (σ :
    CategoryTheory.Triangulated.StabilityCondition.WithClassMap
      C v)
  (W : Λ →+ ℂ)
  (hW :
    CategoryTheory.Triangulated.stabSeminorm
        C σ (W - σ.Z) <
      ENNReal.ofReal 1)
  {a b ε₀ : ℝ} (hab : a < b)
  [Fact (a < b)] [Fact (b - a ≤ 1)]
  (hFiniteLength :
    CategoryTheory.Triangulated.ThinFiniteLengthInInterval
      C σ a b)
  (hε₀ : 0 < ε₀) (hε₀2 : ε₀ < 1 / 4)
  (hε₀8 : ε₀ < 1 / 8)
  (hthin : b - a + 2 * ε₀ < 1)
  (hsin :
    CategoryTheory.Triangulated.stabSeminorm
        C σ (W - σ.Z) <
      ENNReal.ofReal
        (Real.sin (Real.pi * ε₀)))
  (hW_interval :
    ∀ {F : C},
      CategoryTheory.Triangulated.Slicing.intervalProp
          C σ.slicing a b F →
        ¬CategoryTheory.Limits.IsZero F →
          W
              (CategoryTheory.Triangulated.cl
                C v F) ≠
            0)
  (hWindow :
    ∀ {F : C},
      CategoryTheory.Triangulated.Slicing.intervalProp
          C σ.slicing a b F →
        ¬CategoryTheory.Limits.IsZero F →
          a + ε₀ <
              CategoryTheory.Triangulated.wPhaseOf
                (W
                  (CategoryTheory.Triangulated.cl
                    C v F))
                ((a + b) / 2) ∧
            CategoryTheory.Triangulated.wPhaseOf
                (W
                  (CategoryTheory.Triangulated.cl
                    C v F))
                ((a + b) / 2) <
              b - ε₀)
  {E : C}
  (hE :
    CategoryTheory.Triangulated.Slicing.intervalProp
      C σ.slicing a b E)
  (hEne : ¬CategoryTheory.Limits.IsZero E)
  (t : ℝ) :
  ∃ X Y f g h,
    CategoryTheory.Pretriangulated.Triangle.mk
          f g h ∈
        CategoryTheory.Pretriangulated.distinguishedTriangles ∧
      CategoryTheory.Triangulated.StabilityCondition.WithClassMap.deformedGtPred
          C σ W hW ε₀ t X ∧
        CategoryTheory.Triangulated.StabilityCondition.WithClassMap.deformedLePred
          C σ W hW ε₀ t Y

Something wrong, better idea? Suggest a change