The phase-language classification of tilted semistable objects

This file owns the two source-shaped classes of Lemma 14.17 of arXiv:1902.08184v4, IsPhaseTiltTypeOne and IsPhaseTiltTypeTwo, proves each gives a semistable object of the tilted heart, proves the converse from the canonical original-cohomology sequence and strict old-HN phase separation, and records the resulting characterisation.

This is the module a consumer of Lemma 14.17 should import.

def CategoryTheory.Triangulated.WeakStabilityCondition.WeakPreStabilityCondition.IsPhaseTiltTypeOne {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) (E : C) : Prop

The first class in the phase-language form of Lemma 14.17: an original heart semistable object with no maps from original zero-charge objects.

Equations

• sigma.IsPhaseTiltTypeOne E = (sigma.weakStabilityFunctionOnHeart.IsSemistable E ∧ ∀ (A0 : C), sigma.zeroCharge A0 → ∀ (f : A0 ⟶ E), f = 0)

def CategoryTheory.Triangulated.WeakStabilityCondition.WeakPreStabilityCondition.IsPhaseTiltTypeTwo {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) : Prop

The second class in the phase-language form of Lemma 14.17: an extension of a zero-charge object by the shift of a semistable object of the original heart. These are exactly the hypotheses the printed case (2) records: the free-class membership of U is not carried here, because it is automatic by phaseFree_of_tiltHeart_triangle.

The final implication is the positive-imaginary part of the lemma's moreover clause. It is retained because it is load-bearing rather than decorative: without it a split extension U⟦1⟧ ⊕ V with V a nonzero zero-charge object satisfies every other clause while failing semistability, since Definition 14.2 gives a zero-charge subobject the slope +∞.

Equations

• One or more equations did not get rendered due to their size.

theorem CategoryTheory.Triangulated.WeakStabilityCondition.WeakPreStabilityCondition.isSemistable_of_isPhaseTiltTypeOne {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) (hcharge : (sigma.phaseTiltWeakStabilityFunction beta hbeta0 hbeta1).charge E ≠ 0) (hE : sigma.IsPhaseTiltTypeOne E) : (sigma.phaseTiltWeakStabilityFunction beta hbeta0 hbeta1).IsSemistable E

Objects of the first class are semistable for the phase-tilted weak stability function.

theorem CategoryTheory.Triangulated.WeakStabilityCondition.WeakPreStabilityCondition.isSemistable_of_isPhaseTiltTypeTwo {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) (hcharge : (sigma.phaseTiltWeakStabilityFunction beta hbeta0 hbeta1).charge E ≠ 0) (hE : sigma.IsPhaseTiltTypeTwo beta hbeta0 hbeta1 E) : (sigma.phaseTiltWeakStabilityFunction beta hbeta0 hbeta1).IsSemistable E

Objects of the second class are semistable for the phase-tilted weak stability function.

theorem CategoryTheory.Triangulated.WeakStabilityCondition.WeakPreStabilityCondition.phaseTiltClassification_of_isSemistable {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} (hE : (sigma.phaseTiltWeakStabilityFunction beta ⋯ hbeta1).IsSemistable E) (hcharge : (sigma.phaseTiltWeakStabilityFunction beta ⋯ hbeta1).charge E ≠ 0) : sigma.IsPhaseTiltTypeOne E ∨ sigma.IsPhaseTiltTypeTwo beta ⋯ hbeta1 E

The reverse direction of the phase-language form of Lemma 14.17. The canonical original-cohomology sequence splits a tilted-semistable object into H⁻¹(E)[1] and H⁰(E); strict phase separation forces one of those two terms to have zero charge.

theorem CategoryTheory.Triangulated.WeakStabilityCondition.WeakPreStabilityCondition.isSemistable_of_phaseTiltClassification {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) (hcharge : (sigma.phaseTiltWeakStabilityFunction beta hbeta0 hbeta1).charge E ≠ 0) (hE : sigma.IsPhaseTiltTypeOne E ∨ sigma.IsPhaseTiltTypeTwo beta hbeta0 hbeta1 E) : (sigma.phaseTiltWeakStabilityFunction beta hbeta0 hbeta1).IsSemistable E

The constructive direction of the phase-language classification: either class described in Lemma 14.17 gives a semistable object in the tilted heart.

theorem CategoryTheory.Triangulated.WeakStabilityCondition.WeakPreStabilityCondition.phaseTiltWeakStabilityFunction_isSemistable_iff_classification {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 ⋯ ⋯).tilt.heart E) (hcharge : (sigma.phaseTiltWeakStabilityFunction beta ⋯ hbeta1).charge E ≠ 0) : (sigma.phaseTiltWeakStabilityFunction beta ⋯ hbeta1).IsSemistable E ↔ sigma.IsPhaseTiltTypeOne E ∨ sigma.IsPhaseTiltTypeTwo beta ⋯ hbeta1 E

Full phase-language classification of nonzero-charge semistable objects after tilting, combining both directions of Lemma 14.17. The strict lower bound on beta records that a finite slope cutoff corresponds to a phase cut strictly inside (0, 1).