Documentation

DerivedAlgGeo.AlgebraicGeometry.Stability.Slope.HarderNarasimhan.HeartTransport

The μ-slope and its Harder–Narasimhan property, read on the heart #

The Gieseker lane builds the μ-slope on Coh X and proves the Harder–Narasimhan property there. The abstract stability machinery is written against the heart of a t-structure. This file joins the two, and it is the first time in the tree that a stability-theoretic hypothesis stated for a heart is discharged from geometry.

What makes it possible #

Two things that did not exist before this lane:

Composing them is all that happens here. Nothing is re-proved.

What this does not discharge #

heart_hasHNProperty still takes MuHNInput, exactly as hasHNProperty does. Neither of that structure's two fields has ever been proved for a projective surface: one asks for Coh X to be a Noetherian category, and the other is Grothendieck's boundedness lemma. Carrying the result to the heart does not make either easier, and it must not be read as having discharged them.

The local instances, and why they are local #

HasDerivedCategory records a chosen localization, and the repository's convention is that HasDerivedCategory.standard is a local instance in each consumer and never a global one, so that the choice is literally the same term everywhere. The heart's abelian structure is local for the same reason. Both follow the pattern already used across the derived-category files.

source
@[reducible, inline]
abbrev AlgebraicGeometry.Stability.Gieseker.PolarizedVarietyData.cohHeart {k : Type u} [Field k] {X : Scheme} [X.Over (Spec (CommRingCat.of k))] [IsVariety k X] :
CategoryTheory.ObjectProperty (DerivedCategory (Coh X))

The heart of the canonical t-structure on the derived category of coherent sheaves.

Equations
Instances For
    source
    noncomputable def AlgebraicGeometry.Stability.Gieseker.PolarizedVarietyData.heartWeakSlopeData {k : Type u} [Field k] {X : Scheme} [X.Over (Spec (CommRingCat.of k))] [IsVariety k X] {P : PolarizedVarietyData k X} (h : MuPositivityData P) :
    CategoryTheory.Triangulated.WeakSlopeData cohHeart.FullSubcategory

    The μ-slope, read on the heart.

    Coh X is the heart of the canonical t-structure, and weak slope data transports along that identification.

    Equations
    Instances For
      source
      theorem AlgebraicGeometry.Stability.Gieseker.PolarizedVarietyData.heart_hasHNProperty {k : Type u} [Field k] {X : Scheme} [X.Over (Spec (CommRingCat.of k))] [IsVariety k X] {P : PolarizedVarietyData k X} (h : MuPositivityData P) (I : MuHNInput P h) :
      (heartWeakSlopeData h).toWeakStabilityFunction.HasHNProperty

      The Harder–Narasimhan property on the heart.

      The abstract stability machinery takes this as a hypothesis at every use site and no geometric category had ever supplied it in the form the machinery asks for. MuHNInput is still a hypothesis; see the module docstring on why that matters.

      source
      theorem AlgebraicGeometry.Stability.Gieseker.PolarizedVarietyData.heartWeakSlopeData_rank_functor {k : Type u} [Field k] {X : Scheme} [X.Over (Spec (CommRingCat.of k))] [IsVariety k X] {P : PolarizedVarietyData k X} (h : MuPositivityData P) (F : Coh X) :
      (heartWeakSlopeData h).rank ((DerivedCategory.heartEquivalence (Coh X)).functor.obj F) = P.multiplicity F

      The rank on the heart is the multiplicity of the sheaf it comes from.

      source
      theorem AlgebraicGeometry.Stability.Gieseker.PolarizedVarietyData.heartWeakSlopeData_topSlope_functor {k : Type u} [Field k] {X : Scheme} [X.Over (Spec (CommRingCat.of k))] [IsVariety k X] {P : PolarizedVarietyData k X} (h : MuPositivityData P) (F : Coh X) :
      (heartWeakSlopeData h).topSlope ((DerivedCategory.heartEquivalence (Coh X)).functor.obj F) = (P.weakSlopeData h).topSlope F

      The slope on the heart is the μ-slope of the sheaf it comes from.