Documentation

DerivedAlgGeo.CategoryTheory.Abelian.Stability.Weak.SlopeOrder

Transporting weak HN filtrations across the same slope order #

Two weak slope data may use different numerical normalizations while inducing the same order on objects. Their semistable objects and HN filtrations are then the same. This file records that fact without requiring equality of the underlying rank and degree homomorphisms.

The motivating example is a polarized surface: the leading two Hilbert coefficients differ from numerical rank and divisor degree by a positive scaling and an affine rank term. That changes the displayed finite slope but not its order, and keeps rank-zero slope equal to ⊤.

source
structure CategoryTheory.Triangulated.WeakSlopeData.SameSlopeOrder {A : Type u} [Category.{v, u} A] [Abelian A] (D E : WeakSlopeData A) :
Prop

Two weak slope data define the same preorder on slopes of objects.

Instances For
    source
    theorem CategoryTheory.Triangulated.WeakSlopeData.SameSlopeOrder.lt_iff {A : Type u} [Category.{v, u} A] [Abelian A] {D E : WeakSlopeData A} (h : D.SameSlopeOrder E) (X Y : A) :
    D.topSlope X < D.topSlope Y ↔ E.topSlope X < E.topSlope Y

    Strict slope comparisons agree as well.

    source
    theorem CategoryTheory.Triangulated.WeakSlopeData.SameSlopeOrder.isSemistable_iff {A : Type u} [Category.{v, u} A] [Abelian A] {D E : WeakSlopeData A} (h : D.SameSlopeOrder E) (X : A) :
    D.toWeakStabilityFunction.IsSemistable X ↔ E.toWeakStabilityFunction.IsSemistable X

    The two weak slope data have exactly the same semistable objects.

    source
    noncomputable def CategoryTheory.Triangulated.AbelianWeakHNFiltration.changeSlopeOrder {A : Type u} [Category.{v, u} A] [Abelian A] {D E : WeakSlopeData A} {X : A} (F : AbelianWeakHNFiltration D.toWeakStabilityFunction X) (h : D.SameSlopeOrder E) :
    AbelianWeakHNFiltration E.toWeakStabilityFunction X

    Reinterpret an HN filtration using weak slope data with the same slope order. The subobject chain is unchanged; only its intrinsic slope labels are recomputed.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      theorem CategoryTheory.Triangulated.WeakSlopeData.SameSlopeOrder.hasHNProperty {A : Type u} [Category.{v, u} A] [Abelian A] {D E : WeakSlopeData A} (h : D.SameSlopeOrder E) (hD : D.toWeakStabilityFunction.HasHNProperty) :
      E.toWeakStabilityFunction.HasHNProperty

      The HN property depends only on the order induced by the honest slope.