Phase control inside an owner deformed interval #
The stability-seminorm estimate controls the perturbed phase of every old semistable factor. This module specializes that estimate to the midpoint branch used by owner skewed stability data and records the interval forms needed by phase-confinement and HN-assembly arguments.
theorem
CategoryTheory.Triangulated.StabilityCondition.WithClassMap.skewedPhase_sub_lt_of_stabilitySeminorm
(C : Type u)
[Category.{v, u} C]
[Limits.HasZeroObject C]
[HasShift C ℤ]
[Preadditive C]
[∀ (n : ℤ), (shiftFunctor C n).Additive]
[Pretriangulated 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}
(hP : σ.slicing.P φ E)
(hE : ¬Limits.IsZero E)
(haφ : a < φ)
(hφb : φ < b)
:
Every old nonzero semistable factor in a thin witness interval has its
perturbed phase within ε of its old phase.
theorem
CategoryTheory.Triangulated.StabilityCondition.WithClassMap.skewedPhase_mem_interval_of_stabilitySeminorm
(C : Type u)
[Category.{v, u} C]
[Limits.HasZeroObject C]
[HasShift C ℤ]
[Preadditive C]
[∀ (n : ℤ), (shiftFunctor C n).Additive]
[Pretriangulated 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}
(hP : σ.slicing.P φ E)
(hE : ¬Limits.IsZero E)
(haφ : a < φ)
(hφb : φ < b)
:
Interval form of the owner factor phase-control estimate.
theorem
CategoryTheory.Triangulated.StabilityCondition.WithClassMap.skewedPhase_mem_lower_branch
(C : Type u)
[Category.{v, u} C]
[Limits.HasZeroObject C]
[HasShift C ℤ]
[Preadditive C]
[∀ (n : ℤ), (shiftFunctor C n).Additive]
[Pretriangulated 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}
(hP : σ.slicing.P φ E)
(hE : ¬Limits.IsZero E)
(haφ : a < φ)
(hφb : φ < b)
:
The thin-witness factor phase lies in the common branch based at the lower endpoint.
theorem
CategoryTheory.Triangulated.StabilityCondition.WithClassMap.skewedPhase_mem_upper_branch
(C : Type u)
[Category.{v, u} C]
[Limits.HasZeroObject C]
[HasShift C ℤ]
[Preadditive C]
[∀ (n : ℤ), (shiftFunctor C n).Additive]
[Pretriangulated 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}
(hP : σ.slicing.P φ E)
(hE : ¬Limits.IsZero E)
(haφ : a < φ)
(hφb : φ < b)
:
The thin-witness factor phase lies in the common branch based at the upper endpoint.
theorem
CategoryTheory.Triangulated.StabilityCondition.WithClassMap.charge_ne_of_interval
(C : Type u)
[Category.{v, u} C]
[Limits.HasZeroObject C]
[HasShift C ℤ]
[Preadditive C]
[∀ (n : ℤ), (shiftFunctor C n).Additive]
[Pretriangulated 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}
(hI : Slicing.intervalProp C σ.slicing a b E)
(hE : ¬Limits.IsZero E)
:
The perturbed charge of a nonzero object in a thin owner interval cannot vanish.
theorem
CategoryTheory.Triangulated.StabilityCondition.WithClassMap.skewedPhase_mem_expanded_interval
(C : Type u)
[Category.{v, u} C]
[Limits.HasZeroObject C]
[HasShift C ℤ]
[Preadditive C]
[∀ (n : ℤ), (shiftFunctor C n).Additive]
[Pretriangulated 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}
(hI : Slicing.intervalProp C σ.slicing a b E)
(hE : ¬Limits.IsZero E)
:
Phase control on old semistable factors lifts to every nonzero object in the same thin owner interval.
theorem
CategoryTheory.Triangulated.StabilityCondition.WithClassMap.skewedPhase_eq_of_mem_branch
(C : Type u)
[Category.{v, u} C]
[Limits.HasZeroObject C]
[HasShift C ℤ]
[Preadditive C]
[∀ (n : ℤ), (shiftFunctor C n).Additive]
[Pretriangulated 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 c d : ℝ}
(hab : a < b)
(hcd : c < d)
{E : C}
(hcharge : W (classOf C κ E) ≠ 0)
(hbranch :
(WeakStabilityCondition.StabilityCondition.Deformation.skewedStabilityFunctionOfSeminormLtOne C σ W hr0 hr1 hW
hab).phase
E ∈ Set.Ioc
((WeakStabilityCondition.StabilityCondition.Deformation.skewedStabilityFunctionOfSeminormLtOne C σ W hr0 hr1 hW
hcd).α - 1)
((WeakStabilityCondition.StabilityCondition.Deformation.skewedStabilityFunctionOfSeminormLtOne C σ W hr0 hr1 hW
hcd).α + 1))
:
(WeakStabilityCondition.StabilityCondition.Deformation.skewedStabilityFunctionOfSeminormLtOne C σ W hr0 hr1 hW
hab).phase
E = (WeakStabilityCondition.StabilityCondition.Deformation.skewedStabilityFunctionOfSeminormLtOne C σ W hr0 hr1 hW
hcd).phase
E
Two owner skewed functions built from the same perturbed charge select the same phase whenever the charge is nonzero and one selected phase lies on the other's branch.
theorem
CategoryTheory.Triangulated.StabilityCondition.WithClassMap.skewedPhase_eq_of_common_interval
(C : Type u)
[Category.{v, u} C]
[Limits.HasZeroObject C]
[HasShift C ℤ]
[Preadditive C]
[∀ (n : ℤ), (shiftFunctor C n).Additive]
[Pretriangulated 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 c d ε : ℝ}
(hab : a < b)
(hcd : c < d)
(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 * ε)))
(hleft : (c + d) / 2 - 1 < a - ε)
(hright : b + ε ≤ (c + d) / 2 + 1)
{E : C}
(hI : Slicing.intervalProp C σ.slicing a b E)
(hE : ¬Limits.IsZero E)
:
(WeakStabilityCondition.StabilityCondition.Deformation.skewedStabilityFunctionOfSeminormLtOne C σ W hr0 hr1 hW
hab).phase
E = (WeakStabilityCondition.StabilityCondition.Deformation.skewedStabilityFunctionOfSeminormLtOne C σ W hr0 hr1 hW
hcd).phase
E
Two owner skewed functions agree on a shared nonzero interval object when the first interval's controlled phase window lies in the second branch.
theorem
CategoryTheory.Triangulated.StabilityCondition.WithClassMap.skewedSemistable_of_subinterval
(C : Type u)
[Category.{v, u} C]
[Limits.HasZeroObject C]
[HasShift C ℤ]
[Preadditive C]
[∀ (n : ℤ), (shiftFunctor C n).Additive]
[Pretriangulated 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 c d ε ψ : ℝ}
(hab : a < b)
(hcd : c < d)
(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 * ε)))
(hleft : (c + d) / 2 - 1 < a - ε)
(hright : b + ε ≤ (c + d) / 2 + 1)
(hmono : Slicing.intervalProp C σ.slicing c d ≤ Slicing.intervalProp C σ.slicing a b)
{E : C}
(hI : Slicing.intervalProp C σ.slicing c d E)
(hSS :
(WeakStabilityCondition.StabilityCondition.Deformation.skewedStabilityFunctionOfSeminormLtOne C σ W hr0 hr1 hW
hab).IsSemistable
E ψ)
:
(WeakStabilityCondition.StabilityCondition.Deformation.skewedStabilityFunctionOfSeminormLtOne C σ W hr0 hr1 hW
hcd).IsSemistable
E ψ
Perturbed semistability transports to a narrower interval presentation when the source phase window lies in the target branch.