Noetherian zero-charge objects after phase tilting #
This file proves the noetherianity part of the zero-charge comparison needed for Proposition 14.16. The tilted weak function has exactly the original zero-charge objects. A subobject of such an object in the tilted heart again has zero charge; its quotient therefore has zero charge as well. The zero-charge comparison puts all three terms back in the original heart, so the same distinguished triangle exhibits an original-heart subobject.
Consequently the original NoetherianTorsionSubcategory chain condition
applies to every tilted-heart subobject chain of a zero-charge object. The
result is stated using Mathlib's standard IsNoetherianObject, which supplies
the well-founded subobject order used to choose maximal zero-charge
subobjects in the remaining torsion-pair assembly.
In a heart short exact sequence 0 → Q → E → N → 0, if
Q is right-orthogonal to zero-charge objects, then every zero-charge
subobject of E maps monomorphically to N.
This is the kernel/image argument behind the injectivity sentence in the proof of Proposition 14.16.
A morphism from an original zero-charge object to an original phase-torsion object which is monic in the tilted heart is already monic in the original heart. Its original-heart kernel is again zero-charge, hence is an object of the tilted heart; tilted monicity then forces that kernel to vanish.
Original zero-charge objects lie in the phase-torsion class at every
cutoff below 1.
A phase-compatible tilting envelope rotates to a zero-charge subobject of
F[1] in the tilted heart whose quotient is right-orthogonal to all
zero-charge objects. This formalizes the first short exact sequence used in
the proof of Proposition 14.16.
A phase-compatible envelope of an original semistable object has a
semistable middle term. The middle term has no zero-charge subobjects by
strict phase separation (1 > beta), so the general saturation lemma applies
to the envelope's zero-charge quotient.
A raw Definition 14.12 tilting envelope makes every increasing chain of
tilted zero-charge subobjects of F[1] terminate.
The raw middle term is not required to lie in the phase-cut free class. For
each subobject A ⟶ F[1], the envelope's Ext-vanishing and triangle
exactness instead give a lift A ⟶ F⁰. Pulling F⁰ ⟶ F[1] back along
A ⟶ F[1] makes this lift canonical: the pullback maps epimorphically to
A and monomorphically to the original zero-charge object F⁰. The
original noetherian hypothesis stabilizes the pullback chain, after which
epimorphic cancellation forces the given chain to stabilize.
The semistable-reduction step of Proposition 19.5.
Let R be an extension of a shifted old semistable U[1] by a zero-charge
object, and assume U[1] is right-orthogonal to tilted zero-charge objects.
After quotienting R by its maximal zero-charge subobject, the resulting
quotient is tilted semistable and has the same charge as U[1].
The key diagram is the middle part of the kernel--cokernel sequence for the
composite from the maximal zero-charge subobject to the right-hand
zero-charge term. The composite is monic by
mono_comp_of_zeroCharge_of_rightOrthogonal, so that middle sequence is
short exact and identifies the quotient as an extension of U[1] by a new
zero-charge object.
Boundary-phase saturation.
The maximal zero-charge quotient of an extension of U[1] by a zero-charge
object is semistable without assuming in advance that U[1] is
right-orthogonal to zero-charge objects. Intersecting the maximal
zero-charge subobject with U[1] gives an original torsion object. The
six-term original-cohomology sequence identifies the quotient of that
intersection with Utilde[1] and supplies an envelope
U ⟶ Utilde ⟶ A0. Its inclusion into the maximal quotient forces the
envelope's right-orthogonality, so Utilde is semistable and the quotient is
of phase-tilt type two.
The chain-transfer step in Proposition 14.16.
Suppose 0 → Q → E → N → 0 is short exact in the tilted heart,
Q is right-orthogonal to tilted zero-charge objects, and N is an original
phase-torsion object. Every chain of zero-charge subobjects of E then maps
monomorphically to a chain of original zero-charge subobjects of N, so the
original noetherian torsion hypothesis forces it to terminate.
Zero-charge decompositions of shifted phase-free objects discharge the relative-chain seam in the noetherian assembly.
For E in the tilted heart, compose the envelope subobject
A⁰ ⟶ H⁻¹(E)[1] with the canonical cohomology subobject
H⁻¹(E)[1] ⟶ E. The kernel--cokernel sequence of this composite gives a
short exact sequence
coker(A⁰ ⟶ H⁻¹(E)[1]) ⟶ coker(A⁰ ⟶ E) ⟶ H⁰(E).
Its left term is right-orthogonal by the supplied decomposition and its right
term is an original phase-torsion object, so
phaseTilt_zeroChargeChain_terminates_of_rightOrthogonal constructs a maximal
zero-charge subobject of the middle term. The general pullback lemma
hasZeroChargeDecomposition_of_reduction then lifts that decomposition
across A⁰ ⟶ E.
Phase-compatible envelopes provide the shifted decompositions consumed
by phaseTilt_hasZeroChargeDecompositions_of_freeShiftDecompositions.
Raw Definition 14.12 envelopes provide the phase-compatible shifted
decompositions needed after tilting. The bridge does not strengthen the raw
middle term to a phase-free object: it first applies
phaseTilt_zeroChargeChain_terminates_of_tiltingEnvelope, then chooses a
maximal tilted zero-charge subobject.
Every tilted-heart zero-charge object is noetherian when the original zero-charge class is the torsion class of a noetherian torsion subcategory.
This is independent of the still-open construction of the zero-charge torsion pair on the whole tilted heart: it proves the intrinsic noetherianity of the objects which will form that torsion class.
Once the original zero-charge objects have been made into a torsion pair
on the tilted heart, their intrinsic noetherianity upgrades that pair to a
NoetherianTorsionSubcategory.
The proof factors every chain of torsion subobjects through the torsion term
of the chosen torsion/free decomposition. That term has zero charge, hence
is a noetherian object by
phaseTilt_isNoetherianObject_of_zeroCharge; stabilization in its standard
subobject lattice forces the original chain maps to be isomorphisms.
Equations
- sigma.phaseTiltNoetherianTorsionSubcategory beta hbeta0 hbeta1 N hN Psharp hP = { pair := Psharp, noetherian := ⋯ }
Instances For
Termination of zero-charge subobject chains in every tilted-heart object
produces the zero-charge torsion decompositions by the maximal-subobject
construction in Noetherian.lean.
This is the precise order-theoretic seam in the proof of Proposition 14.16: the envelope argument is responsible only for this relative chain condition; images, pullbacks, right orthogonality, and the resulting torsion pair are then automatic.
The noetherian zero-charge obligation after tilting, assembled directly
from zero-charge decompositions in the tilted heart. This removes the
intermediate HeartTorsionPair parameter from
phaseTiltNoetherianTorsionSubcategory: once the maximal-subobject argument
has produced the decompositions, both the torsion pair and its chain condition
are automatic.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Definition 14.12(1) supplies the original noetherian torsion class, so after the maximal-subobject argument has produced tilted zero-charge decompositions, the full noetherian torsion obligation of Proposition 14.16 is assembled without any further input.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The noetherian zero-charge torsion structure assembled from Definition 14.12(1) and phase-compatible instances of its envelope clause. Unlike the older chain-condition constructor, this version performs the envelope reduction, reduced-chain argument, and pullback internally.
Equations
- sigma.phaseTiltNoetherianTorsionSubcategoryOfPhaseEnvelopes beta hbeta0 hbeta1 htilt henv = sigma.phaseTiltNoetherianTorsionSubcategoryOfTiltingProperty beta hbeta0 hbeta1 htilt ⋯
Instances For
The noetherian tilted zero-charge torsion structure constructed directly
from Definition 14.12. Its raw envelope clause is restricted to the
phase-cut free class by TiltingProperty.hasTiltingEnvelope_of_phaseFree,
then converted to tilted zero-charge decompositions by chain termination.
Equations
- sigma.phaseTiltNoetherianTorsionSubcategoryOfTiltingEnvelopes beta hbeta0 hbeta1 htilt = sigma.phaseTiltNoetherianTorsionSubcategoryOfTiltingProperty beta hbeta0 hbeta1 htilt ⋯
Instances For
The full noetherian zero-charge torsion structure, with the relative chain condition as its only remaining envelope-level input.
Equations
- sigma.phaseTiltNoetherianTorsionSubcategoryOfChainCondition beta hbeta0 hbeta1 htilt hacc = sigma.phaseTiltNoetherianTorsionSubcategoryOfTiltingProperty beta hbeta0 hbeta1 htilt ⋯