The tilting property (Definition 14.12)

The tilting property from Definition 14.12 of arXiv:1902.08184v4, on the reviewed abstract layer. A weak prestability condition already carries its Harder--Narasimhan slicing, so the paper's condition muPlus F < +infinity is phrased here as phiPlus F < 1: for an object of the slicing heart these say that the largest HN factor is off the real-axis boundary. This is the same phase-language convention as WeakStabilityCondition/Tilting/TorsionPair/Slope.lean. The normalized slope--phase ray identity is formalized downstream in WeakStabilityCondition/Basic/ChargeRay.lean, and the exact finite-slope adapter is provided by Tilting/TorsionPair/SourceSlope.lean. The coverage coordinate remains mapped; review and owner-gated promotion are separate governance steps.

The short exact sequence F -> Ftilde -> F0 in part (2) is a distinguished triangle whose three vertices lie in the heart, following the convention of Basic.lean and Noetherian.lean. The condition Hom(A0, Ftilde[1]) = 0 is stated literally as vanishing of every such map.

Downstream source theorem

The categorical work is assembled in the Tilting modules: heart cohomology, the semistable classification, termination of zero-charge chains, the HN recursion, support transport, and reverse slicing. The exact source-facing statements now live in Tilting/Source:

• slopeTorsionPair is display (14.1) with its finite weak-slope parameter;
• sourceTiltWeakStabilityFunction_isSemistable_iff_classification is the sign-separated statement of Lemma 14.17;
• sourceTiltConclusion packages Proposition 14.16 with charge Z/(I-b), support, and the noetherian zero-charge torsion conclusion.

Those declarations do not by themselves promote the coverage registry past mapped; source review evidence and owner signoff remain required.

def CategoryTheory.Triangulated.WeakStabilityCondition.IsNoetherianTorsionSubcategory {C : Type u_1} [Category.{u_3, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (t : TStructure C) (B : ObjectProperty C) : Prop

An object property is a noetherian torsion subcategory when it is the torsion class of a NoetherianTorsionSubcategory. This exposes the class parameter suppressed by the data-carrying structure of Definition 14.6.

Equations

• CategoryTheory.Triangulated.WeakStabilityCondition.IsNoetherianTorsionSubcategory t B = ∃ (N : CategoryTheory.Triangulated.WeakStabilityCondition.NoetherianTorsionSubcategory t), N.pair.tors = B

def CategoryTheory.Triangulated.WeakStabilityCondition.WeakPreStabilityCondition.zeroCharge {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) : ObjectProperty C

The zero-charge subcategory of the slicing heart, for the ambient charge sigma.Z ∘ v. This is the A0 occurring in Definition 14.12.

Equations

• sigma.zeroCharge E = ((CategoryTheory.Triangulated.Slicing.toTStructure C sigma.slicing).heart E ∧ sigma.Z (v (CategoryTheory.Triangulated.K₀.of C E)) = 0)

def CategoryTheory.Triangulated.WeakStabilityCondition.WeakPreStabilityCondition.HasFiniteMaxSlope {C : Type u_1} [Category.{u_3, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {Lambda : Type u_2} [AddCommGroup Lambda] {v : K₀ C →+ Lambda} (sigma : WeakPreStabilityCondition v) (F : C) : Prop

The phase-language form of muPlus F < +infinity for a nonzero object of the slicing heart: its largest HN phase is strictly below the boundary phase 1.

Equations

• sigma.HasFiniteMaxSlope F = ∃ (hF : ¬CategoryTheory.Limits.IsZero F), CategoryTheory.Triangulated.Slicing.phiPlus C sigma.slicing F hF < 1

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

The envelope required by Definition 14.12(2): a heart short exact sequence F -> Ftilde -> F0 with zero-charge quotient and Hom(A0, Ftilde[1]) = 0.

Equations

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

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

A tilting envelope whose middle term is explicitly in the phase-cut torsion-free class. Rotating its defining triangle gives the short exact sequence in the tilted heart used in the proof of Proposition 14.16.

The paper obtains this membership implicitly when it passes from Definition 14.12(2) to 0 → F⁰ → F[1] → F̃[1] → 0. It is named here so that the heart-membership conversion is an independently checkable boundary; it is not added to TiltingProperty as an extra axiom.

Equations

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

theorem CategoryTheory.Triangulated.WeakStabilityCondition.WeakPreStabilityCondition.HasPhaseTiltingEnvelope.hasTiltingEnvelope {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 : ℝ} {F : C} (hbeta1 : beta ≤ 1) (h : sigma.HasPhaseTiltingEnvelope beta F) : sigma.HasTiltingEnvelope F

Forgetting the phase-cut membership recovers a Definition 14.12 envelope.

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

The tilting property, Definition 14.12 (phase-language form).

1. The zero-charge subcategory is noetherian torsion.
2. Every heart object whose largest HN phase is below 1 has a tilting envelope.

The support property of a weak stability condition is not used by this definition, so it is stated on the underlying weak prestability condition.

• zeroCharge_noetherian : IsNoetherianTorsionSubcategory (Slicing.toTStructure C sigma.slicing) sigma.zeroCharge

  Definition 14.12(1).

• exists_envelope (F : C) : (Slicing.toTStructure C sigma.slicing).heart F → sigma.HasFiniteMaxSlope F → sigma.HasTiltingEnvelope F

  Definition 14.12(2), with finite maximum slope in phase language.

theorem CategoryTheory.Triangulated.WeakStabilityCondition.WeakPreStabilityCondition.TiltingProperty.hasTiltingEnvelope_of_phaseFree {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) (h : sigma.TiltingProperty) (beta : ℝ) (hbeta1 : beta < 1) (F : C) (hF : phaseFree sigma.slicing beta F) : sigma.HasTiltingEnvelope F

Definition 14.12(2) supplies a raw tilting envelope for every object in a phase-cut torsion-free class. The zero object is handled by the contractible triangle; for a nonzero object, the leProp beta bound makes its largest phase strictly smaller than 1.

This deliberately returns HasTiltingEnvelope, not HasPhaseTiltingEnvelope: the raw envelope's middle term need not remain in P((0, beta]). Its Ext-vanishing is instead used to prove termination of zero-charge subobject chains after tilting.