14.2. Deformation: DeformedGtLe
14.2.1. P_in_deformedGtPred
\mathcal{P}(s) \subset Q(>t) for s \ge t + \varepsilon (Bridgeland p.24). A \sigma-semistable object of phase s \ge t + \varepsilon lies in Q(>t): obtain a Q-HN filtration via sigmaSemistable_hasDeformedHN, split at t, then show the Q(\le t) part vanishes.
Proof: Get the Q-HN filtration with phases in (s - 2\varepsilon, s + 4\varepsilon). For the last nonzero factor j_0, phase confinement gives s - \varepsilon < Q\text{-phase}(j_0). Since s \ge t + \varepsilon, all Q-phases exceed t. Build the extension closure witness from the Postnikov tower.
theorem
CategoryTheory.Triangulated.P_in_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) {ε₀ : ℝ} (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 * ε))) {s t : ℝ} (hst : s ≥ t + ε) {E : C} (hP : σ.slicing.P s E) (hE : ¬CategoryTheory.Limits.IsZero E) : CategoryTheory.Triangulated.StabilityCondition.WithClassMap.deformedGtPred C σ W hW ε t ECategoryTheory.Triangulated.P_in_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) {ε₀ : ℝ} (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 * ε))) {s t : ℝ} (hst : s ≥ t + ε) {E : C} (hP : σ.slicing.P s E) (hE : ¬CategoryTheory.Limits.IsZero E) : CategoryTheory.Triangulated.StabilityCondition.WithClassMap.deformedGtPred C σ W hW ε t E
Something wrong, better idea? Suggest a change
14.2.2. P_in_deformedLtPred
\mathcal{P}(s) \subset Q(<t) for s \le t - \varepsilon (dual). A \sigma-semistable object of phase s \le t - \varepsilon lies in Q(<t).
Proof: Dual of P_in_deformedGtPred: get Q-HN, find the first nonzero factor, use \phi^+(\text{factor}) \le s and phase confinement to show all Q-phases are < t.
theorem
CategoryTheory.Triangulated.P_in_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) {ε₀ : ℝ} (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 * ε))) {s t : ℝ} (hst : s ≤ t - ε) {E : C} (hP : σ.slicing.P s E) (hE : ¬CategoryTheory.Limits.IsZero E) : CategoryTheory.Triangulated.StabilityCondition.WithClassMap.deformedLtPred C σ W hW ε t ECategoryTheory.Triangulated.P_in_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) {ε₀ : ℝ} (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 * ε))) {s t : ℝ} (hst : s ≤ t - ε) {E : C} (hP : σ.slicing.P s E) (hE : ¬CategoryTheory.Limits.IsZero E) : CategoryTheory.Triangulated.StabilityCondition.WithClassMap.deformedLtPred C σ W hW ε t E
Something wrong, better idea? Suggest a change
14.2.3. sigmaSemistable_deformedGtLe_triangle
For a \sigma-semistable object E of phase s and cutoff t with s - \varepsilon < t < s + \varepsilon, there exists a distinguished triangle X \to E \to Y with X \in Q(>t) and Y \in Q(\le t).
Proof: Get the Q-HN filtration. Split the Postnikov tower at the cutoff t: factors with Q-phase > t give X \in Q(>t) and the rest give Y \in Q(\le t).
theorem
CategoryTheory.Triangulated.sigmaSemistable_deformedGtLe_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ε₀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} {φ : ℝ} (hP : σ.slicing.P φ E) (hE : ¬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 YCategoryTheory.Triangulated.sigmaSemistable_deformedGtLe_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ε₀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} {φ : ℝ} (hP : σ.slicing.P φ E) (hE : ¬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
14.2.4. deformedGtLe_triangle
Q(>t)/Q(\le t) truncation triangle (Bridgeland Step 2). For any object E, there exists a distinguished triangle X \to E \to Y with X \in Q(>t) and Y \in Q(\le t).
Proof: Decompose E via its \sigma-HN filtration. Each \sigma-semistable factor has a Q(>t)/Q(\le t) truncation by sigmaSemistable_deformedGtLe_triangle. Assemble these via iterated octahedral axiom applications along the Postnikov tower.
theorem
CategoryTheory.Triangulated.deformedGtLe_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ε₀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) (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 YCategoryTheory.Triangulated.deformedGtLe_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ε₀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) (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