14.9. Deformation: HomVanishing🔗

14.9.1. deformedPred🔗

Deformed slicing predicate (Node 7.Q). Given a stability condition \sigma, a perturbation W with \|W - Z\|_\sigma < 1, the deformed slicing Q(\psi) consists of zero objects and objects that are W-semistable of W-phase \psi in some thin interval \mathcal{P}((a, b)) with b - a + 2\varepsilon_0 < 1 and the enveloping condition a + \varepsilon_0 \le \psi \le b - \varepsilon_0.

Construction: Defined as a disjunction: either E is zero, or there exist a < b with the thinness and enveloping constraints such that E is W-semistable of phase \psi in \mathcal{P}((a, b)).

def

CategoryTheory.Triangulated.StabilityCondition.WithClassMap.deformedPred.{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)
  (ε₀ ψ : ℝ) : CategoryTheory.ObjectProperty C
CategoryTheory.Triangulated.StabilityCondition.WithClassMap.deformedPred.{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)
  (ε₀ ψ : ℝ) :
  CategoryTheory.ObjectProperty C

Something wrong, better idea? Suggest a change

14.9.2. deformedPred_zero🔗

Zero objects lie in every Q(\psi).

Proof: Immediate from the left disjunct of the deformed predicate.

theorem

CategoryTheory.Triangulated.StabilityCondition.WithClassMap.deformedPred_zero.{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} (hE : CategoryTheory.Limits.IsZero E) :
  CategoryTheory.Triangulated.StabilityCondition.WithClassMap.deformedPred
    C σ W hW ε₀ ψ E
CategoryTheory.Triangulated.StabilityCondition.WithClassMap.deformedPred_zero.{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}
  (hE : CategoryTheory.Limits.IsZero E) :
  CategoryTheory.Triangulated.StabilityCondition.WithClassMap.deformedPred
    C σ W hW ε₀ ψ E

Something wrong, better idea? Suggest a change

14.9.3. deformedPred_closedUnderIso🔗

The deformed predicate Q(\psi) is closed under isomorphisms.

Proof: Transport the interval membership, W-nonvanishing, phase equality, and semistability condition across the isomorphism using K_0 invariance and HN filtration transport.

theorem

CategoryTheory.Triangulated.StabilityCondition.WithClassMap.deformedPred_closedUnderIso.{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)
  (ε₀ ψ : ℝ) :
  (CategoryTheory.Triangulated.StabilityCondition.WithClassMap.deformedPred
      C σ W hW ε₀ ψ).IsClosedUnderIsomorphisms
CategoryTheory.Triangulated.StabilityCondition.WithClassMap.deformedPred_closedUnderIso.{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)
  (ε₀ ψ : ℝ) :
  (CategoryTheory.Triangulated.StabilityCondition.WithClassMap.deformedPred
      C σ W hW ε₀
      ψ).IsClosedUnderIsomorphisms

Something wrong, better idea? Suggest a change

14.9.4. mem_phaseShiftHeart_of_phaseBounds_smallGap🔗

An object E with \phi^-(E) > t and \phi^+(E) \le t + 1 lies in the heart of the t-structure \mathcal{P}((t, t+1]).

Proof: The bounds place E in both the \le 0 and \ge 0 parts of the shifted slicing, hence in the heart.

theorem

CategoryTheory.Triangulated.mem_phaseShiftHeart_of_phaseBounds_smallGap.{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}
  (hE : ¬CategoryTheory.Limits.IsZero E) {t : ℝ}
  (hgt : t < CategoryTheory.Triangulated.Slicing.phiMinus C s E hE)
  (hle : CategoryTheory.Triangulated.Slicing.phiPlus C s E hE ≤ t + 1) :
  (CategoryTheory.Triangulated.Slicing.toTStructure C
        (CategoryTheory.Triangulated.Slicing.phaseShift C s t)).heart
    E
CategoryTheory.Triangulated.mem_phaseShiftHeart_of_phaseBounds_smallGap.{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}
  (hE : ¬CategoryTheory.Limits.IsZero E)
  {t : ℝ}
  (hgt :
    t <
      CategoryTheory.Triangulated.Slicing.phiMinus
        C s E hE)
  (hle :
    CategoryTheory.Triangulated.Slicing.phiPlus
        C s E hE ≤
      t + 1) :
  (CategoryTheory.Triangulated.Slicing.toTStructure
        C
        (CategoryTheory.Triangulated.Slicing.phaseShift
          C s t)).heart
    E

Something wrong, better idea? Suggest a change

14.9.5. gtProp_leProp_of_phaseShiftHeart🔗

If E is a nonzero object in the heart of the phase-shifted t-structure \mathcal{P}((a-1,a]) and \phi^+(E) \leq u, then E \in \mathcal{P}(>a) and E \in \mathcal{P}(\leq u).

Proof: Heart membership directly gives E \in \mathcal{P}(>a) via the shifted slicing, and the upper bound \phi^+(E) \leq u gives E \in \mathcal{P}(\leq u) by monotonicity.

theorem

CategoryTheory.Triangulated.gtProp_leProp_of_phaseShiftHeart.{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} {a u : ℝ}
  (hHeart :
    (CategoryTheory.Triangulated.Slicing.toTStructure C
          (CategoryTheory.Triangulated.Slicing.phaseShift C s a)).heart
      E)
  (hE : ¬CategoryTheory.Limits.IsZero E)
  (hu : CategoryTheory.Triangulated.Slicing.phiPlus C s E hE ≤ u) :
  CategoryTheory.Triangulated.Slicing.gtProp C s a E ∧
    CategoryTheory.Triangulated.Slicing.leProp C s u E
CategoryTheory.Triangulated.gtProp_leProp_of_phaseShiftHeart.{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} {a u : ℝ}
  (hHeart :
    (CategoryTheory.Triangulated.Slicing.toTStructure
          C
          (CategoryTheory.Triangulated.Slicing.phaseShift
            C s a)).heart
      E)
  (hE : ¬CategoryTheory.Limits.IsZero E)
  (hu :
    CategoryTheory.Triangulated.Slicing.phiPlus
        C s E hE ≤
      u) :
  CategoryTheory.Triangulated.Slicing.gtProp
      C s a E ∧
    CategoryTheory.Triangulated.Slicing.leProp
      C s u E

Something wrong, better idea? Suggest a change

14.9.6. geProp_leProp_of_phaseShiftHeart🔗

If E is a nonzero object in the heart of the phase-shifted t-structure \mathcal{P}((a-1,a]) and \ell \leq \phi^-(E), then E \in \mathcal{P}(\geq \ell) and E \in \mathcal{P}(\leq a+1).

Proof: Membership in the heart gives \phi^-(E) > a (from the \mathcal{P}(>a) part) and \phi^+(E) \leq a+1 (from the \mathcal{P}(\leq a+1) part); the lower bound \ell \leq \phi^-(E) then implies E \in \mathcal{P}(\geq \ell).

theorem

CategoryTheory.Triangulated.geProp_leProp_of_phaseShiftHeart.{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} {a l : ℝ}
  (hHeart :
    (CategoryTheory.Triangulated.Slicing.toTStructure C
          (CategoryTheory.Triangulated.Slicing.phaseShift C s a)).heart
      E)
  (hE : ¬CategoryTheory.Limits.IsZero E)
  (hl : l ≤ CategoryTheory.Triangulated.Slicing.phiMinus C s E hE) :
  CategoryTheory.Triangulated.Slicing.geProp C s l E ∧
    CategoryTheory.Triangulated.Slicing.leProp C s (a + 1) E
CategoryTheory.Triangulated.geProp_leProp_of_phaseShiftHeart.{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} {a l : ℝ}
  (hHeart :
    (CategoryTheory.Triangulated.Slicing.toTStructure
          C
          (CategoryTheory.Triangulated.Slicing.phaseShift
            C s a)).heart
      E)
  (hE : ¬CategoryTheory.Limits.IsZero E)
  (hl :
    l ≤
      CategoryTheory.Triangulated.Slicing.phiMinus
        C s E hE) :
  CategoryTheory.Triangulated.Slicing.geProp
      C s l E ∧
    CategoryTheory.Triangulated.Slicing.leProp
      C s (a + 1) E

Something wrong, better idea? Suggest a change

14.9.7. midpoint_left_target_thin🔗

If \psi_1 \leq \psi_2 + 2\varepsilon_0 and \varepsilon_0 < 1/8, then (\psi_1 + \varepsilon_0) - \bigl(\tfrac{\psi_1+\psi_2}{2} - \tfrac{1}{2}\bigr) + 2\varepsilon_0 < 1.

Proof: A direct linear arithmetic computation from the hypotheses.

theorem

CategoryTheory.Triangulated.midpoint_left_target_thin {ψ₁ ψ₂ ε₀ : ℝ}
  (hsmall : ψ₁ ≤ ψ₂ + 2 * ε₀) (hε₀8 : ε₀ < 1 / 8) :
  ψ₁ + ε₀ - ((ψ₁ + ψ₂) / 2 - 1 / 2) + 2 * ε₀ < 1
CategoryTheory.Triangulated.midpoint_left_target_thin
  {ψ₁ ψ₂ ε₀ : ℝ}
  (hsmall : ψ₁ ≤ ψ₂ + 2 * ε₀)
  (hε₀8 : ε₀ < 1 / 8) :
  ψ₁ + ε₀ - ((ψ₁ + ψ₂) / 2 - 1 / 2) +
      2 * ε₀ <
    1

Something wrong, better idea? Suggest a change

14.9.8. midpoint_right_target_thin🔗

If \psi_1 \leq \psi_2 + 2\varepsilon_0 and \varepsilon_0 < 1/8, then \bigl(\tfrac{\psi_1+\psi_2}{2} + \tfrac{1}{2}\bigr) - (\psi_2 - \varepsilon_0) + 2\varepsilon_0 < 1.

Proof: A direct linear arithmetic computation from the hypotheses.

theorem

CategoryTheory.Triangulated.midpoint_right_target_thin {ψ₁ ψ₂ ε₀ : ℝ}
  (hsmall : ψ₁ ≤ ψ₂ + 2 * ε₀) (hε₀8 : ε₀ < 1 / 8) :
  (ψ₁ + ψ₂) / 2 - 1 / 2 + 1 - (ψ₂ - ε₀) + 2 * ε₀ < 1
CategoryTheory.Triangulated.midpoint_right_target_thin
  {ψ₁ ψ₂ ε₀ : ℝ}
  (hsmall : ψ₁ ≤ ψ₂ + 2 * ε₀)
  (hε₀8 : ε₀ < 1 / 8) :
  (ψ₁ + ψ₂) / 2 - 1 / 2 + 1 - (ψ₂ - ε₀) +
      2 * ε₀ <
    1

Something wrong, better idea? Suggest a change

14.9.9. midpoint_image_window_thin🔗

If \psi_2 < \psi_1 \leq \psi_2 + 2\varepsilon_0 and \varepsilon_0 < 1/8, then the interval width (\psi_2 + \varepsilon_0) - (\psi_1 - \varepsilon_0) + 2\varepsilon_0 < 1.

Proof: A direct linear arithmetic computation from the hypotheses.

theorem

CategoryTheory.Triangulated.midpoint_image_window_thin {ψ₁ ψ₂ ε₀ : ℝ}
  (hgap : ψ₂ < ψ₁) (hsmall : ψ₁ ≤ ψ₂ + 2 * ε₀) (hε₀8 : ε₀ < 1 / 8) :
  ψ₂ + ε₀ - (ψ₁ - ε₀) + 2 * ε₀ < 1
CategoryTheory.Triangulated.midpoint_image_window_thin
  {ψ₁ ψ₂ ε₀ : ℝ} (hgap : ψ₂ < ψ₁)
  (hsmall : ψ₁ ≤ ψ₂ + 2 * ε₀)
  (hε₀8 : ε₀ < 1 / 8) :
  ψ₂ + ε₀ - (ψ₁ - ε₀) + 2 * ε₀ < 1

Something wrong, better idea? Suggest a change

14.9.10. mem_phaseShiftHeart_of_midpoint_left🔗

If E is nonzero with \psi_1 - \varepsilon_0 \leq \phi^-(E) and \phi^+(E) \leq \psi_1 + \varepsilon_0 (so E has phases near \psi_1), \psi_2 < \psi_1, \psi_1 \leq \psi_2 + 2\varepsilon_0, and \varepsilon_0 < 1/4, then E lies in the heart of the t-structure \mathcal{P}\bigl((\tfrac{\psi_1+\psi_2}{2}-\tfrac{3}{2},\, \tfrac{\psi_1+\psi_2}{2}-\tfrac{1}{2}]\bigr).

Proof: By mem_phaseShiftHeart_of_phaseBounds_smallGap, it suffices to show \tfrac{\psi_1+\psi_2}{2} - \tfrac{1}{2} < \phi^-(E) and \phi^+(E) \leq \tfrac{\psi_1+\psi_2}{2} + \tfrac{1}{2}; both follow from the hypotheses on \psi_1, \psi_2, \varepsilon_0 by linear arithmetic.

theorem

CategoryTheory.Triangulated.mem_phaseShiftHeart_of_midpoint_left.{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}
  (hE : ¬CategoryTheory.Limits.IsZero E) {ψ₁ ψ₂ ε₀ : ℝ}
  (hlo :
    ψ₁ - ε₀ ≤ CategoryTheory.Triangulated.Slicing.phiMinus C s E hE)
  (hhi : CategoryTheory.Triangulated.Slicing.phiPlus C s E hE ≤ ψ₁ + ε₀)
  (hgap : ψ₂ < ψ₁) (hsmall : ψ₁ ≤ ψ₂ + 2 * ε₀) (hε₀4 : ε₀ < 1 / 4) :
  (CategoryTheory.Triangulated.Slicing.toTStructure C
        (CategoryTheory.Triangulated.Slicing.phaseShift C s
          ((ψ₁ + ψ₂) / 2 - 1 / 2))).heart
    E
CategoryTheory.Triangulated.mem_phaseShiftHeart_of_midpoint_left.{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}
  (hE : ¬CategoryTheory.Limits.IsZero E)
  {ψ₁ ψ₂ ε₀ : ℝ}
  (hlo :
    ψ₁ - ε₀ ≤
      CategoryTheory.Triangulated.Slicing.phiMinus
        C s E hE)
  (hhi :
    CategoryTheory.Triangulated.Slicing.phiPlus
        C s E hE ≤
      ψ₁ + ε₀)
  (hgap : ψ₂ < ψ₁)
  (hsmall : ψ₁ ≤ ψ₂ + 2 * ε₀)
  (hε₀4 : ε₀ < 1 / 4) :
  (CategoryTheory.Triangulated.Slicing.toTStructure
        C
        (CategoryTheory.Triangulated.Slicing.phaseShift
          C s
          ((ψ₁ + ψ₂) / 2 - 1 / 2))).heart
    E

Something wrong, better idea? Suggest a change

14.9.11. mem_phaseShiftHeart_of_midpoint_right🔗

If E is nonzero with \psi_2 - \varepsilon_0 \leq \phi^-(E) and \phi^+(E) \leq \psi_2 + \varepsilon_0 (so E has phases near \psi_2), \psi_2 < \psi_1, \psi_1 \leq \psi_2 + 2\varepsilon_0, and \varepsilon_0 < 1/4, then E lies in the heart \mathcal{P}\bigl((\tfrac{\psi_1+\psi_2}{2}-\tfrac{3}{2},\, \tfrac{\psi_1+\psi_2}{2}-\tfrac{1}{2}]\bigr).

Proof: Analogous to mem_phaseShiftHeart_of_midpoint_left, by mem_phaseShiftHeart_of_phaseBounds_smallGap, using that the phases of E near \psi_2 together with \psi_2 < \psi_1 \leq \psi_2 + 2\varepsilon_0 and \varepsilon_0 < 1/4 place E in the required window.

theorem

CategoryTheory.Triangulated.mem_phaseShiftHeart_of_midpoint_right.{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}
  (hE : ¬CategoryTheory.Limits.IsZero E) {ψ₁ ψ₂ ε₀ : ℝ}
  (hlo :
    ψ₂ - ε₀ ≤ CategoryTheory.Triangulated.Slicing.phiMinus C s E hE)
  (hhi : CategoryTheory.Triangulated.Slicing.phiPlus C s E hE ≤ ψ₂ + ε₀)
  (hgap : ψ₂ < ψ₁) (hsmall : ψ₁ ≤ ψ₂ + 2 * ε₀) (hε₀4 : ε₀ < 1 / 4) :
  (CategoryTheory.Triangulated.Slicing.toTStructure C
        (CategoryTheory.Triangulated.Slicing.phaseShift C s
          ((ψ₁ + ψ₂) / 2 - 1 / 2))).heart
    E
CategoryTheory.Triangulated.mem_phaseShiftHeart_of_midpoint_right.{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}
  (hE : ¬CategoryTheory.Limits.IsZero E)
  {ψ₁ ψ₂ ε₀ : ℝ}
  (hlo :
    ψ₂ - ε₀ ≤
      CategoryTheory.Triangulated.Slicing.phiMinus
        C s E hE)
  (hhi :
    CategoryTheory.Triangulated.Slicing.phiPlus
        C s E hE ≤
      ψ₂ + ε₀)
  (hgap : ψ₂ < ψ₁)
  (hsmall : ψ₁ ≤ ψ₂ + 2 * ε₀)
  (hε₀4 : ε₀ < 1 / 4) :
  (CategoryTheory.Triangulated.Slicing.toTStructure
        C
        (CategoryTheory.Triangulated.Slicing.phaseShift
          C s
          ((ψ₁ + ψ₂) / 2 - 1 / 2))).heart
    E

Something wrong, better idea? Suggest a change

14.9.12. hom_eq_zero_of_deformedPred🔗

Sharp hom-vanishing for Q (Bridgeland's Lemma 7.6). If E \in Q(\psi_1) and F \in Q(\psi_2) with \psi_1 > \psi_2, then every morphism E \to F is zero.

Proof: Two cases. **Large gap** (\psi_1 > \psi_2 + 2\varepsilon_0): phase confinement puts E and F in disjoint \sigma-intervals, so interval hom-vanishing applies. **Small gap** (\psi_1 - \psi_2 \le 2\varepsilon_0): embed both in the abelian heart \mathcal{P}((c, c+1]) of a \sigma-t-structure. Factor f as E \twoheadrightarrow \operatorname{im}(f) \hookrightarrow F. The K_0 identity W(E) = W(\ker f) + W(\operatorname{im} f) with \operatorname{wPhaseOf}(W(\operatorname{im} f)) \le \psi_2 < \psi_1 forces \operatorname{wPhaseOf}(W(\ker f)) > \psi_1, contradicting E's W-semistability.

theorem

CategoryTheory.Triangulated.StabilityCondition.WithClassMap.hom_eq_zero_of_deformedPred.{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} {ψ₁ ψ₂ : ℝ}
  (hE :
    CategoryTheory.Triangulated.StabilityCondition.WithClassMap.deformedPred
      C σ W hW ε₀ ψ₁ E)
  (hF :
    CategoryTheory.Triangulated.StabilityCondition.WithClassMap.deformedPred
      C σ W hW ε₀ ψ₂ F)
  (hgap : ψ₁ > ψ₂) (f : E ⟶ F) : f = 0
CategoryTheory.Triangulated.StabilityCondition.WithClassMap.hom_eq_zero_of_deformedPred.{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} {ψ₁ ψ₂ : ℝ}
  (hE :
    CategoryTheory.Triangulated.StabilityCondition.WithClassMap.deformedPred
      C σ W hW ε₀ ψ₁ E)
  (hF :
    CategoryTheory.Triangulated.StabilityCondition.WithClassMap.deformedPred
      C σ W hW ε₀ ψ₂ F)
  (hgap : ψ₁ > ψ₂) (f : E ⟶ F) : f = 0

Large gap (ψ₁ > ψ₂ + 2ε₀): Phase confinement (phase_confinement_from_stabSeminorm) puts E and F in disjoint σ-intervals, so intervalHom_eq_zero applies (cf. hom_eq_zero_of_wSemistable_gap).
Small gap (ψ₁ - ψ₂ ≤ 2ε₀): Embed both E, F in the abelian heart P((c, c+1]) of a σ-t-structure. Factor f as E ↠ im(f) ↪ F. F's W-semistability (weakened to only require K ∈ P((a,b)), not Q) gives wPhaseOf(W(im(f))) ≤ ψ₂. The K₀ identity W(E) = W(ker(f)) + W(im(f)) with phase(W(E)) = ψ₁ > ψ₂ forces phase(W(ker(f))) > ψ₁, contradicting E's W-semistability.

Something wrong, better idea? Suggest a change