Noetherian torsion subcategories (Definition 14.6) #
The noetherian-torsion layer of §14 of arXiv:1902.08184v4: subobject chains
in the heart, the termination condition, noetherian torsion subcategories,
and the identification of a torsion pair's free class with the right
orthogonal of its torsion class — the place free_of_orthogonal (#94) was
built for.
The design decision, recorded (Remark 14.7 as the definition) #
Definition 14.6 calls B ⊆ A a noetherian torsion subcategory if B is an
abelian subcategory, B is a noetherian abelian category, and (B, B^⊥) is
a torsion pair in A. The pin supplies an abelian instance on the full heart,
but B here is an object property inside the ambient category; there is no
bundled abelian-category/noetherian structure on that property whose
equivalence with the chain condition is available. Remark 14.7 characterises
the notion for extension-closed
B: every increasing chain of B-subobjects of a fixed E ∈ A
terminates. That chain condition is statable — a subobject is a heart
monomorphism, which is a map whose cone is again in the heart — and it is
what every use in §14 consumes (Lemmas 14.8, 14.11, Remark 14.14, and the
proof of Proposition 14.16 all run on chain termination, never on the
abstract noetherian-ness). So the chain condition is the definition
here, the torsion-pair half is carried as a HeartTorsionPair, and the
equivalence of Remark 14.7 is not claimed — it is the textbook
justification for the choice, not a theorem of this file.
What is deliberately NOT declared here #
Lemmas 14.8 and 14.11 are statable but left undeclared, per the standing rule that absent beats sorry-backed. What their proofs need, precisely:
- Lemma 14.8 (
A⁰noetherian torsion +Zoverℚ[i]⟹Anoetherian): the proof runs on surjection chains, kernels of composites, maximal subobjects withℑZ = 0extracted from HN filtrations, and a discreteness argument for the charge image. Missing at the pin: kernel and image lemmas needed by the maximal-subobject construction and a formalization decision for "Z defined over ℚ[i]" that makes the discreteness step honest. The abelian weak-HN package and its existence for the slicing heart are now available inHarderNarasimhan.lean. - Lemma 14.11 (bounded-slope chains terminate): the statement needs only
slopeand the chains below; the proof needsμ⁺/μ⁻from HN data, the compact-parallelogram argument, and the finitely-many-HN-classes input of Remark 12.3, which is support-property infrastructure.
The remaining kernel/image, discreteness and support inputs should be added in focused modules before these two lemmas are attempted; #108 records the definitions and the boundary.
Heart monomorphisms and subobject chains #
A map between heart objects is a heart monomorphism when its cone is
again in the heart: for heart objects, a distinguished triangle
A ⟶ E ⟶ Q with Q in the heart is a short exact sequence
0 → A → E → Q → 0, so this is exactly "A is a subobject of E with
quotient Q".
Equations
- One or more equations did not get rendered due to their size.
Instances For
An increasing chain of B-subobjects of a fixed heart object E
(Remark 14.7's data): objects obj i of class B, each a heart subobject
of the next and of E, compatibly.
- obj : ℕ → C
The chain objects.
Every chain object is of class
B.The inclusion of each chain object into the next.
The inclusion of each chain object into
E.- step_mono (i : ℕ) : IsHeartMono t (self.step i)
Each step is a heart monomorphism.
- toAmbient_mono (i : ℕ) : IsHeartMono t (self.toAmbient i)
Each inclusion into
Eis a heart monomorphism. The inclusions are compatible with the steps.
Instances For
A chain terminates when all steps are eventually isomorphisms.
Equations
- CategoryTheory.Triangulated.WeakStabilityCondition.SubobjectChain.Terminates t c = ∃ (N : ℕ), ∀ (i : ℕ), N ≤ i → CategoryTheory.IsIso (c.step i)
Instances For
Definition 14.6, in the chain form #
A noetherian torsion subcategory of the heart of t
(Definition 14.6, with Remark 14.7's chain characterisation as the
noetherian-ness — see the module docstring for why): a torsion pair on the
heart whose torsion class satisfies the ascending chain condition on
subobjects of every heart object.
- pair : Tilting.HeartTorsionPair t
The torsion pair
(B, B^⊥). - noetherian (E : C) : t.heart E → ∀ (c : SubobjectChain t self.pair.tors E), SubobjectChain.Terminates t c
Chain termination: every increasing chain of torsion subobjects of a heart object terminates.
Instances For
The right orthogonal of a class inside the heart: heart objects
receiving no nonzero map from the class. This is Definition 14.6's B^⊥.
Equations
Instances For
Right orthogonality is invariant under isomorphism of the target.
A torsion pair's free class is the right orthogonal of its torsion
class — so the pair carried by NoetherianTorsionSubcategory really is
(B, B^⊥) in Definition 14.6's sense. The forward inclusion is the
hom_eq_zero axiom; the reverse is free_of_orthogonal, the dual
characterisation added for the #86 review's finding F1.
Constructing the zero-charge torsion pair #
The constructive datum needed to make the zero-charge class a torsion class: every heart object has a zero-charge subobject with right-orthogonal quotient. This is the exact output of the maximal-subobject argument in the proof of Proposition 14.16.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Zero-charge decompositions assemble into the torsion pair
(A⁰, (A⁰)⊥) on the heart.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Zero charge as a Serre class in the full heart #
The zero-charge property transported from ambient objects to objects of the abelian full heart.
Equations
Instances For
Zero-charge heart objects form a Serre class: they are closed under subobjects, quotients, and extensions.
Nonvacuity #
The zero subcategory is noetherian torsion for every t-structure: the
torsion pair is ({0}, A) with the inverse-rotated contractible triangle as
decomposition, and a chain of zero subobjects has every step an isomorphism
already.
Maps between zero objects are isomorphisms.
The degenerate torsion pair with the zero objects as torsion class and the whole heart torsion-free.
Equations
- One or more equations did not get rendered due to their size.
Instances For
NoetherianTorsionSubcategory is nonvacuous for every t-structure:
the zero subcategory qualifies.
Equations
Instances For
Inheritance #
Chain termination passes to sub-properties: a chain in B' with
B' ≤ B is a chain in B. Recorded because the intended instantiation is
A⁰ ⊆ a larger torsion class, as in the proof of Proposition 14.16.
From the relative chain condition to noetherian heart objects #
For composable monomorphisms X ⟶ Y ⟶ Z, the canonical sequence
coker(X ⟶ Y) ⟶ coker(X ⟶ Z) ⟶ coker(Y ⟶ Z) extracted from the
kernel--cokernel sequence of a composition.
Equations
Instances For
The canonical cokernel-of-a-composite sequence is short exact when the second map is a monomorphism.
The middle three terms
ker g ⟶ coker f ⟶ coker (f ≫ g) of the kernel--cokernel sequence.
Equations
Instances For
The middle kernel--cokernel sequence is short exact when f ≫ g is
monic and g is epic. This is the 3×3 fragment used when a
zero-charge subobject of an extension maps monomorphically to its right-hand
term.
The first three terms
ker f ⟶ ker (f ≫ g) ⟶ ker g of the kernel--cokernel sequence.
Equations
Instances For
If f is epic, the first three kernels in the composition sequence form
a short exact sequence.
Saturating a semistable object by a zero-charge quotient preserves semistability provided the saturated middle term receives no maps from zero-charge objects.
For a test subobject X ⟶ E, pull it back to the semistable subobject
F ⟶ E. The quotient of the pullback inside X embeds into the
zero-charge quotient V, so it has zero charge. Consequently the two
charges in the semistability comparison for E agree with those in the
corresponding comparison for F.
A quotient of a semistable heart object by a zero-charge subobject is semistable.
For a test subobject X ⟶ B of the quotient, pull it back along
E ⟶ B. The pullback is the kernel of the composite E ⟶ B ⟶ Y.
The three resulting short exact sequences show that the pullback has the
same charge as X; semistability of E therefore gives precisely the
required comparison for B.
A monomorphism in the abelian full heart gives a heart monomorphism in
the ambient triangle formulation used by SubobjectChain.
A heart monomorphism between objects of the full heart is a monomorphism in that abelian category.
If the torsion class of a noetherian torsion subcategory is the zero-charge class of a weak stability function, then every zero-charge object is noetherian in the ordinary abelian-heart sense.
This is the bridge from Definition 14.6's relative chain formulation to the well-founded subobject order used to choose maximal zero-charge subobjects in the proof of Proposition 14.16. Closure of zero charge under heart subobjects supplies the hypothesis that a general subobject chain lies in the torsion class.
If zero-charge subobject chains terminate in a fixed heart object, then that object has a maximal zero-charge subobject and the corresponding quotient is right-orthogonal.
The right-orthogonality proof takes the image of a hypothetical map into the quotient and pulls it back to a larger zero-charge subobject.
A zero-charge decomposition lifts across a short exact sequence whose kernel has zero charge. Concretely, the zero-charge subobject of the quotient is pulled back to the middle term; its pullback is again zero-charge because it is an extension of the old kernel by that subobject.
This is the abelian pullback step used after the envelope reduction in the proof of Proposition 14.16.
If zero-charge subobject chains terminate in every heart object, then every object has a maximal zero-charge subobject and the corresponding quotient is right-orthogonal. Thus the relative chain condition constructs the zero-charge torsion pair, rather than merely verifying noetherianity after the pair has been supplied.