Skewed stability data on an owner interval #
A perturbed charge need not itself define a stability condition yet. On a thin interval it supplies a skewed phase whenever it is nonzero on the old semistable factors. This module owns that intermediate object and its triangle-additive phase comparisons.
structure
CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Deformation.SkewedStabilityFunction
(C : Type u)
[Category.{v, u} C]
[Limits.HasZeroObject C]
[HasShift C ℤ]
[Preadditive C]
[∀ (n : ℤ), (shiftFunctor C n).Additive]
[Pretriangulated C]
{Λ : Type u'}
[AddCommGroup Λ]
(v : K₀ C →+ Λ)
(s : Slicing C)
(a b : ℝ)
:
Type u'
A perturbed central charge on the owner interval P((a,b)), with a branch
centre and nonvanishing on the original semistable factors in that interval.
The perturbed central charge.
- α : ℝ
The centre of the chosen phase branch.
The branch centre lies in the interval.
The perturbed charge does not vanish on old nonzero semistable factors.
Instances For
@[reducible, inline]
abbrev
CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Deformation.SkewedStabilityFunction.charge
{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 →+ Λ}
{s : Slicing C}
{a b : ℝ}
(F : SkewedStabilityFunction C κ s a b)
(E : C)
:
The perturbed charge of an ambient object.
Equations
- F.charge E = F.W (CategoryTheory.Triangulated.classOf C κ E)
Instances For
@[reducible, inline]
noncomputable abbrev
CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Deformation.SkewedStabilityFunction.phase
{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 →+ Λ}
{s : Slicing C}
{a b : ℝ}
(F : SkewedStabilityFunction C κ s a b)
(E : C)
:
The perturbed phase on the branch selected by the skewed data.
Equations
Instances For
@[reducible, inline]
abbrev
CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Deformation.SkewedStabilityFunction.ChargeNe
{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 →+ Λ}
{s : Slicing C}
{a b : ℝ}
(F : SkewedStabilityFunction C κ s a b)
(E : C)
:
Nonvanishing of an object's perturbed charge.
Instances For
theorem
CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Deformation.SkewedStabilityFunction.phase_congr
{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 →+ Λ}
{s : Slicing C}
{a b : ℝ}
(F : SkewedStabilityFunction C κ s a b)
{E E' : C}
(h : F.charge E = F.charge E')
:
Equal perturbed charges have equal phases.
theorem
CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Deformation.SkewedStabilityFunction.phase_iso
{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 →+ Λ}
{s : Slicing C}
{a b : ℝ}
(F : SkewedStabilityFunction C κ s a b)
{E E' : C}
(e : E ≅ E')
:
Isomorphic objects have equal perturbed phases.
theorem
CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Deformation.SkewedStabilityFunction.charge_triangle
{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 →+ Λ}
{s : Slicing C}
{a b : ℝ}
(F : SkewedStabilityFunction C κ s a b)
(T : Pretriangulated.Triangle C)
(hT : T ∈ Pretriangulated.distinguishedTriangles)
:
Perturbed charges are additive along distinguished triangles.
theorem
CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Deformation.SkewedStabilityFunction.phase_seesaw
{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 →+ Λ}
{s : Slicing C}
{a b : ℝ}
(F : SkewedStabilityFunction C κ s a b)
{E E₁ E₂ : C}
{ψ : ℝ}
(hsum : F.charge E₁ + F.charge E₂ = F.charge E)
(hψ : F.phase E = ψ)
(hE₁_range : F.phase E₁ ∈ Set.Ioc (ψ - 1) ψ)
(hE₂_ne : F.ChargeNe E₂)
(hE₂_range : F.phase E₂ ∈ Set.Ioo (ψ - 1) (ψ + 1))
:
The charge-level phase see-saw for ambient objects.
theorem
CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Deformation.SkewedStabilityFunction.phase_seesaw_strict
{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 →+ Λ}
{s : Slicing C}
{a b : ℝ}
(F : SkewedStabilityFunction C κ s a b)
{E E₁ E₂ : C}
{ψ : ℝ}
(hsum : F.charge E₁ + F.charge E₂ = F.charge E)
(hψ : F.phase E = ψ)
(hE₂_lt : F.phase E₂ < ψ)
(hE₂_ne : F.ChargeNe E₂)
(hE₂_range : F.phase E₂ ∈ Set.Ioo (ψ - 1) (ψ + 1))
(hE₁_range : F.phase E₁ ∈ Set.Ioo (ψ - 1) (ψ + 1))
:
Strict charge-level phase see-saw for ambient objects.
structure
CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Deformation.SkewedStabilityFunction.IsSemistable
{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 →+ Λ}
{s : Slicing C}
{a b : ℝ}
(F : SkewedStabilityFunction C κ s a b)
(E : C)
(ψ : ℝ)
:
An interval object is semistable for the perturbed charge when every admissible nonzero subobject triangle has phase at most its phase.
- interval : Slicing.intervalProp C s a b E
The object lies in the old thin interval.
- nonzero : ¬Limits.IsZero E
The object is nonzero.
- charge_ne : F.ChargeNe E
Its perturbed charge is nonzero.
Its chosen perturbed phase is
ψ.- phase_le_of_triangle ⦃K Q : C⦄ ⦃i : K ⟶ E⦄ ⦃q : E ⟶ Q⦄ ⦃δ : Q ⟶ (shiftFunctor C 1).obj K⦄ : Pretriangulated.Triangle.mk i q δ ∈ Pretriangulated.distinguishedTriangles → Slicing.intervalProp C s a b K → Slicing.intervalProp C s a b Q → ¬Limits.IsZero K → F.phase K ≤ ψ
Every nonzero subobject represented by an interval triangle has phase at most
ψ.
Instances For
theorem
CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Deformation.SkewedStabilityFunction.IsSemistable.phase_le_of_quotient_triangle
{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 →+ Λ}
{s : Slicing C}
{a b : ℝ}
{F : SkewedStabilityFunction C κ s a b}
{E : C}
{ψ : ℝ}
(h : F.IsSemistable E ψ)
{K Q : C}
{i : K ⟶ E}
{q : E ⟶ Q}
{δ : Q ⟶ (shiftFunctor C 1).obj K}
(hT : Pretriangulated.Triangle.mk i q δ ∈ Pretriangulated.distinguishedTriangles)
(hQcharge : F.ChargeNe Q)
(hQrange : F.phase Q ∈ Set.Ioo (ψ - 1) (ψ + 1))
(hKrange : ¬Limits.IsZero K → F.phase K ∈ Set.Ioc (ψ - 1) ψ)
:
A nonzero quotient in an admissible interval triangle has phase at least that of a skewed-semistable object, provided all three selected phases lie on the same branch.
theorem
CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Deformation.SkewedStabilityFunction.IsSemistable.phase_mem_Ioc
{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 →+ Λ}
{s : Slicing C}
{a b : ℝ}
{F : SkewedStabilityFunction C κ s a b}
{E : C}
{ψ : ℝ}
(h : F.IsSemistable E ψ)
:
A perturbed-semistable object's phase lies on its chosen branch.
theorem
CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Deformation.SkewedStabilityFunction.IsSemistable.charge_polar
{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 →+ Λ}
{s : Slicing C}
{a b : ℝ}
{F : SkewedStabilityFunction C κ s a b}
{E : C}
{ψ : ℝ}
(h : F.IsSemistable E ψ)
:
Polar form of the charge of a perturbed-semistable object.
theorem
CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Deformation.SkewedStabilityFunction.IsSemistable.ofIso
{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 →+ Λ}
{s : Slicing C}
{a b : ℝ}
{F : SkewedStabilityFunction C κ s a b}
{E E' : C}
{ψ : ℝ}
(h : F.IsSemistable E ψ)
(e : E ≅ E')
:
F.IsSemistable E' ψ
Transport perturbed semistability across an isomorphism of ambient objects.
theorem
CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Deformation.SkewedStabilityFunction.IsSemistable.ofCompatibleInterval
{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 →+ Λ}
{s : Slicing C}
{a b c d : ℝ}
{F : SkewedStabilityFunction C κ s a b}
{G : SkewedStabilityFunction C κ s c d}
{E : C}
{ψ : ℝ}
(h : F.IsSemistable E ψ)
(hI : Slicing.intervalProp C s c d E)
(hmono : Slicing.intervalProp C s c d ≤ Slicing.intervalProp C s a b)
(hcharge : G.charge E = F.charge E)
(hphaseE : G.phase E = F.phase E)
(hphaseSub : ∀ {K : C}, Slicing.intervalProp C s c d K → ¬Limits.IsZero K → G.phase K = F.phase K)
:
G.IsSemistable E ψ
Transport skewed semistability to a second interval presentation once the admissible triangles widen to the old interval and the selected phases agree on the ambient object and every nonzero candidate subobject.