Source-facing Proposition 14.16 and Lemma 14.17

This file exposes the completed phase-language infrastructure with the exact slope cutoff, tilted heart, and central charge used in arXiv:1902.08184v4. In particular, the output charge is definitionally Z/(I-b), not merely a unit rotation of Z.

structure CategoryTheory.Triangulated.WeakStabilityCondition.WeakPreStabilityCondition.SourceTiltConclusion {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] {V : Type u_2} [NormedAddCommGroup V] [NormedSpace ℝ V] {v : K₀ C →+ V} (sigma : WeakPreStabilityCondition v) (b : ℝ) (htilt : sigma.TiltingProperty) (Zlin : V →ₗ[ℝ] ℂ) : Type (max u_1 u_2)

The conclusions of Proposition 14.16 with the exact source normalization. The weak prestability condition supplies the ambient slicing and HN filtrations; support upgrades it to weak stability, and zeroChargeNoetherian records the proposition's final assertion.

• condition : WeakPreStabilityCondition v

  The tilted weak prestability condition with charge Z/(I-b).

• condition_eq : self.condition = sigma.sourceTiltWeakPreStabilityConditionOfTiltingProperty b htilt

  The condition is the canonical source-normalized construction.

• support : (sigma.sourceTiltWeakStabilityFunction b).HasSupportProperty v (sourceTiltLinearCharge b Zlin)

  The support property for the exact source-normalized heart charge.

• zeroChargeNoetherian : NoetherianTorsionSubcategory (sigma.slopeTorsionPair b).tilt

  The new zero-charge subcategory is noetherian torsion.

• zeroCharge_tors : self.zeroChargeNoetherian.pair.tors = (sigma.sourceTiltWeakStabilityFunction b).zeroCharge

  Its torsion class is exactly the source-normalized zero-charge class.

noncomputable def CategoryTheory.Triangulated.WeakStabilityCondition.WeakPreStabilityCondition.sourceTiltConclusion {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] {V : Type u_2} [NormedAddCommGroup V] [NormedSpace ℝ V] {v : K₀ C →+ V} (sigma : WeakPreStabilityCondition v) (b : ℝ) (htilt : sigma.TiltingProperty) (Zlin : V →ₗ[ℝ] ℂ) (hcompat : ∀ (x : V), Zlin x = sigma.Z x) (hsupport : sigma.weakStabilityFunctionOnHeart.HasSupportProperty v Zlin) : sigma.SourceTiltConclusion b htilt Zlin

Proposition 14.16 (source normalization).

A weak prestability condition with the tilting and support properties tilts at every finite weak slope b. The returned central charge is exactly Z/(I-b), and the new zero-charge subcategory is noetherian torsion.

Equations

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

@[simp]

theorem CategoryTheory.Triangulated.WeakStabilityCondition.WeakPreStabilityCondition.sourceTiltConclusion_condition_Z {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] {V : Type u_2} [NormedAddCommGroup V] [NormedSpace ℝ V] {v : K₀ C →+ V} (sigma : WeakPreStabilityCondition v) (b : ℝ) (htilt : sigma.TiltingProperty) (Zlin : V →ₗ[ℝ] ℂ) (hcompat : ∀ (x : V), Zlin x = sigma.Z x) (hsupport : sigma.weakStabilityFunctionOnHeart.HasSupportProperty v Zlin) : (sigma.sourceTiltConclusion b htilt Zlin hcompat hsupport).condition.Z = sigma.sourceTiltLatticeCharge b

theorem CategoryTheory.Triangulated.WeakStabilityCondition.WeakPreStabilityCondition.sourceTiltWeakStabilityFunction_isSemistable_iff_phaseClassification {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] {V : Type u_2} [NormedAddCommGroup V] {v : K₀ C →+ V} (sigma : WeakPreStabilityCondition v) (b : ℝ) {E : C} (hEtilt : (sigma.slopeTorsionPair b).tilt.heart E) (hcharge : (sigma.sourceTiltWeakStabilityFunction b).charge E ≠ 0) : (sigma.sourceTiltWeakStabilityFunction b).IsSemistable E ↔ sigma.IsPhaseTiltTypeOne E ∨ sigma.IsPhaseTiltTypeTwo (slopeCutPhase b) ⋯ ⋯ E

Lemma 14.17 (source-normalized semistable classification).

The semistable objects for Z/(I-b) are exactly the two classes constructed in the phase-language classification. Here the cutoff inside those classes is definitionally the normalized phase of the paper's weak slope b.

theorem CategoryTheory.Triangulated.WeakStabilityCondition.WeakPreStabilityCondition.sourceTilt_typeOne_im_nonneg {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] {V : Type u_2} [NormedAddCommGroup V] {v : K₀ C →+ V} (sigma : WeakPreStabilityCondition v) (b : ℝ) {E : C} (hcharge : (sigma.sourceTiltWeakStabilityFunction b).charge E ≠ 0) (hE : sigma.IsPhaseTiltTypeOne E) : 0 ≤ (sigma.Z (v (K₀.of C E))).im

The first class of Lemma 14.17 has nonnegative original imaginary charge.

theorem CategoryTheory.Triangulated.WeakStabilityCondition.WeakPreStabilityCondition.sourceTilt_typeTwo_im_neg {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] {V : Type u_2} [NormedAddCommGroup V] {v : K₀ C →+ V} (sigma : WeakPreStabilityCondition v) (b : ℝ) {E : C} (hEtilt : (sigma.slopeTorsionPair b).tilt.heart E) (hcharge : (sigma.sourceTiltWeakStabilityFunction b).charge E ≠ 0) (hE : sigma.IsPhaseTiltTypeTwo (slopeCutPhase b) ⋯ ⋯ E) : (sigma.Z (v (K₀.of C E))).im < 0

The extension class of Lemma 14.17 has strictly negative original imaginary charge.

theorem CategoryTheory.Triangulated.WeakStabilityCondition.WeakPreStabilityCondition.sourceTiltWeakStabilityFunction_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] {V : Type u_2} [NormedAddCommGroup V] {v : K₀ C →+ V} (sigma : WeakPreStabilityCondition v) (b : ℝ) {E : C} (hEtilt : (sigma.slopeTorsionPair b).tilt.heart E) (hcharge : (sigma.sourceTiltWeakStabilityFunction b).charge E ≠ 0) : (sigma.sourceTiltWeakStabilityFunction b).IsSemistable E ↔ 0 ≤ (sigma.Z (v (K₀.of C E))).im ∧ sigma.IsPhaseTiltTypeOne E ∨ (sigma.Z (v (K₀.of C E))).im < 0 ∧ sigma.IsPhaseTiltTypeTwo (slopeCutPhase b) ⋯ ⋯ E

Lemma 14.17 (source coordinates). The two cases are separated by the sign of the imaginary part of the original charge.

The phase-free field the second branch used to carry is no longer a hypothesis: phaseFree_of_tiltHeart_triangle derives it from the standing hypotheses of the printed lemma. The branch still carries the positive-imaginary Hom implication, which is the positive-imaginary half of the printed moreover clause and is load-bearing: a split U⟦1⟧ ⊕ V with V a nonzero zero-charge object meets every other clause of case (2) and is not semistable, because Definition 14.2 gives a zero-charge subobject the slope +∞. Promotion of the coverage coordinate remains owner-gated on accepting that reading of the source.

theorem CategoryTheory.Triangulated.WeakStabilityCondition.WeakPreStabilityCondition.hom_eq_zero_of_zeroCharge_to_sourceTiltSemistable {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] {V : Type u_2} [NormedAddCommGroup V] {v : K₀ C →+ V} (sigma : WeakPreStabilityCondition v) (b : ℝ) {E A0 : C} (hE : (sigma.sourceTiltWeakStabilityFunction b).IsSemistable E) (hcharge : (sigma.sourceTiltWeakStabilityFunction b).charge E ≠ 0) (hA0 : sigma.zeroCharge A0) (hrefine : 0 < ((sigma.sourceTiltWeakStabilityFunction b).charge E).im ∨ (sigma.sourceTiltWeakStabilityFunction b).IsStable E) (f : A0 ⟶ E) : f = 0

The moreover clause of Lemma 14.17 for the exact source charge: positive imaginary part or strict source stability kills every map from an original zero-charge object.