14.4. Deformation: DeformedSlicingHN🔗

14.4.1. deformedPred_shift_one🔗

Forward shift for Q. If E is Q-semistable of phase \phi, then E[1] is Q-semistable of phase \phi + 1.

Proof: Transport the deformed predicate through the shift: the interval shifts by +1, the W-phase shifts by +1 (via wPhaseOf_neg and negation W(E[1]) = -W(E)), and semistability transfers by shifting all triangles.

theorem

CategoryTheory.Triangulated.deformedPred_shift_one.{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 < ε) {φ : ℝ} {X : C}
  (h :
    CategoryTheory.Triangulated.StabilityCondition.WithClassMap.deformedPred
      C σ W hW ε φ X) :
  CategoryTheory.Triangulated.StabilityCondition.WithClassMap.deformedPred
    C σ W hW ε (φ + 1) ((CategoryTheory.shiftFunctor C 1).obj X)
CategoryTheory.Triangulated.deformedPred_shift_one.{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 < ε) {φ : ℝ} {X : C}
  (h :
    CategoryTheory.Triangulated.StabilityCondition.WithClassMap.deformedPred
      C σ W hW ε φ X) :
  CategoryTheory.Triangulated.StabilityCondition.WithClassMap.deformedPred
    C σ W hW ε (φ + 1)
    ((CategoryTheory.shiftFunctor C 1).obj
      X)

Something wrong, better idea? Suggest a change

14.4.2. deformedPred_of_shift_one🔗

Backward shift for Q. If E[1] is Q-semistable of phase \phi + 1, then E is Q-semistable of phase \phi.

Proof: Reverse the shift transport: shift the interval by -1, invert the W-phase shift, and transfer semistability by shifting triangles by -1.

theorem

CategoryTheory.Triangulated.deformedPred_of_shift_one.{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 < ε) {φ : ℝ} {X : C}
  (h :
    CategoryTheory.Triangulated.StabilityCondition.WithClassMap.deformedPred
      C σ W hW ε (φ + 1) ((CategoryTheory.shiftFunctor C 1).obj X)) :
  CategoryTheory.Triangulated.StabilityCondition.WithClassMap.deformedPred
    C σ W hW ε φ X
CategoryTheory.Triangulated.deformedPred_of_shift_one.{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 < ε) {φ : ℝ} {X : C}
  (h :
    CategoryTheory.Triangulated.StabilityCondition.WithClassMap.deformedPred
      C σ W hW ε (φ + 1)
      ((CategoryTheory.shiftFunctor C
            1).obj
        X)) :
  CategoryTheory.Triangulated.StabilityCondition.WithClassMap.deformedPred
    C σ W hW ε φ X

Something wrong, better idea? Suggest a change

14.4.3. deformedGtPred_shift_one🔗

Q(>t)[1] \subseteq Q(>t+1): the forward shift sends Q(>t)-objects to Q(>t+1).

Proof: Induction on the extension closure defining Q(>t): zero objects shift to zero, semistable objects shift by deformedPred_shift_one, and extensions shift by shifting the distinguished triangle.

theorem

CategoryTheory.Triangulated.StabilityCondition.WithClassMap.deformedGtPred_shift_one.{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 < ε) {t : ℝ} {X : C}
  (hX :
    CategoryTheory.Triangulated.StabilityCondition.WithClassMap.deformedGtPred
      C σ W hW ε t X) :
  CategoryTheory.Triangulated.StabilityCondition.WithClassMap.deformedGtPred
    C σ W hW ε (t + 1) ((CategoryTheory.shiftFunctor C 1).obj X)
CategoryTheory.Triangulated.StabilityCondition.WithClassMap.deformedGtPred_shift_one.{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 < ε) {t : ℝ} {X : C}
  (hX :
    CategoryTheory.Triangulated.StabilityCondition.WithClassMap.deformedGtPred
      C σ W hW ε t X) :
  CategoryTheory.Triangulated.StabilityCondition.WithClassMap.deformedGtPred
    C σ W hW ε (t + 1)
    ((CategoryTheory.shiftFunctor C 1).obj
      X)

Something wrong, better idea? Suggest a change

14.4.4. deformedLePred_shift_one🔗

Q(\le t)[1] \subseteq Q(\le t+1): the forward shift sends Q(\le t)-objects to Q(\le t+1).

Proof: Same induction as deformedGtPred_shift_one.

theorem

CategoryTheory.Triangulated.StabilityCondition.WithClassMap.deformedLePred_shift_one.{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 < ε) {t : ℝ} {X : C}
  (hX :
    CategoryTheory.Triangulated.StabilityCondition.WithClassMap.deformedLePred
      C σ W hW ε t X) :
  CategoryTheory.Triangulated.StabilityCondition.WithClassMap.deformedLePred
    C σ W hW ε (t + 1) ((CategoryTheory.shiftFunctor C 1).obj X)
CategoryTheory.Triangulated.StabilityCondition.WithClassMap.deformedLePred_shift_one.{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 < ε) {t : ℝ} {X : C}
  (hX :
    CategoryTheory.Triangulated.StabilityCondition.WithClassMap.deformedLePred
      C σ W hW ε t X) :
  CategoryTheory.Triangulated.StabilityCondition.WithClassMap.deformedLePred
    C σ W hW ε (t + 1)
    ((CategoryTheory.shiftFunctor C 1).obj
      X)

Something wrong, better idea? Suggest a change

14.4.5. deformedLePred_shift_neg_one🔗

Q(\le t)[-1] \subseteq Q(\le t-1): the backward shift sends Q(\le t)-objects to Q(\le t-1).

Proof: For semistable objects, use deformedPred_of_shift_one applied to Y = E[-1] with Y[1] \cong E. For extensions, shift the triangle by -1.

theorem

CategoryTheory.Triangulated.StabilityCondition.WithClassMap.deformedLePred_shift_neg_one.{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 < ε) {t : ℝ} {X : C}
  (hX :
    CategoryTheory.Triangulated.StabilityCondition.WithClassMap.deformedLePred
      C σ W hW ε t X) :
  CategoryTheory.Triangulated.StabilityCondition.WithClassMap.deformedLePred
    C σ W hW ε (t - 1) ((CategoryTheory.shiftFunctor C (-1)).obj X)
CategoryTheory.Triangulated.StabilityCondition.WithClassMap.deformedLePred_shift_neg_one.{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 < ε) {t : ℝ} {X : C}
  (hX :
    CategoryTheory.Triangulated.StabilityCondition.WithClassMap.deformedLePred
      C σ W hW ε t X) :
  CategoryTheory.Triangulated.StabilityCondition.WithClassMap.deformedLePred
    C σ W hW ε (t - 1)
    ((CategoryTheory.shiftFunctor C
          (-1)).obj
      X)

Something wrong, better idea? Suggest a change

14.4.6. isZero_of_deformedGtPred_deformedLePred🔗

If X \in Q(>t) \cap Q(\le t), then X = 0.

Proof: The identity \operatorname{id}_X : X \to X is a morphism from a Q(>t)-object to a Q(\le t)-object, which is zero by hom-vanishing.

theorem

CategoryTheory.Triangulated.isZero_of_deformedGtPred_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)
  {ε : ℝ} (hε : 0 < ε) (hε2 : ε < 1 / 4) (hε8 : ε < 1 / 8)
  (hsin :
    CategoryTheory.Triangulated.stabSeminorm C σ (W - σ.Z) <
      ENNReal.ofReal (Real.sin (Real.pi * ε)))
  {t : ℝ} {X : C}
  (hGt :
    CategoryTheory.Triangulated.StabilityCondition.WithClassMap.deformedGtPred
      C σ W hW ε t X)
  (hLe :
    CategoryTheory.Triangulated.StabilityCondition.WithClassMap.deformedLePred
      C σ W hW ε t X) :
  CategoryTheory.Limits.IsZero X
CategoryTheory.Triangulated.isZero_of_deformedGtPred_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)
  {ε : ℝ} (hε : 0 < ε) (hε2 : ε < 1 / 4)
  (hε8 : ε < 1 / 8)
  (hsin :
    CategoryTheory.Triangulated.stabSeminorm
        C σ (W - σ.Z) <
      ENNReal.ofReal
        (Real.sin (Real.pi * ε)))
  {t : ℝ} {X : C}
  (hGt :
    CategoryTheory.Triangulated.StabilityCondition.WithClassMap.deformedGtPred
      C σ W hW ε t X)
  (hLe :
    CategoryTheory.Triangulated.StabilityCondition.WithClassMap.deformedLePred
      C σ W hW ε t X) :
  CategoryTheory.Limits.IsZero X

Something wrong, better idea? Suggest a change

14.4.7. deformedGtPred_of_triangle_obj₃🔗

Third-vertex closure for Q(>t): if X \to S \to Y is distinguished with X, S \in Q(>t), then Y \in Q(>t).

Proof: Rotate the triangle: S \to Y \to X[1] is distinguished. Since X[1] \in Q(>t+1) \subseteq Q(>t), the extension closure gives Y \in Q(>t).

theorem

CategoryTheory.Triangulated.deformedGtPred_of_triangle_obj₃.{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 < ε) {t : ℝ} {X S Y : C} {f : X ⟶ S} {g : S ⟶ Y}
  {h : Y ⟶ (CategoryTheory.shiftFunctor C 1).obj X}
  (hT :
    CategoryTheory.Pretriangulated.Triangle.mk f g h ∈
      CategoryTheory.Pretriangulated.distinguishedTriangles)
  (hX :
    CategoryTheory.Triangulated.StabilityCondition.WithClassMap.deformedGtPred
      C σ W hW ε t X)
  (hS :
    CategoryTheory.Triangulated.StabilityCondition.WithClassMap.deformedGtPred
      C σ W hW ε t S) :
  CategoryTheory.Triangulated.StabilityCondition.WithClassMap.deformedGtPred
    C σ W hW ε t Y
CategoryTheory.Triangulated.deformedGtPred_of_triangle_obj₃.{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 < ε) {t : ℝ} {X S Y : C}
  {f : X ⟶ S} {g : S ⟶ Y}
  {h :
    Y ⟶
      (CategoryTheory.shiftFunctor C
            1).obj
        X}
  (hT :
    CategoryTheory.Pretriangulated.Triangle.mk
        f g h ∈
      CategoryTheory.Pretriangulated.distinguishedTriangles)
  (hX :
    CategoryTheory.Triangulated.StabilityCondition.WithClassMap.deformedGtPred
      C σ W hW ε t X)
  (hS :
    CategoryTheory.Triangulated.StabilityCondition.WithClassMap.deformedGtPred
      C σ W hW ε t S) :
  CategoryTheory.Triangulated.StabilityCondition.WithClassMap.deformedGtPred
    C σ W hW ε t Y

Something wrong, better idea? Suggest a change

14.4.8. deformedLePred_of_triangle_obj₁🔗

First-vertex closure for Q(\le t): if X \to R_0 \to R_1 is distinguished with R_0, R_1 \in Q(\le t), then X \in Q(\le t).

Proof: Inverse-rotate: R_1[-1] \to X \to R_0 is distinguished. Since R_1[-1] \in Q(\le t-1) \subseteq Q(\le t), extension closure gives X \in Q(\le t).

theorem

CategoryTheory.Triangulated.deformedLePred_of_triangle_obj₁.{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 < ε) {t : ℝ} {X R₀ R₁ : C} {f : X ⟶ R₀} {g : R₀ ⟶ R₁}
  {h : R₁ ⟶ (CategoryTheory.shiftFunctor C 1).obj X}
  (hT :
    CategoryTheory.Pretriangulated.Triangle.mk f g h ∈
      CategoryTheory.Pretriangulated.distinguishedTriangles)
  (hR₀ :
    CategoryTheory.Triangulated.StabilityCondition.WithClassMap.deformedLePred
      C σ W hW ε t R₀)
  (hR₁ :
    CategoryTheory.Triangulated.StabilityCondition.WithClassMap.deformedLePred
      C σ W hW ε t R₁) :
  CategoryTheory.Triangulated.StabilityCondition.WithClassMap.deformedLePred
    C σ W hW ε t X
CategoryTheory.Triangulated.deformedLePred_of_triangle_obj₁.{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 < ε) {t : ℝ}
  {X R₀ R₁ : C} {f : X ⟶ R₀} {g : R₀ ⟶ R₁}
  {h :
    R₁ ⟶
      (CategoryTheory.shiftFunctor C
            1).obj
        X}
  (hT :
    CategoryTheory.Pretriangulated.Triangle.mk
        f g h ∈
      CategoryTheory.Pretriangulated.distinguishedTriangles)
  (hR₀ :
    CategoryTheory.Triangulated.StabilityCondition.WithClassMap.deformedLePred
      C σ W hW ε t R₀)
  (hR₁ :
    CategoryTheory.Triangulated.StabilityCondition.WithClassMap.deformedLePred
      C σ W hW ε t R₁) :
  CategoryTheory.Triangulated.StabilityCondition.WithClassMap.deformedLePred
    C σ W hW ε t X

Something wrong, better idea? Suggest a change

14.4.9. isZero_deformedLe_of_deformedGt_triangle🔗

If S \in Q(>t) and distinguished triangle X \to S \to Y with X \in Q(>t) and Y \in Q(\le t), then Y = 0.

Proof: Third-vertex closure gives Y \in Q(>t). Combined with Y \in Q(\le t), apply isZero_of_deformedGtPred_deformedLePred.

theorem

CategoryTheory.Triangulated.isZero_deformedLe_of_deformedGt_triangle.{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 * ε)))
  {t : ℝ} {X S Y : C} {f : X ⟶ S} {g : S ⟶ Y}
  {h : Y ⟶ (CategoryTheory.shiftFunctor C 1).obj X}
  (hT :
    CategoryTheory.Pretriangulated.Triangle.mk f g h ∈
      CategoryTheory.Pretriangulated.distinguishedTriangles)
  (hX :
    CategoryTheory.Triangulated.StabilityCondition.WithClassMap.deformedGtPred
      C σ W hW ε t X)
  (hS :
    CategoryTheory.Triangulated.StabilityCondition.WithClassMap.deformedGtPred
      C σ W hW ε t S)
  (hY :
    CategoryTheory.Triangulated.StabilityCondition.WithClassMap.deformedLePred
      C σ W hW ε t Y) :
  CategoryTheory.Limits.IsZero Y
CategoryTheory.Triangulated.isZero_deformedLe_of_deformedGt_triangle.{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 * ε)))
  {t : ℝ} {X S Y : C} {f : X ⟶ S}
  {g : S ⟶ Y}
  {h :
    Y ⟶
      (CategoryTheory.shiftFunctor C
            1).obj
        X}
  (hT :
    CategoryTheory.Pretriangulated.Triangle.mk
        f g h ∈
      CategoryTheory.Pretriangulated.distinguishedTriangles)
  (hX :
    CategoryTheory.Triangulated.StabilityCondition.WithClassMap.deformedGtPred
      C σ W hW ε t X)
  (hS :
    CategoryTheory.Triangulated.StabilityCondition.WithClassMap.deformedGtPred
      C σ W hW ε t S)
  (hY :
    CategoryTheory.Triangulated.StabilityCondition.WithClassMap.deformedLePred
      C σ W hW ε t Y) :
  CategoryTheory.Limits.IsZero Y

Something wrong, better idea? Suggest a change

14.4.10. isZero_deformedGt_of_deformedLe_triangle🔗

Dual: if S \in Q(\le t) and distinguished triangle X \to S \to Y with X \in Q(>t) and Y \in Q(\le t), then X = 0.

Proof: First-vertex closure gives X \in Q(\le t). Combined with X \in Q(>t), apply isZero_of_deformedGtPred_deformedLePred.

theorem

CategoryTheory.Triangulated.isZero_deformedGt_of_deformedLe_triangle.{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 * ε)))
  {t : ℝ} {X S Y : C} {f : X ⟶ S} {g : S ⟶ Y}
  {h : Y ⟶ (CategoryTheory.shiftFunctor C 1).obj X}
  (hT :
    CategoryTheory.Pretriangulated.Triangle.mk f g h ∈
      CategoryTheory.Pretriangulated.distinguishedTriangles)
  (hX :
    CategoryTheory.Triangulated.StabilityCondition.WithClassMap.deformedGtPred
      C σ W hW ε t X)
  (hS :
    CategoryTheory.Triangulated.StabilityCondition.WithClassMap.deformedLePred
      C σ W hW ε t S)
  (hY :
    CategoryTheory.Triangulated.StabilityCondition.WithClassMap.deformedLePred
      C σ W hW ε t Y) :
  CategoryTheory.Limits.IsZero X
CategoryTheory.Triangulated.isZero_deformedGt_of_deformedLe_triangle.{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 * ε)))
  {t : ℝ} {X S Y : C} {f : X ⟶ S}
  {g : S ⟶ Y}
  {h :
    Y ⟶
      (CategoryTheory.shiftFunctor C
            1).obj
        X}
  (hT :
    CategoryTheory.Pretriangulated.Triangle.mk
        f g h ∈
      CategoryTheory.Pretriangulated.distinguishedTriangles)
  (hX :
    CategoryTheory.Triangulated.StabilityCondition.WithClassMap.deformedGtPred
      C σ W hW ε t X)
  (hS :
    CategoryTheory.Triangulated.StabilityCondition.WithClassMap.deformedLePred
      C σ W hW ε t S)
  (hY :
    CategoryTheory.Triangulated.StabilityCondition.WithClassMap.deformedLePred
      C σ W hW ε t Y) :
  CategoryTheory.Limits.IsZero X

Something wrong, better idea? Suggest a change

14.4.11. deformedSlicing_hn_exists🔗

Q-HN existence (Bridgeland p.24, Steps 1+2). Every object admits a Q-HN filtration.

Proof: For zero objects, use the trivial filtration. For nonzero E, decompose via the \sigma-HN filtration. Each \sigma-factor admits a Q-HN via sigmaSemistable_hasDeformedHN. Combine deformedGtLe_triangle (Step 2: Q(>t)/Q(\le t) truncation) with exists_hn_of_deformedGt_deformedLe_triangle (Step 1: recursive refinement of truncation triangles into a full HN filtration).

theorem

CategoryTheory.Triangulated.deformedSlicing_hn_exists.{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ε₀10 : ε₀ < 1 / 10)
  (hWide :
    CategoryTheory.Triangulated.WideSectorFiniteLength C σ ε₀ hε₀ ⋯)
  {ε : ℝ} (hε : 0 < ε) (hεε₀ : ε < ε₀)
  (hsin :
    CategoryTheory.Triangulated.stabSeminorm C σ (W - σ.Z) <
      ENNReal.ofReal (Real.sin (Real.pi * ε)))
  (E : C) :
  Nonempty
    (CategoryTheory.Triangulated.HNFiltration C
      (CategoryTheory.Triangulated.StabilityCondition.WithClassMap.deformedPred
        C σ W hW ε)
      E)
CategoryTheory.Triangulated.deformedSlicing_hn_exists.{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ε₀10 : ε₀ < 1 / 10)
  (hWide :
    CategoryTheory.Triangulated.WideSectorFiniteLength
      C σ ε₀ hε₀ ⋯)
  {ε : ℝ} (hε : 0 < ε) (hεε₀ : ε < ε₀)
  (hsin :
    CategoryTheory.Triangulated.stabSeminorm
        C σ (W - σ.Z) <
      ENNReal.ofReal
        (Real.sin (Real.pi * ε)))
  (E : C) :
  Nonempty
    (CategoryTheory.Triangulated.HNFiltration
      C
      (CategoryTheory.Triangulated.StabilityCondition.WithClassMap.deformedPred
        C σ W hW ε)
      E)

Something wrong, better idea? Suggest a change