Documentation

DerivedAlgGeo.CategoryTheory.Abelian.Stability.Weak.Cutoff

The two classes at a weak slope cutoff #

Cutoff.lean cuts two classes out of an abelian category by a phase β : ℝ, which is available for a strict stability function. This file cuts them by a slope μ₀ : WithTop ℝ for a weak one:

T μ₀ = {E | every weak HN slope of E exceeds μ₀}
F μ₀ = {E | every weak HN slope of E is at most μ₀}

Why the cutoff is WithTop ℝ, and what that buys #

Because slopes are. A rank-zero object has charge on the real boundary, so slope ⊤, so μMinus = ⊤ > μ₀ for every finite μ₀, so it lies in T μ₀ — mem_hnTors_of_slope_eq_top below. That is the classical convention: torsion sheaves are in the torsion class at every finite slope cutoff.

This is the correct replacement for SlopeCutoff.lean's mem_hnTors_of_rank_zero, and the replacement is not cosmetic. The strict lemma reaches its conclusion through phase_eq_one_of_rank_zero, which needs degree_pos_of_rank_zero — the curve hypothesis, false on a surface, where a skyscraper has c₁ = 0 and so degree 0. With charge exactly 0 there is no phase at all (arg 0 = 0 is not a phase), and no phase comparison can place the object. The slope ⊤ places it, with no positivity hypothesis whatever.

The cutoff μ₀ = ⊤ is permitted and degenerate in the expected direction: no slope exceeds ⊤, so T ⊤ contains only the zero object while F ⊤ is everything. Nothing below excludes it.

What is here and what is next #

hom_eq_zero_of_mem_hnTors_of_mem_hnFree is the Hom-vanishing half of a torsion pair. The splitting half is WeakSplitting.lean, and with both present the two classes are a torsion pair — assembled as WeakStabilityFunctionOn.hnTorsionPair in Weak/Tilting/TorsionPair/WeakStabilityFunction.lean. This file still states only the Hom-vanishing, which is all it needs.

source
def CategoryTheory.Triangulated.WeakStabilityFunctionOn.hnTors {A : Type u} [Category.{v, u} A] [Abelian A] (W : WeakStabilityFunctionOn (abelianDatum A)) (μ₀ : WithTop ℝ) :
Set A

The torsion class at a weak slope cutoff: the zero object, and the objects whose weak HN slopes all exceed μ₀.

Equations
Instances For
    source
    def CategoryTheory.Triangulated.WeakStabilityFunctionOn.hnFree {A : Type u} [Category.{v, u} A] [Abelian A] (W : WeakStabilityFunctionOn (abelianDatum A)) (μ₀ : WithTop ℝ) :
    Set A

    The torsion-free class at a weak slope cutoff: the zero object, and the objects whose weak HN slopes are all at most μ₀.

    Equations
    Instances For
      source
      theorem CategoryTheory.Triangulated.WeakStabilityFunctionOn.isZero_mem_hnTors {A : Type u} [Category.{v, u} A] [Abelian A] {W : WeakStabilityFunctionOn (abelianDatum A)} {μ₀ : WithTop ℝ} {E : A} (hE : Limits.IsZero E) :
      E ∈ W.hnTors μ₀
      source
      theorem CategoryTheory.Triangulated.WeakStabilityFunctionOn.isZero_mem_hnFree {A : Type u} [Category.{v, u} A] [Abelian A] {W : WeakStabilityFunctionOn (abelianDatum A)} {μ₀ : WithTop ℝ} {E : A} (hE : Limits.IsZero E) :
      E ∈ W.hnFree μ₀
      source
      theorem CategoryTheory.Triangulated.WeakStabilityFunctionOn.mem_hnTors_iff_forall {A : Type u} [Category.{v, u} A] [Abelian A] {W : WeakStabilityFunctionOn (abelianDatum A)} {μ₀ : WithTop ℝ} (hHN : W.HasHNProperty) {E : A} (hE : ¬Limits.IsZero E) :
      E ∈ W.hnTors μ₀ ↔ ∀ (F : AbelianWeakHNFiltration W E), μ₀ < F.μMinus

      Membership is independent of the filtration chosen, because μ⁻ is.

      The HN property is needed for the reverse direction only: without a filtration to exhibit, the universally quantified condition is vacuous while membership asks for a witness.

      source
      theorem CategoryTheory.Triangulated.WeakStabilityFunctionOn.mem_hnFree_iff_forall {A : Type u} [Category.{v, u} A] [Abelian A] {W : WeakStabilityFunctionOn (abelianDatum A)} {μ₀ : WithTop ℝ} (hHN : W.HasHNProperty) {E : A} (hE : ¬Limits.IsZero E) :
      E ∈ W.hnFree μ₀ ↔ ∀ (F : AbelianWeakHNFiltration W E), F.μPlus ≤ μ₀

      Membership is independent of the filtration chosen, because μ⁺ is.

      source
      theorem CategoryTheory.Triangulated.WeakStabilityFunctionOn.mem_hnTors_of_slope_eq_top {A : Type u} [Category.{v, u} A] [Abelian A] {W : WeakStabilityFunctionOn (abelianDatum A)} {μ₀ : WithTop ℝ} {E : A} (hE : W.IsSemistable E) (hslope : W.slope E = ⊤) (hμ : μ₀ ≠ ⊤) :
      E ∈ W.hnTors μ₀

      A weak-semistable object of slope ⊤ lies in the torsion class at every finite cutoff. This is the skyscraper, and it is the whole reason the cutoff is valued in WithTop ℝ rather than in ℝ.

      source
      theorem CategoryTheory.Triangulated.WeakStabilityFunctionOn.mem_hnTors_of_charge_eq_zero {A : Type u} [Category.{v, u} A] [Abelian A] {W : WeakStabilityFunctionOn (abelianDatum A)} {μ₀ : WithTop ℝ} {E : A} (hE : W.IsSemistable E) (hcharge : W.charge E = 0) (hμ : μ₀ ≠ ⊤) :
      E ∈ W.hnTors μ₀

      A weak-semistable object of charge 0 lies in the torsion class at every finite cutoff. The rank-zero, degree-zero case in charge terms.

      source
      theorem CategoryTheory.Triangulated.WeakStabilityFunctionOn.isZero_of_mem_hnTors_of_mem_hnFree {A : Type u} [Category.{v, u} A] [Abelian A] {W : WeakStabilityFunctionOn (abelianDatum A)} {μ₀ : WithTop ℝ} {E : A} (hT : E ∈ W.hnTors μ₀) (hF : E ∈ W.hnFree μ₀) :
      Limits.IsZero E

      The two classes meet only in zero. An object in both would have μ₀ < μ⁻ ≤ μ⁺ ≤ μ₀.

      source
      theorem CategoryTheory.Triangulated.WeakStabilityFunctionOn.hom_eq_zero_of_mem_hnTors_of_semistable {A : Type u} [Category.{v, u} A] [Abelian A] {W : WeakStabilityFunctionOn (abelianDatum A)} {μ₀ : WithTop ℝ} {E B : A} (hE : ¬Limits.IsZero E) (hT : E ∈ W.hnTors μ₀) (hB : W.IsSemistable B) (hslope : W.slope B ≤ μ₀) (f : E ⟶ B) :
      f = 0

      Hom-vanishing, for a weak-semistable target. A map from an object whose weak HN slopes all exceed μ₀ to a weak-semistable object of slope at most μ₀ is zero.

      source
      theorem CategoryTheory.Triangulated.WeakStabilityFunctionOn.hom_eq_zero_of_mem_hnTors_of_mem_hnFree {A : Type u} [Category.{v, u} A] [Abelian A] {W : WeakStabilityFunctionOn (abelianDatum A)} {μ₀ : WithTop ℝ} (hHN : W.HasHNProperty) {E B : A} (hT : E ∈ W.hnTors μ₀) (hFr : B ∈ W.hnFree μ₀) (f : E ⟶ B) :
      f = 0

      Hom-vanishing. A map from an object whose weak HN slopes all exceed μ₀ to an object whose weak HN slopes are all at most μ₀ is zero: its image is a quotient of the source and a subobject of the target, so μ₀ < μ⁻(image) and μ⁺(image) ≤ μ₀, which μMinus_le_μPlus contradicts unless the image is zero.

      The HN property is needed for the image, which is neither of the two given objects.