The extremal slopes of a weak HN filtration

This is Uniqueness/Extrema.lean and PhaseMonotone.lean for the slope-indexed weak filtration of WeakHarderNarasimhan.lean.

Why the port is mechanical, recorded because it was the question this work turned on. The strict development never performs arithmetic on phases. It compares them, and nothing else: across Extrema.lean, PhaseMonotone.lean, Uniqueness/Tail.lean and Uniqueness/Destabilizing.lean there is not one linarith, no subtraction, no Real.pi, no arg. Every step is le_antisymm, le_of_not_gt, lt_of_le_of_lt or StrictAnti.antitone, all of which hold over WithTop ℝ exactly as over ℝ. The one genuinely analytic input is Hom-vanishing for semistable objects of decreasing value, and its weak counterpart hom_eq_zero_of_semistable_slope_gt is proved in WeakSlopeGeometry.lean from the slope see-saw.

The subobject-lattice primitives are shared rather than duplicated: they are already charge-free, so AbelianHNFiltration.le_of_ofLE_comp_cokernel_zero, StabilityFunction.subobjectCokernelBotIso and StabilityFunction.subobject_isZero_iff_eq_bot are used here directly. The first of those sits in the strict filtration's namespace even though it mentions no charge; moving it is a rename across the strict development and is deliberately not done here.

Contents

• le_chain_of_semistable_μ_gt, eq_bot_of_semistable_μ_gt_μPlus — a weak-semistable subobject of large slope is trapped in the filtration.
• chain_one_isSemistable, μ_chain_one, chain_one_ne_bot — the first chain step is the maximal destabilizing subobject.
• μPlus_eq, μMinus_eq — the extrema are intrinsic, so the cutoff classes of WeakCutoff.lean are well defined.
• μPlus_le_of_mono, μMinus_le_of_epi — the monotonicity that traps the image of a map between the two cutoff classes.

theorem CategoryTheory.Triangulated.AbelianWeakHNFiltration.hom_eq_zero_to_factor {A : Type u} [Category.{v, u} A] [Abelian A] {W : WeakStabilityFunctionOn (abelianDatum A)} {E B : A} (F : AbelianWeakHNFiltration W E) (hB : W.IsSemistable B) (j : Fin F.n) (hslope : F.μ j < W.slope B) (f : B ⟶ F.factor j) : f = 0

A weak-semistable object of slope above an HN factor has no morphisms to that factor.

theorem CategoryTheory.Triangulated.AbelianWeakHNFiltration.le_chain_of_semistable_μ_gt {A : Type u} [Category.{v, u} A] [Abelian A] {W : WeakStabilityFunctionOn (abelianDatum A)} {E : A} (F : AbelianWeakHNFiltration W E) {B : Subobject E} (hB : W.IsSemistable (Subobject.underlying.obj B)) {k : ℕ} (hk : k ≤ F.n) (hslope : ∀ (j : Fin F.n), k ≤ ↑j → F.μ j < W.slope (Subobject.underlying.obj B)) : B ≤ F.chain ⟨k, ⋯⟩

A weak-semistable subobject whose slope is above every factor from index k onward lies in the k-th term of an HN filtration.

theorem CategoryTheory.Triangulated.AbelianWeakHNFiltration.eq_bot_of_semistable_μ_gt_μPlus {A : Type u} [Category.{v, u} A] [Abelian A] {W : WeakStabilityFunctionOn (abelianDatum A)} {E : A} (F : AbelianWeakHNFiltration W E) {B : Subobject E} (hB : W.IsSemistable (Subobject.underlying.obj B)) (hslope : F.μPlus < W.slope (Subobject.underlying.obj B)) : B = ⊥

A weak-semistable subobject whose slope is above the highest HN slope is zero.

theorem CategoryTheory.Triangulated.AbelianWeakHNFiltration.chain_one_ne_bot {A : Type u} [Category.{v, u} A] [Abelian A] {W : WeakStabilityFunctionOn (abelianDatum A)} {E : A} (F : AbelianWeakHNFiltration W E) : F.chain ⟨1, ⋯⟩ ≠ ⊥

The first nonzero term in an HN filtration is not bottom.

theorem CategoryTheory.Triangulated.AbelianWeakHNFiltration.μ_chain_one {A : Type u} [Category.{v, u} A] [Abelian A] {W : WeakStabilityFunctionOn (abelianDatum A)} {E : A} (F : AbelianWeakHNFiltration W E) : W.slope (Subobject.underlying.obj (F.chain ⟨1, ⋯⟩)) = F.μPlus

The slope of the first nonzero term is the highest HN slope.

theorem CategoryTheory.Triangulated.AbelianWeakHNFiltration.chain_one_isSemistable {A : Type u} [Category.{v, u} A] [Abelian A] {W : WeakStabilityFunctionOn (abelianDatum A)} {E : A} (F : AbelianWeakHNFiltration W E) : W.IsSemistable (Subobject.underlying.obj (F.chain ⟨1, ⋯⟩))

The first nonzero term in an HN filtration is weak-semistable.

theorem CategoryTheory.Triangulated.AbelianWeakHNFiltration.μPlus_eq {A : Type u} [Category.{v, u} A] [Abelian A] {W : WeakStabilityFunctionOn (abelianDatum A)} {E : A} (F G : AbelianWeakHNFiltration W E) : F.μPlus = G.μPlus

The highest slope is intrinsic: any two weak HN filtrations of the same object have the same first slope.

theorem CategoryTheory.Triangulated.AbelianWeakHNFiltration.chain_one_eq {A : Type u} [Category.{v, u} A] [Abelian A] {W : WeakStabilityFunctionOn (abelianDatum A)} {E : A} (F G : AbelianWeakHNFiltration W E) : F.chain ⟨1, ⋯⟩ = G.chain ⟨1, ⋯⟩

The first nonzero term is intrinsic: any two weak HN filtrations of the same object have the same maximally destabilizing subobject.

theorem CategoryTheory.Triangulated.AbelianWeakHNFiltration.semistable_μ_le_μPlus {A : Type u} [Category.{v, u} A] [Abelian A] {W : WeakStabilityFunctionOn (abelianDatum A)} {E : A} (F : AbelianWeakHNFiltration W E) {B : Subobject E} (hB : W.IsSemistable (Subobject.underlying.obj B)) : W.slope (Subobject.underlying.obj B) ≤ F.μPlus

No nonzero weak-semistable subobject has slope above the first HN slope.

theorem CategoryTheory.Triangulated.AbelianWeakHNFiltration.hom_eq_zero_to_semistable_of_μ_lt_μMinus {A : Type u} [Category.{v, u} A] [Abelian A] {W : WeakStabilityFunctionOn (abelianDatum A)} {E B : A} (F : AbelianWeakHNFiltration W E) (hB : W.IsSemistable B) (hslope : W.slope B < F.μMinus) (f : E ⟶ B) : f = 0

Every morphism to a weak-semistable object of slope below the lowest HN slope is zero. Induction along the chain: each step factors through a successive quotient, which is semistable of slope above the target.

theorem CategoryTheory.Triangulated.AbelianWeakHNFiltration.exists_epi_to_semistable_μ_μMinus {A : Type u} [Category.{v, u} A] [Abelian A] {W : WeakStabilityFunctionOn (abelianDatum A)} {E : A} (F : AbelianWeakHNFiltration W E) : ∃ (Q : A) (q : E ⟶ Q), Epi q ∧ W.IsSemistable Q ∧ W.slope Q = F.μMinus

The last HN factor, presented as a weak-semistable quotient of the filtered object at the lowest HN slope.

theorem CategoryTheory.Triangulated.AbelianWeakHNFiltration.μMinus_eq {A : Type u} [Category.{v, u} A] [Abelian A] {W : WeakStabilityFunctionOn (abelianDatum A)} {E : A} (F G : AbelianWeakHNFiltration W E) : F.μMinus = G.μMinus

The lowest slope is intrinsic: any two weak HN filtrations of the same object have the same last slope.

theorem CategoryTheory.Triangulated.AbelianWeakHNFiltration.μPlus_le_of_mono {A : Type u} [Category.{v, u} A] [Abelian A] {W : WeakStabilityFunctionOn (abelianDatum A)} {X Y : A} (F : AbelianWeakHNFiltration W X) (G : AbelianWeakHNFiltration W Y) (i : X ⟶ Y) [Mono i] : F.μPlus ≤ G.μPlus

μPlus is monotone along monomorphisms. The maximal destabilizing subobject of the source maps to a weak-semistable subobject of the target of the same slope, and no weak-semistable subobject exceeds μPlus.

theorem CategoryTheory.Triangulated.AbelianWeakHNFiltration.μMinus_le_of_epi {A : Type u} [Category.{v, u} A] [Abelian A] {W : WeakStabilityFunctionOn (abelianDatum A)} {X Y : A} (F : AbelianWeakHNFiltration W X) (G : AbelianWeakHNFiltration W Y) (p : X ⟶ Y) [Epi p] : F.μMinus ≤ G.μMinus

μMinus is monotone along epimorphisms. A strict drop would make the composite onto the last HN factor of the target a nonzero epimorphism that hom_eq_zero_to_semistable_of_μ_lt_μMinus forces to vanish.