Transfer of semistability across the tilt #
This file owns the transfer results: semistability on the original heart in the torsion and torsion-free cases, and semistability of an object whose rotated charge lies on a fixed ray.
theorem
CategoryTheory.Triangulated.WeakStabilityCondition.WeakPreStabilityCondition.weakStabilityFunctionOnHeart_isSemistable_of_phaseTors_phaseTiltSemistable
{C : Type u_1}
[Category.{u_3, u_1} C]
[Preadditive C]
[Limits.HasZeroObject C]
[HasShift C ℤ]
[∀ (n : ℤ), (shiftFunctor C n).Additive]
[Pretriangulated C]
[IsTriangulated C]
{Lambda : Type u_2}
[AddCommGroup Lambda]
{v : K₀ C →+ Lambda}
(sigma : WeakPreStabilityCondition v)
(beta : ℝ)
(hbeta0 : 0 < beta)
(hbeta1 : beta < 1)
{E : C}
(hEtors : phaseTors sigma.slicing beta E)
(hEss : (sigma.phaseTiltWeakStabilityFunction beta ⋯ hbeta1).IsSemistable E)
(hcharge : (sigma.phaseTiltWeakStabilityFunction beta ⋯ hbeta1).charge E ≠ 0)
:
A charged torsion-class object which is semistable after the phase tilt was already semistable in the original heart.
theorem
CategoryTheory.Triangulated.WeakStabilityCondition.WeakPreStabilityCondition.weakStabilityFunctionOnHeart_isSemistable_of_phaseFree_shiftSemistable
{C : Type u_1}
[Category.{u_3, u_1} C]
[Preadditive C]
[Limits.HasZeroObject C]
[HasShift C ℤ]
[∀ (n : ℤ), (shiftFunctor C n).Additive]
[Pretriangulated C]
[IsTriangulated C]
{Lambda : Type u_2}
[AddCommGroup Lambda]
{v : K₀ C →+ Lambda}
(sigma : WeakPreStabilityCondition v)
(beta : ℝ)
(hbeta0 : 0 ≤ beta)
(hbeta1 : beta < 1)
{U : C}
(hUfree : phaseFree sigma.slicing beta U)
(hUss : (sigma.phaseTiltWeakStabilityFunction beta hbeta0 hbeta1).IsSemistable ((shiftFunctor C 1).obj U))
(hcharge : (sigma.phaseTiltWeakStabilityFunction beta hbeta0 hbeta1).charge ((shiftFunctor C 1).obj U) ≠ 0)
:
If the shift of a charged torsion-free object is semistable in the tilted heart, the unshifted object is semistable in the original heart.
theorem
CategoryTheory.Triangulated.WeakStabilityCondition.WeakPreStabilityCondition.phaseTiltWeakStabilityFunction_isSemistable_of_ray
{C : Type u_1}
[Category.{u_3, u_1} C]
[Preadditive C]
[Limits.HasZeroObject C]
[HasShift C ℤ]
[∀ (n : ℤ), (shiftFunctor C n).Additive]
[Pretriangulated C]
[IsTriangulated C]
{Lambda : Type u_2}
[AddCommGroup Lambda]
{v : K₀ C →+ Lambda}
(sigma : WeakPreStabilityCondition v)
(beta : ℝ)
(hbeta0 : 0 ≤ beta)
(hbeta1 : beta < 1)
{E : C}
(hEtilt : (slicingTorsionPair sigma.slicing hbeta0 ⋯).tilt.heart E)
{theta m : ℝ}
(htheta : theta ∈ Set.Ioc 0 1)
(hm : 0 < m)
(hcharge :
(sigma.phaseTiltWeakStabilityFunction beta hbeta0 hbeta1).charge E = ↑m * Complex.exp (↑(Real.pi * theta) * Complex.I))
(hle : Slicing.leProp C sigma.slicing (beta + theta) E)
(hHom :
0 < ((sigma.phaseTiltWeakStabilityFunction beta hbeta0 hbeta1).charge E).im →
∀ (A0 : C), sigma.zeroCharge A0 → ∀ (f : A0 ⟶ E), f = 0)
:
(sigma.phaseTiltWeakStabilityFunction beta hbeta0 hbeta1).IsSemistable E
A ray criterion for semistability in the tilted heart. The object has a
single nonzero-charge phase theta; the Hom condition excludes zero-charge
subobjects when that ray lies in the open upper half-plane.