Heart-level assembly for the weak upper tilt

This file gathers the three heart-level obligations in Proposition 14.16:

• the weak Harder--Narasimhan property;
• the noetherian zero-charge torsion subcategory;
• transport of the support property.

The generic HN recursion is discharged by hasHNProperty_of_quotientInduction; the noetherian structure is discharged by phaseTiltNoetherianTorsionSubcategoryOfTiltingProperty; and support is transported unconditionally by phaseTilt_hasSupportProperty.

The first constructor keeps the relative zero-charge chain condition and rank-decreasing quotient induction visible. The second discharges both from phase-compatible envelopes. The final constructor starts directly from the raw Definition 14.12 tilting property: envelope Ext-vanishing terminates zero-charge chains, while TiltHarderNarasimhan saturates the boundary factor and iterates the cohomological reduction over the original H⁻¹ and H⁰ HN filtrations.

structure CategoryTheory.Triangulated.WeakStabilityCondition.WeakPreStabilityCondition.PhaseTiltHeartObligations {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) (beta : ℝ) (hbeta0 : 0 ≤ beta) (hbeta1 : beta < 1) (Zlin : V →ₗ[ℝ] ℂ) : Type u_1

The heart-level input to the ambient phase-tilt constructor. It packages the HN, noetherian, and support conclusions without itself asserting a paper-level source statement.

• hasHN : (sigma.phaseTiltWeakStabilityFunction beta hbeta0 hbeta1).HasHNProperty

  Harder--Narasimhan filtrations for the rotated weak function.

• zeroChargeNoetherian : NoetherianTorsionSubcategory (slicingTorsionPair sigma.slicing hbeta0 ⋯).tilt

  The tilted zero-charge class, with its torsion-pair and chain data.

• zeroCharge_tors : self.zeroChargeNoetherian.pair.tors = (sigma.phaseTiltWeakStabilityFunction beta hbeta0 hbeta1).zeroCharge

  Its torsion class is exactly the new zero-charge class.

• support : (sigma.phaseTiltWeakStabilityFunction beta hbeta0 hbeta1).HasSupportProperty v (phaseTiltLinearCharge beta Zlin)

  Support for numerical classes of tilted weak-semistable objects.

noncomputable def CategoryTheory.Triangulated.WeakStabilityCondition.WeakPreStabilityCondition.phaseTiltHeartObligations {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) (beta : ℝ) (hbeta0 : 0 < beta) (hbeta1 : beta < 1) (htilt : sigma.TiltingProperty) (Zlin : V →ₗ[ℝ] ℂ) (hcompat : ∀ (x : V), Zlin x = sigma.Z x) (hsupport : sigma.weakStabilityFunctionOnHeart.HasSupportProperty v Zlin) (hacc : ∀ (E : C), (slicingTorsionPair sigma.slicing ⋯ ⋯).tilt.heart E → ∀ (c : SubobjectChain (slicingTorsionPair sigma.slicing ⋯ ⋯).tilt (sigma.phaseTiltWeakStabilityFunction beta ⋯ hbeta1).zeroCharge E), SubobjectChain.Terminates (slicingTorsionPair sigma.slicing ⋯ ⋯).tilt c) (rank : (slicingTorsionPair sigma.slicing ⋯ ⋯).tilt.heart.FullSubcategory → ℕ) (hquot : (sigma.phaseTiltWeakStabilityFunction beta ⋯ hbeta1).HasHNQuotientInduction rank) : sigma.PhaseTiltHeartObligations beta ⋯ hbeta1 Zlin

Assemble all heart-level obligations for Proposition 14.16 from its two remaining constructive seams.

Equations

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

noncomputable def CategoryTheory.Triangulated.WeakStabilityCondition.WeakPreStabilityCondition.phaseTiltHeartObligationsOfPhaseEnvelopes {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) (beta : ℝ) (hbeta0 : 0 < beta) (hbeta1 : beta < 1) (htilt : sigma.TiltingProperty) (Zlin : V →ₗ[ℝ] ℂ) (hcompat : ∀ (x : V), Zlin x = sigma.Z x) (hsupport : sigma.weakStabilityFunctionOnHeart.HasSupportProperty v Zlin) (henv : ∀ (F : C), phaseFree sigma.slicing beta F → sigma.HasPhaseTiltingEnvelope beta F) : sigma.PhaseTiltHeartObligations beta ⋯ hbeta1 Zlin

Assemble the heart-level obligations with the relative zero-charge chain condition discharged by phase-compatible envelopes. Compared with phaseTiltHeartObligations, this constructor removes the order-theoretic hacc input: the envelope reduction, reduced-chain termination, and pullback of the maximal zero-charge subobject are performed in TiltNoetherian.

The weak HN property is then obtained by boundary saturation followed by the H⁻¹ and H⁰ filtration inductions in TiltHarderNarasimhan; no external rank or quotient-induction premise remains.

Equations

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

noncomputable def CategoryTheory.Triangulated.WeakStabilityCondition.WeakPreStabilityCondition.phaseTiltHeartObligationsOfTiltingProperty {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) (beta : ℝ) (hbeta0 : 0 < beta) (hbeta1 : beta < 1) (htilt : sigma.TiltingProperty) (Zlin : V →ₗ[ℝ] ℂ) (hcompat : ∀ (x : V), Zlin x = sigma.Z x) (hsupport : sigma.weakStabilityFunctionOnHeart.HasSupportProperty v Zlin) : sigma.PhaseTiltHeartObligations beta ⋯ hbeta1 Zlin

Assemble all heart-level obligations for the weak upper tilt directly from Definition 14.12's raw TiltingProperty.

The raw envelope middle term is not asserted to be phase-free. Instead, phaseTilt_zeroChargeChain_terminates_of_tiltingEnvelope uses its Ext-vanishing to bound tilted zero-charge subobject chains; maximal subobjects then provide the phase-compatible decompositions consumed by the HN and noetherian assemblies.

Equations

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

theorem CategoryTheory.Triangulated.WeakStabilityCondition.WeakPreStabilityCondition.phaseTilt_hasHNPropertyOfTiltingProperty {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) (beta : ℝ) (hbeta0 : 0 < beta) (hbeta1 : beta < 1) (htilt : sigma.TiltingProperty) : (sigma.phaseTiltWeakStabilityFunction beta ⋯ hbeta1).HasHNProperty

Definition 14.12's tilting property supplies the heart-level HN property for the rotated weak stability function, independently of any numerical realization or support-property input.