Documentation

DerivedAlgGeo.AlgebraicGeometry.Stability.Slope.HarderNarasimhan.Consequences

What the Harder–Narasimhan property unlocks on Coh X #

hasHNProperty is the hypothesis the abstract theory takes at every one of its use sites. With it proved, those sites become theorems about coherent sheaves, and this file collects them. Nothing here re-proves anything: each declaration applies an existing result from Abelian/Stability/Weak/HarderNarasimhan.lean or Abelian/Stability/Weak/Splitting.lean to the filtration Existence.lean builds.

Everything here is about the μ-slope. The Gieseker order is not mentioned and not imported; the one-step filtration of a Gieseker-semistable sheaf lives with the other comparison statements, in Stability/Comparison.lean.

The chosen filtration #

The HN filtration is not unique as a term, only as a mathematical object, and the abstract theory states existence as Nonempty. hnFiltration picks one with choice. Everything downstream that mentions μPlus or μMinus is therefore about that choice, which is why the genuinely mathematical statement below, filtration_muPlus_ne_top_of_isPure, is proved for an arbitrary filtration first and only then specialized.

The torsion/torsion-free splitting #

For a cutoff μ₀, exists_shortExact_hnTors_hnFree cuts the filtration at its crossing index and produces a short exact sequence whose subsheaf has all slopes above μ₀ and whose quotient has all slopes at or below it. That is the input a tilted heart is built from; constructing the tilt belongs to the abstract tilting lane, not here.

source
noncomputable def AlgebraicGeometry.Stability.Gieseker.PolarizedVarietyData.hnFiltration {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) {F : Coh X} (hF : ¬CategoryTheory.Limits.IsZero F) :
CategoryTheory.Triangulated.AbelianWeakHNFiltration (P.weakSlopeData h).toWeakStabilityFunction F

The Harder–Narasimhan filtration of a nonzero coherent sheaf. A choice of one of the filtrations exists_filtration produces.

Equations
Instances For
    source
    noncomputable def AlgebraicGeometry.Stability.Gieseker.PolarizedVarietyData.muPlus {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) {F : Coh X} (hF : ¬CategoryTheory.Limits.IsZero F) :
    WithTop ℝ

    The largest Harder–Narasimhan slope of a nonzero coherent sheaf.

    Equations
    Instances For
      source
      noncomputable def AlgebraicGeometry.Stability.Gieseker.PolarizedVarietyData.muMinus {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) {F : Coh X} (hF : ¬CategoryTheory.Limits.IsZero F) :
      WithTop ℝ

      The smallest Harder–Narasimhan slope of a nonzero coherent sheaf.

      Equations
      Instances For
        source
        theorem AlgebraicGeometry.Stability.Gieseker.PolarizedVarietyData.muMinus_le_muPlus {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) {F : Coh X} (hF : ¬CategoryTheory.Limits.IsZero F) :
        muMinus h I hF ≤ muPlus h I hF

        The smallest Harder–Narasimhan slope does not exceed the largest.

        source
        theorem AlgebraicGeometry.Stability.Gieseker.PolarizedVarietyData.muPlus_eq_topSlope_chain_one {k : Type u} [Field k] {X : Scheme} [X.Over (Spec (CommRingCat.of k))] [IsVariety k X] {P : PolarizedVarietyData k X} (h : MuPositivityData P) {Y : Coh X} (G : CategoryTheory.Triangulated.AbelianWeakHNFiltration (P.weakSlopeData h).toWeakStabilityFunction Y) :
        G.μPlus = (P.weakSlopeData h).topSlope (CategoryTheory.Subobject.underlying.obj (G.chain ⟨0, ⋯⟩.succ))

        The first chain step of a filtration realizes μPlus as the slope of a subobject.

        This is firstFactorIso read as a statement about μPlus: the opening factor runs out of the bottom subobject, so it is the first chain step.

        source
        theorem AlgebraicGeometry.Stability.Gieseker.PolarizedVarietyData.not_isZero_chain_one {k : Type u} [Field k] {X : Scheme} [X.Over (Spec (CommRingCat.of k))] [IsVariety k X] {P : PolarizedVarietyData k X} (h : MuPositivityData P) {Y : Coh X} (G : CategoryTheory.Triangulated.AbelianWeakHNFiltration (P.weakSlopeData h).toWeakStabilityFunction Y) :
        ¬CategoryTheory.Limits.IsZero (CategoryTheory.Subobject.underlying.obj (G.chain ⟨0, ⋯⟩.succ))

        The first chain step of a filtration is a nonzero subobject.

        source
        theorem AlgebraicGeometry.Stability.Gieseker.PolarizedVarietyData.filtration_muPlus_ne_top_of_isPure {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} (hF : P.IsPure F) (G : CategoryTheory.Triangulated.AbelianWeakHNFiltration (P.weakSlopeData h).toWeakStabilityFunction F) :
        G.μPlus ≠ ⊤

        For a pure sheaf the largest Harder–Narasimhan slope is finite.

        μPlus is the slope of the first chain step, which is a nonzero subobject; purity gives it positive multiplicity, and only multiplicity zero produces ⊤.

        source
        theorem AlgebraicGeometry.Stability.Gieseker.PolarizedVarietyData.muPlus_ne_top_of_isPure {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) {F : Coh X} (hF : P.IsPure F) :
        muPlus h I ⋯ ≠ ⊤

        μPlus of a pure coherent sheaf is finite.

        source
        theorem AlgebraicGeometry.Stability.Gieseker.PolarizedVarietyData.exists_subobject_hnTors_cokernel_hnFree {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) (μ₀ : WithTop ℝ) (F : Coh X) :
        ∃ (T : CategoryTheory.Subobject F), CategoryTheory.Subobject.underlying.obj T ∈ (P.weakSlopeData h).toWeakStabilityFunction.hnTors μ₀ ∧ CategoryTheory.Limits.cokernel T.arrow ∈ (P.weakSlopeData h).toWeakStabilityFunction.hnFree μ₀

        The Harder–Narasimhan torsion subsheaf at a cutoff. Every coherent sheaf has a subsheaf whose Harder–Narasimhan slopes all exceed μ₀ and whose quotient's all fail to.

        source
        theorem AlgebraicGeometry.Stability.Gieseker.PolarizedVarietyData.exists_shortExact_hnTors_hnFree {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) (μ₀ : WithTop ℝ) (F : Coh X) :
        ∃ (T : Coh X) (Q : Coh X) (i : T ⟶ F) (p : F ⟶ Q) (w : CategoryTheory.CategoryStruct.comp i p = 0), T ∈ (P.weakSlopeData h).toWeakStabilityFunction.hnTors μ₀ ∧ Q ∈ (P.weakSlopeData h).toWeakStabilityFunction.hnFree μ₀ ∧ { X₁ := T, X₂ := F, X₃ := Q, f := i, g := p, zero := w }.ShortExact

        The torsion/torsion-free splitting as a short exact sequence. This is the input a tilted heart is built from; the tilt itself belongs to the abstract tilting lane.