Transporting Harder–Narasimhan filtrations #

WeakSlopeTransport.lean moves the slope data along an equivalence of abelian categories. This file moves the filtrations, and therefore HasHNProperty itself, which is the point of the exercise: an existence theorem proved on one category becomes an existence theorem on any equivalent one.

Why this is not automatic #

A filtration is not a homomorphism. It is a strictly increasing chain of subobjects from bottom to top, together with the slope and the semistability of the cokernel of each step. So three things have to move, and each needs its own input:

the chain, by Subobject.mapEquivalence — an order isomorphism, so strictness and the two endpoints survive, which a merely monotone map would not give;
the factors, by Subobject.cokernelOfLEMapFunctorIso — the factors are cokernels of chain steps, not subobjects;
the slopes and semistability of those factors, by congr_topSlope_functor and congr_isSemistable.

The last step #

Transporting a filtration of Z produces a filtration of e.functor.obj Z, but HasHNProperty on the target category asks for a filtration of an arbitrary object E. Taking Z to be e.inverse.obj E leaves a counit isomorphism to cross, so a filtration must also move along an isomorphism of the object it filters. AbelianWeakHNFiltration.ofIso in WeakTruncation.lean already does exactly that, and is reused rather than rebuilt.

source

def CategoryTheory.Triangulated.WeakSlopeData.congrFiltration {A : Type u₁} [Category.{v₁, u₁} A] [Abelian A] {B : Type u₂} [Category.{v₂, u₂} B] [Abelian B] (D : WeakSlopeData A) (e : A ≌ B) [e.functor.PreservesMonomorphisms] [e.inverse.PreservesMonomorphisms] {Z : A} (G : AbelianWeakHNFiltration D.toWeakStabilityFunction Z) :

AbelianWeakHNFiltration (D.congr e).toWeakStabilityFunction (e.functor.obj Z)

A filtration transported along an equivalence.

The chain is the image of the chain under the order isomorphism on subobject lattices; the slope vector is unchanged; the factors are identified with the images of the original factors, which is what Subobject.cokernelOfLEMapFunctorIso supplies.

Equations