The subobject correspondence for a quotient, without a charge #
For a subobject M ≤ S of an object E of an abelian category, the subobject of E/M cut out
by S pulls back to S again. This is the classical correspondence between subobjects of
E/M and subobjects of E containing M — one half of it, in the form the
Harder--Narasimhan truncation consumes.
Why this file exists #
Abelian/Stability/Uniqueness/SubobjectLattice.lean already has
this statement, as AbelianHNFiltration.pullback_imageSubobject_eq. Its proof, however, runs
through a central charge: it shows the offending cokernel has charge 0 and concludes it
vanishes, by semiClosedUpperHalfPlane_ne_zero — a nonzero object has nonzero charge.
That implication is exactly what weak stability drops, and it fails on exactly the object the
surface case of Bridgeland's Lemma 6.2 is about: a skyscraper on a surface is nonzero with
charge 0. So the charge proof cannot be reused for the weak Harder--Narasimhan theory, and
the truncation tailAt that depends on it does not port — which is what currently blocks the
weak torsion pair, and with it the tilt.
The statement, though, has nothing to do with stability. It is true in any abelian category. This file proves it that way, so the weak lane can use it.
Method: pseudoelements #
The proof is a diagram chase, carried out with CategoryTheory.Abelian.Pseudoelement. This is
the first use of pseudoelements in this repository, which is a deliberate choice: the
alternative is an explicit five-lemma argument on the two short exact sequences
0 → M → S → S/M → 0 and 0 → M → T → T/M → 0, and the chase is both shorter and closer to
the textbook proof.
Pseudoelements are not elements, and two of their failures matter here.
pseudo_pullback's witness is not unique. Mathlib says so and shipsCounterexamples/Pseudoelement.lean; Borceux claims uniqueness and is wrong.- There is no subtraction.
sub_of_eq_imageis the only sanctioned "difference": fromf x = f yit produceszwithf z = 0such thatg z = g xfor everygkillingy.
Nothing below reaches outside eq_zero_iff, pseudo_surjective_of_epi,
pseudo_exact_of_exact and sub_of_eq_image. A chase that needs more than those is probably
unsound.
Relationship to the existing lemma #
The signature of AbelianHNFiltration.pullback_imageSubobject_eq is deliberately left alone —
it takes a StabilityFunction argument, and Uniqueness/Tail.lean calls it that way. Dropping
that argument is a rename across the strict development. This file supplies the charge-free
statement under its own name; wiring the existing lemma to delegate is a separate edit.
If a subobject maps trivially to the quotient by another subobject, it is contained in that subobject.
Stated here so this file depends on Mathlib alone; the identical statement in
Uniqueness/SubobjectLattice.lean is charge-free too, but lives under StabilityCondition,
which a CategoryTheory leaf must not import.
The image of S in E/M pulls back to something containing S.
This half is formal — it is the unit of the exists ⊣ pullback adjunction, here written out
through the pullback square — and the existing charge-based proof already had it charge-free.
The subobject correspondence, charge-free.
For M ≤ S, pulling the image of S in E/M back along the quotient map recovers S.
The containment S ≤ pullback (image …) is formal. The reverse is the chase: a pseudoelement
of the pullback agrees with one of S after applying the quotient map, so their sub_of_eq_image
difference dies in E/M, hence comes from M, hence from S — and S's own cokernel kills
it. M ≤ S is used exactly once, at that last step, and it is the only place it is needed.
The pulled-back sequence, and the third isomorphism #
0 → M → (pullback p).obj B → B → 0 is exact for every subobject B of E/M. From it the
comparison of successive quotients follows, which is the second half of what the
Harder--Narasimhan truncation needs.
Every pullback of a subobject of E/M contains M: the composite M → E → E/M is zero,
so it lifts through the pullback.
The restricted quotient map out of a pullback is epi.
The kernel inclusion followed by the restricted quotient map is zero.
0 → M → (pullback p).obj B → B → 0 is exact.
Pulling back is natural in the subobject: the inclusion of pullbacks commutes with the restricted quotient maps.
Successive quotients are unchanged by pulling back, charge-free.
The comparison map is epi because the restricted quotient map is; it is mono by the same chase
as pullback_imageSubobject_eq, with shortExact_ofLE_pullbackπ supplying the preimage in M
and M ≤ (pullback p).obj B₁ absorbing it.
Equations
- One or more equations did not get rendered due to their size.