Owner phase confinement for perturbed semistable objects #
Cutoff triangles inside a thin old phase interval, together with rotated-charge signs, confine the intrinsic old phases of a perturbed-semistable object.
theorem
CategoryTheory.Triangulated.StabilityCondition.WithClassMap.skewed_phiPlus_le
(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)
{a b ε ψ : ℝ}
(hab : a < b)
(hε : 0 < ε)
(hε2 : ε ≤ 1 / 2)
(hthin : b - a + 2 * ε < 1)
(hsin :
WeakStabilityCondition.StabilityCondition.Deformation.stabilitySeminorm C σ (W - σ.Z) < ENNReal.ofReal (Real.sin (Real.pi * ε)))
{E : C}
(hSS :
(WeakStabilityCondition.StabilityCondition.Deformation.skewedStabilityFunctionOfSeminormLtOne C σ W hr0 hr1 hW
hab).IsSemistable
E ψ)
:
The intrinsic highest old phase of an owner perturbed-semistable object is at most its perturbed phase plus the deformation radius.
theorem
CategoryTheory.Triangulated.StabilityCondition.WithClassMap.skewed_phiMinus_ge
(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)
{a b ε ψ : ℝ}
(hab : a < b)
(hε : 0 < ε)
(hε2 : ε ≤ 1 / 2)
(hthin : b - a + 2 * ε < 1)
(hsin :
WeakStabilityCondition.StabilityCondition.Deformation.stabilitySeminorm C σ (W - σ.Z) < ENNReal.ofReal (Real.sin (Real.pi * ε)))
{E : C}
(hSS :
(WeakStabilityCondition.StabilityCondition.Deformation.skewedStabilityFunctionOfSeminormLtOne C σ W hr0 hr1 hW
hab).IsSemistable
E ψ)
:
The intrinsic lowest old phase of an owner perturbed-semistable object is at least its perturbed phase minus the deformation radius.
theorem
CategoryTheory.Triangulated.StabilityCondition.WithClassMap.deformedPred_intrinsic_bounds
(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ε : 0 < ε)
(hε2 : ε ≤ 1 / 2)
(hsin :
WeakStabilityCondition.StabilityCondition.Deformation.stabilitySeminorm C σ (W - σ.Z) < ENNReal.ofReal (Real.sin (Real.pi * ε)))
{E : C}
(h : deformedPred C σ W hr0 hr1 hW ε ψ E)
(hE : ¬Limits.IsZero E)
:
A nonzero owner deformed-slice object has both intrinsic old phase bounds predicted by its phase and the deformation radius.
theorem
CategoryTheory.Triangulated.StabilityCondition.WithClassMap.deformedPred_geProp
(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ε : 0 < ε)
(hε2 : ε ≤ 1 / 2)
(hsin :
WeakStabilityCondition.StabilityCondition.Deformation.stabilitySeminorm C σ (W - σ.Z) < ENNReal.ofReal (Real.sin (Real.pi * ε)))
:
Every owner deformed-slice object lies above its weak old lower phase cut.
theorem
CategoryTheory.Triangulated.StabilityCondition.WithClassMap.deformedPred_leProp
(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ε : 0 < ε)
(hε2 : ε ≤ 1 / 2)
(hsin :
WeakStabilityCondition.StabilityCondition.Deformation.stabilitySeminorm C σ (W - σ.Z) < ENNReal.ofReal (Real.sin (Real.pi * ε)))
:
Every owner deformed-slice object lies below its weak old upper phase cut.
theorem
CategoryTheory.Triangulated.StabilityCondition.WithClassMap.deformedPred_intervalProp
(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ε : 0 < ε)
(hε2 : ε ≤ 1 / 2)
(hsin :
WeakStabilityCondition.StabilityCondition.Deformation.stabilitySeminorm C σ (W - σ.Z) < ENNReal.ofReal (Real.sin (Real.pi * ε)))
(hδ : 0 < δ)
:
Adding any positive padding turns weak confinement of an owner deformed slice into membership in an open old phase interval.
theorem
CategoryTheory.Triangulated.StabilityCondition.WithClassMap.intervalProp_of_deformed_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)
{ε a b δ : ℝ}
(hε : 0 < ε)
(hε2 : ε ≤ 1 / 2)
(hsin :
WeakStabilityCondition.StabilityCondition.Deformation.stabilitySeminorm C σ (W - σ.Z) < ENNReal.ofReal (Real.sin (Real.pi * ε)))
(hδ : 0 < δ)
{E : C}
(G : HNFiltration C (deformedPred C σ W hr0 hr1 hW ε) E)
(hphase : ∀ (i : Fin G.n), a ≤ G.φ i ∧ G.φ i ≤ b)
:
An owner HN filtration by deformed slices inside a common phase window places its ambient object in the corresponding padded old phase interval.
theorem
CategoryTheory.Triangulated.StabilityCondition.WithClassMap.deformedGtPred_gtProp
(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)
{ε t : ℝ}
(hε : 0 < ε)
(hε2 : ε ≤ 1 / 2)
(hsin :
WeakStabilityCondition.StabilityCondition.Deformation.stabilitySeminorm C σ (W - σ.Z) < ENNReal.ofReal (Real.sin (Real.pi * ε)))
:
The extension-closed owner cut Q(>t) lies above the old phase cutoff
t-ε.
theorem
CategoryTheory.Triangulated.StabilityCondition.WithClassMap.deformedLePred_leProp
(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)
{ε t : ℝ}
(hε : 0 < ε)
(hε2 : ε ≤ 1 / 2)
(hsin :
WeakStabilityCondition.StabilityCondition.Deformation.stabilitySeminorm C σ (W - σ.Z) < ENNReal.ofReal (Real.sin (Real.pi * ε)))
:
The extension-closed owner cut Q(≤t) lies below the old phase cutoff
t+ε.
theorem
CategoryTheory.Triangulated.StabilityCondition.WithClassMap.deformedLtPred_ltProp
(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)
{ε t : ℝ}
(hε : 0 < ε)
(hε2 : ε ≤ 1 / 2)
(hsin :
WeakStabilityCondition.StabilityCondition.Deformation.stabilitySeminorm C σ (W - σ.Z) < ENNReal.ofReal (Real.sin (Real.pi * ε)))
:
The extension-closed owner cut Q(<t) lies strictly below the old phase
cutoff t+ε.