The owner stability seminorm #
The stability seminorm of a charge homomorphism is the supremum of its norm relative to the central charge over all nonzero semistable objects.
noncomputable def
CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Deformation.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 →+ Λ}
(σ : StabilityCondition.WithClassMap C κ)
(U : Λ →+ ℂ)
:
The extended nonnegative stability seminorm of a charge homomorphism.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Deformation.charge_norm_pos
(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 →+ Λ}
(σ : StabilityCondition.WithClassMap C κ)
{E : C}
{φ : ℝ}
(hP : σ.slicing.P φ E)
(hE : ¬Limits.IsZero E)
:
The central charge of a nonzero semistable object has positive norm.
theorem
CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Deformation.ratio_le_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 →+ Λ}
(σ : StabilityCondition.WithClassMap C κ)
(U : Λ →+ ℂ)
{E : C}
{φ : ℝ}
(hP : σ.slicing.P φ E)
(hE : ¬Limits.IsZero E)
:
Every semistable ratio is bounded by the stability seminorm.
theorem
CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Deformation.stabilitySeminorm_nonneg
(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 →+ Λ}
(σ : StabilityCondition.WithClassMap C κ)
(U : Λ →+ ℂ)
:
The stability seminorm is nonnegative.
@[simp]
theorem
CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Deformation.stabilitySeminorm_zero
(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 →+ Λ}
(σ : StabilityCondition.WithClassMap C κ)
:
The zero charge homomorphism has zero stability seminorm.
@[simp]
theorem
CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Deformation.stabilitySeminorm_neg
(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 →+ Λ}
(σ : StabilityCondition.WithClassMap C κ)
(U : Λ →+ ℂ)
:
Negation preserves the stability seminorm.
theorem
CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Deformation.stabilitySeminorm_add_le
(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 →+ Λ}
(σ : StabilityCondition.WithClassMap C κ)
(U V : Λ →+ ℂ)
:
The owner stability seminorm satisfies the triangle inequality.
theorem
CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Deformation.semistableChargeBound_of_stabilitySeminorm_le
(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 →+ Λ}
(σ : StabilityCondition.WithClassMap C κ)
(W : Λ →+ ℂ)
{r : ℝ}
(hr : 0 ≤ r)
(h : stabilitySeminorm C σ (W - σ.Z) ≤ ENNReal.ofReal r)
:
SemistableChargeBound C σ W r
A real upper bound on the stability seminorm supplies the corresponding pointwise relative norm bound.
theorem
CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Deformation.semistableChargeBound_toReal
(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 →+ Λ}
(σ : StabilityCondition.WithClassMap C κ)
(W : Λ →+ ℂ)
(hfinite : stabilitySeminorm C σ (W - σ.Z) ≠ ⊤)
:
SemistableChargeBound C σ W (stabilitySeminorm C σ (W - σ.Z)).toReal
A finite stability seminorm supplies its toReal as a pointwise bound on
semistable charge perturbations.
noncomputable def
CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Deformation.skewedStabilityFunctionOfSeminormLtOne
(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 →+ Λ}
(σ : StabilityCondition.WithClassMap C κ)
(W : Λ →+ ℂ)
{r a b : ℝ}
(hr0 : 0 ≤ r)
(hr1 : r < 1)
(h : stabilitySeminorm C σ (W - σ.Z) ≤ ENNReal.ofReal r)
(hab : a < b)
:
SkewedStabilityFunction C κ σ.slicing a b
A stability-seminorm bound below one produces skewed stability data on every nonempty interval.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Deformation.relativePhase_perturbation_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 →+ Λ}
(σ : StabilityCondition.WithClassMap C κ)
(W : Λ →+ ℂ)
{E : C}
{φ α ε : ℝ}
(hP : σ.slicing.P φ E)
(hE : ¬Limits.IsZero E)
(hφα : φ ∈ Set.Ioo (α - 1 / 2) (α + 1 / 2))
(hε : 0 < ε)
(hε2 : ε ≤ 1 / 2)
(h : stabilitySeminorm C σ (W - σ.Z) < ENNReal.ofReal (Real.sin (Real.pi * ε)))
:
A strict stability-seminorm bound by sin (π ε) strictly controls the
selected phase of every old semistable object on a compatible branch.