Truncation for owner deformed phase cuts #
This file turns owner deformed HN filtrations into cut triangles and proves the two old-to-deformed phase embeddings used in the global construction. The embeddings use a two-radius margin; this avoids any boundary-equality choice while retaining an open neighborhood of every central charge.
theorem
CategoryTheory.Triangulated.StabilityCondition.WithClassMap.exists_deformedCut_triangle_of_hn
(C : Type u)
[Category.{v, u} C]
[Limits.HasZeroObject C]
[HasShift C ℤ]
[Preadditive C]
[∀ (n : ℤ), (shiftFunctor C n).Additive]
[Pretriangulated C]
[IsTriangulated C]
{Λ : Type u'}
[AddCommGroup Λ]
{κ : K₀ C →+ Λ}
(σ : WithClassMap C κ)
(W : Λ →+ ℂ)
{r : ℝ}
(hr0 : 0 ≤ r)
(hr1 : r < 1)
(hW : WeakStabilityCondition.StabilityCondition.Deformation.stabilitySeminorm C σ (W - σ.Z) ≤ ENNReal.ofReal r)
{ε : ℝ}
{E : C}
(G : HNFiltration C (deformedPred C σ W hr0 hr1 hW ε) E)
(t : ℝ)
:
∃ (X : C) (Y : C) (f : X ⟶ E) (g : E ⟶ Y) (δ : Y ⟶ (shiftFunctor C 1).obj X),
Pretriangulated.Triangle.mk f g δ ∈ Pretriangulated.distinguishedTriangles ∧ deformedGtPred C σ W hr0 hr1 hW ε t X ∧ deformedLePred C σ W hr0 hr1 hW ε t Y
Splitting an owner deformed HN filtration at a real cutoff gives the
corresponding Q(>t)/Q(≤t) triangle.
theorem
CategoryTheory.Triangulated.StabilityCondition.WithClassMap.semistable_has_tight_deformedHN
(C : Type u)
[Category.{v, u} C]
[Limits.HasZeroObject C]
[HasShift C ℤ]
[Preadditive C]
[∀ (n : ℤ), (shiftFunctor C n).Additive]
[Pretriangulated C]
[IsTriangulated C]
{Λ : Type u'}
[AddCommGroup Λ]
{κ : K₀ C →+ Λ}
(σ : WithClassMap C κ)
(W : Λ →+ ℂ)
{r : ℝ}
(hr0 : 0 ≤ r)
(hr1 : r < 1)
(hW : WeakStabilityCondition.StabilityCondition.Deformation.stabilitySeminorm C σ (W - σ.Z) ≤ ENNReal.ofReal r)
{ε₀ : ℝ}
(hε₀10 : ε₀ < 1 / 10)
(hWide : WeakStabilityCondition.StabilityCondition.Deformation.WideSectorFiniteLength C σ ε₀)
{ε : ℝ}
(hε : 0 < ε)
(hεε₀ : ε < ε₀)
(hε2 : ε ≤ 1 / 2)
(hε8 : ε < 1 / 8)
(hsin :
WeakStabilityCondition.StabilityCondition.Deformation.stabilitySeminorm C σ (W - σ.Z) < ENNReal.ofReal (Real.sin (Real.pi * ε)))
{E : C}
{φ : ℝ}
(hP : σ.slicing.P φ E)
(hE : ¬Limits.IsZero E)
:
The owner deformed HN filtration of an old semistable object stays in
the closed phase window of radius ε. Its factors are nonzero.
theorem
CategoryTheory.Triangulated.StabilityCondition.WithClassMap.semistable_mem_deformedGt
(C : Type u)
[Category.{v, u} C]
[Limits.HasZeroObject C]
[HasShift C ℤ]
[Preadditive C]
[∀ (n : ℤ), (shiftFunctor C n).Additive]
[Pretriangulated C]
[IsTriangulated C]
{Λ : Type u'}
[AddCommGroup Λ]
{κ : K₀ C →+ Λ}
(σ : WithClassMap C κ)
(W : Λ →+ ℂ)
{r : ℝ}
(hr0 : 0 ≤ r)
(hr1 : r < 1)
(hW : WeakStabilityCondition.StabilityCondition.Deformation.stabilitySeminorm C σ (W - σ.Z) ≤ ENNReal.ofReal r)
{ε₀ : ℝ}
(hε₀10 : ε₀ < 1 / 10)
(hWide : WeakStabilityCondition.StabilityCondition.Deformation.WideSectorFiniteLength C σ ε₀)
{ε : ℝ}
(hε : 0 < ε)
(hεε₀ : ε < ε₀)
(hε2 : ε ≤ 1 / 2)
(hε8 : ε < 1 / 8)
(hsin :
WeakStabilityCondition.StabilityCondition.Deformation.stabilitySeminorm C σ (W - σ.Z) < ENNReal.ofReal (Real.sin (Real.pi * ε)))
{E : C}
{φ t : ℝ}
(hφ : t + 2 * ε ≤ φ)
(hP : σ.slicing.P φ E)
(hE : ¬Limits.IsZero E)
:
deformedGtPred C σ W hr0 hr1 hW ε t E
An old semistable object at least two deformation radii above t
belongs to the owner cut Q(>t).
theorem
CategoryTheory.Triangulated.StabilityCondition.WithClassMap.semistable_mem_deformedLt
(C : Type u)
[Category.{v, u} C]
[Limits.HasZeroObject C]
[HasShift C ℤ]
[Preadditive C]
[∀ (n : ℤ), (shiftFunctor C n).Additive]
[Pretriangulated C]
[IsTriangulated C]
{Λ : Type u'}
[AddCommGroup Λ]
{κ : K₀ C →+ Λ}
(σ : WithClassMap C κ)
(W : Λ →+ ℂ)
{r : ℝ}
(hr0 : 0 ≤ r)
(hr1 : r < 1)
(hW : WeakStabilityCondition.StabilityCondition.Deformation.stabilitySeminorm C σ (W - σ.Z) ≤ ENNReal.ofReal r)
{ε₀ : ℝ}
(hε₀10 : ε₀ < 1 / 10)
(hWide : WeakStabilityCondition.StabilityCondition.Deformation.WideSectorFiniteLength C σ ε₀)
{ε : ℝ}
(hε : 0 < ε)
(hεε₀ : ε < ε₀)
(hε2 : ε ≤ 1 / 2)
(hε8 : ε < 1 / 8)
(hsin :
WeakStabilityCondition.StabilityCondition.Deformation.stabilitySeminorm C σ (W - σ.Z) < ENNReal.ofReal (Real.sin (Real.pi * ε)))
{E : C}
{φ t : ℝ}
(hφ : φ ≤ t - 2 * ε)
(hP : σ.slicing.P φ E)
(hE : ¬Limits.IsZero E)
:
deformedLtPred C σ W hr0 hr1 hW ε t E
An old semistable object at least two deformation radii below t
belongs to the owner cut Q(<t).