Documentation

DerivedAlgGeo.CategoryTheory.Abelian.Stability.Weak.SlopeTop

The surface slope, honestly valued #

WeakSlope.lean gives WeakSlopeData a slope degree / rank, and says of it, correctly, that it is junk at rank zero — division by zero returns 0, where the classical slope is +∞. Every statement there carries a positive-rank hypothesis for that reason.

WeakSlopeGeometry.lean gives WeakStabilityFunctionOn a slope valued in WithTop ℝ, which is ⊤ exactly on the real boundary of the closed upper half-plane — in particular at charge 0, the skyscraper.

This file connects them, which is what makes the junk value harmless rather than merely quarantined: topSlope is the honest slope of a WeakSlopeData, and the two agree wherever the ℝ-valued one means anything.

Why this is the last piece of the surface redirect's first stage #

A rank-zero object on a surface is why SlopeData could not be instantiated: a skyscraper has degree = 0 as well, so its charge is 0 and it has no phase. The cutoff classes of WeakCutoff.lean place it at ⊤, in the torsion class at every finite cutoff, with no positivity hypothesis at all. topSlope_of_rank_zero is the statement that WeakSlopeData's own objects land there — so the geometry and the cutoff agree about skyscrapers, rather than each being separately correct about a different notion of slope.

source
noncomputable def CategoryTheory.Triangulated.WeakSlopeData.topSlope {A : Type u} [Category.{v, u} A] [Abelian A] (D : WeakSlopeData A) (E : A) :
WithTop ℝ

The honest slope of a WeakSlopeData, valued in WithTop ℝ.

Defined through the weak stability function rather than by a second if, so that every result about WeakStabilityFunctionOn.slope — the see-saws, slope_le_of_epi, and the cutoff classes — applies to it without transport.

Equations
Instances For
    source
    theorem CategoryTheory.Triangulated.WeakSlopeData.topSlope_eq_chargeSlope {A : Type u} [Category.{v, u} A] [Abelian A] (D : WeakSlopeData A) (E : A) :
    D.topSlope E = chargeSlope (D.toWeakStabilityFunction.charge E)
    source
    theorem CategoryTheory.Triangulated.WeakSlopeData.topSlope_of_rank_pos {A : Type u} [Category.{v, u} A] [Abelian A] (D : WeakSlopeData A) {E : A} (h : 0 < D.rank E) :
    D.topSlope E = ↑(D.slope E)

    At positive rank the two slopes agree, under the coercion ℝ → WithTop ℝ.

    This is the whole of the compatibility: WeakSlope.lean's slope is correct exactly where its positive-rank hypotheses say it is.

    source
    theorem CategoryTheory.Triangulated.WeakSlopeData.topSlope_of_rank_zero {A : Type u} [Category.{v, u} A] [Abelian A] (D : WeakSlopeData A) {E : A} (h : D.rank E = 0) :
    D.topSlope E = ⊤

    At rank zero the honest slope is ⊤ — no positivity hypothesis anywhere.

    This is the skyscraper. WeakSlope.lean's slope returns 0 here, which is the junk value its docstring warns about; topSlope returns the classical +∞ instead, and that is what WeakCutoff.lean's mem_hnTors_of_slope_eq_top reads.

    source
    theorem CategoryTheory.Triangulated.WeakSlopeData.topSlope_eq_of_iso {A : Type u} [Category.{v, u} A] [Abelian A] (D : WeakSlopeData A) {E F : A} (e : E ≅ F) :
    D.topSlope E = D.topSlope F

    The honest slope is an isomorphism invariant.