Truncating a weak HN filtration above an index #

WeakTruncation.lean ported restrict, the truncation below an index, and recorded that tailAt — the truncation above it, pushed down to the quotient — did not port, because its two supporting lemmas were proved from semiClosedUpperHalfPlane_ne_zero.

CategoryTheory/SubobjectCorrespondence.lean removed that obstruction by proving both without any charge. This file is the port those lemmas unblock.

What changed, and what did not #

The strict tailAt (Uniqueness/Tail.lean:35) reads four charge-dependent facts. Two of them are replaced here by their charge-free counterparts:

strict	here
`pullback_imageSubobject_eq Z`	`Abelian.pullback_imageSubobject_eq`
`cokernelPullbackIso Z`	`Abelian.cokernelPullbackIso`
`phase_cokernel_pullback_eq Z`	`slope_cokernel_pullback_eq`, below
`Z.phase_cokernel_ofLE_congr`	`W.slope_cokernel_ofLE_congr` (#789)

slope_cokernel_pullback_eq is shorter than the phase version it replaces. The strict proof computes both charges and cancels with linear_combination; here the correspondence already supplies an isomorphism of the two quotients, so the slopes agree by slope_eq_of_iso and additivity is never mentioned.

Everything else — the chain, its strictness, its endpoints, the index arithmetic — is the strict proof with phase renamed to μ, and is order-generic exactly as the rest of this development turned out to be.

source

theorem CategoryTheory.Triangulated.WeakStabilityFunctionOn.slope_cokernel_pullback_eq {A : Type u} [Category.{v, u} A] [Abelian A] (W : WeakStabilityFunctionOn (abelianDatum A)) {E : A} (M : Subobject E) {B₁ B₂ : Subobject (Limits.cokernel M.arrow)} (h : B₁ ≤ B₂) :

W.slope (Limits.cokernel (((Subobject.pullback (Limits.cokernel.π M.arrow)).obj B₁).ofLE ((Subobject.pullback (Limits.cokernel.π M.arrow)).obj B₂) ⋯)) = W.slope (Limits.cokernel (B₁.ofLE B₂ h))

Consecutive pulled-back quotient subobjects have the slope of the corresponding quotient factor. The correspondence gives an isomorphism of the two quotients outright, so this is slope_eq_of_iso and nothing else.

source

theorem CategoryTheory.Triangulated.WeakStabilityFunctionOn.isSemistable_cokernel_pullback_iff {A : Type u} [Category.{v, u} A] [Abelian A] (W : WeakStabilityFunctionOn (abelianDatum A)) {E : A} (M : Subobject E) {B₁ B₂ : Subobject (Limits.cokernel M.arrow)} (h : B₁ ≤ B₂) :

W.IsSemistable (Limits.cokernel (((Subobject.pullback (Limits.cokernel.π M.arrow)).obj B₁).ofLE ((Subobject.pullback (Limits.cokernel.π M.arrow)).obj B₂) ⋯)) ↔ W.IsSemistable (Limits.cokernel (B₁.ofLE B₂ h))

Weak semistability likewise transfers across the correspondence.

source

noncomputable def CategoryTheory.Triangulated.AbelianWeakHNFiltration.tailAt {A : Type u} [Category.{v, u} A] [Abelian A] {W : WeakStabilityFunctionOn (abelianDatum A)} {E : A} (F : AbelianWeakHNFiltration W E) (k : ℕ) (hk : k < F.n) :

AbelianWeakHNFiltration W (Limits.cokernel (F.chain ⟨k, ⋯⟩).arrow)

Cut a weak HN filtration above an index: push the chain from index k onward down to the quotient by the k-th term. The factors are the original factors k, …, n-1, so the slopes are the original slopes from k on.

The chain index is written k + j rather than j + k so that the successor step is definitionally (k + j) + 1, which is what factor_slope and factor_semistable of the original filtration are stated at.

Equations