Z(β,ω) read against the weak slope cutoff

Mukai.Charge carries a Mukai class map into an abelian category and makes Z(β,ω) a charge on objects. It stops there, deliberately: its own docstring records that MukaiChargeData asserts nothing about rank, slope or torsion, and that bundling those as hypotheses would make the positivity a case split over invented assumptions.

This file supplies the missing connection in the one form that is an identification rather than a discriminant: MukaiWeakSlopeCompat says the Mukai class's rank component is the rank, and its ω-degree is the degree, of a WeakSlopeData on the same category. Both are true on a polarised surface by definition of the Mukai vector, neither mentions torsion or a cutoff, and everything else below is proved.

The identity everything rests on

Mukai.im_expCharge gives Im Z(β,ω)(r, c, s) = ω·c - r·(β·ω). Under the identification that is

Im Z(β,ω)(E) = degree E - rank E · (β·ω)

so the sign of Im Z(β,ω) is exactly the comparison of μ(E) = degree/rank against the cutoff β·ω. That is the Mukai compatibility: Z(β,ω)'s imaginary part and the weak slope cutoff of WeakCutoff.lean are two readings of one inequality.

Why this needs the weak theory and not the strict one

At rank zero the comparison degree/rank is meaningless and the identity reads Im Z = degree, which degree_nonneg_of_rank_zero makes nonnegative and which vanishes exactly on the skyscraper. So Im Z ≥ 0 is the sharp conclusion for the torsion class, not Im Z > 0: the boundary is attained, and rank_eq_zero_of_im_eq_zero_of_mem_hnTors below says it is attained only there.

That is precisely why Z(β,ω) before tilting is a weak stability function and WeakSlope.lean had to exist. A strict StabilityFunction would have to exclude the skyscraper, and on a K3 the skyscrapers are the subject.

What this is not

It is still not Lemma 6.2. This file relates Im Z(β,ω) to the cutoff classes of the untilted heart; Lemma 6.2 is the statement that Z(β,ω) is a stability function on the tilted heart 𝒜(β,ω), which additionally needs hnTilt and the real-part analysis of CentralCharge/Mukai/Positivity.lean for the boundary case. The four cases remain open, and nothing here calls them closed.

theorem CategoryTheory.Triangulated.WeakSlopeData.rank_pos_of_mem_hnFree {A : Type u} [Category.{v, u} A] [Abelian A] (S : WeakSlopeData A) (hHN : S.toWeakStabilityFunction.HasHNProperty) {μ₀ : ℝ} {E : A} (hE : ¬Limits.IsZero E) (h : E ∈ S.toWeakStabilityFunction.hnFree ↑μ₀) : 0 < S.rank E

The torsion-free class at a finite cutoff contains no rank-zero object.

The dual of mem_hnTors_of_rank_zero, and forced by the same fact: a rank-zero object has slope ⊤, which is not below any finite cutoff. So membership in hnFree at a finite cutoff already implies positive rank, and no separate rank hypothesis is needed downstream.

structure CategoryTheory.Triangulated.MukaiWeakSlopeCompat {A : Type u} [Category.{v, u} A] [Abelian A] {V : Type u_1} [AddCommGroup V] [Module ℝ V] (D : MukaiChargeData A V) (S : WeakSlopeData A) (b : V →ₗ[ℝ] V →ₗ[ℝ] ℝ) (ω : V) : Prop

The Mukai class map computes the rank and the ω-degree.

Two identifications, no discriminants: nothing here mentions torsion, a cutoff, or the Mukai square. For any class map whose first two coordinates are the rank and c₁ the first holds by definition and the second reads degree = ω·c₁; the third coordinate (ch₂ + r on a K3 surface, ch₂ for the plain Chern character) is not constrained.

The degree of WeakSlopeData is real-valued, so ω may be any real class, as in Bridgeland's construction. The rank is integral, and that integrality is what the boundary argument's passage from 0 < r to 1 ≤ r uses.

Compare SlopeData's geometric fields, which are of the same kind. What is deliberately not here is any hypothesis of the shape "E is torsion" or "μ(E) > β·ω" — those are the conclusions.

• rank_eq (E : A) : (D.mukai (K₀Ab.of E)).1 = ↑(S.rank E)

  The rank component of the Mukai class is the rank.

• degree_eq (E : A) : (b ω) (D.mukai (K₀Ab.of E)).2.1 = S.degree E

  The ω-degree of the Mukai class's c₁ component is the degree.

theorem CategoryTheory.Triangulated.MukaiWeakSlopeCompat.im_charge {A : Type u} [Category.{v, u} A] [Abelian A] {V : Type u_1} [AddCommGroup V] [Module ℝ V] {D : MukaiChargeData A V} {S : WeakSlopeData A} {b : V →ₗ[ℝ] V →ₗ[ℝ] ℝ} {ω : V} (C : MukaiWeakSlopeCompat D S b ω) (hb : ∀ (x y : V), (b x) y = (b y) x) (β : V) (E : A) : (MukaiChargeData.charge b β ω D E).im = S.degree E - ↑(S.rank E) * (b β) ω

The identity. Mukai.im_expCharge under the identification: the imaginary part of Z(β,ω) is the degree, shifted by the rank times the cutoff.

theorem CategoryTheory.Triangulated.MukaiWeakSlopeCompat.im_charge_pos_iff_of_rank_pos {A : Type u} [Category.{v, u} A] [Abelian A] {V : Type u_1} [AddCommGroup V] [Module ℝ V] {D : MukaiChargeData A V} {S : WeakSlopeData A} {b : V →ₗ[ℝ] V →ₗ[ℝ] ℝ} {ω : V} (C : MukaiWeakSlopeCompat D S b ω) (hb : ∀ (x y : V), (b x) y = (b y) x) (β : V) {E : A} (hE : 0 < S.rank E) : 0 < (MukaiChargeData.charge b β ω D E).im ↔ ↑((b β) ω) < S.topSlope E

At positive rank the sign of Im Z(β,ω) is the slope comparison, exactly.

theorem CategoryTheory.Triangulated.MukaiWeakSlopeCompat.im_charge_eq_degree_of_rank_zero {A : Type u} [Category.{v, u} A] [Abelian A] {V : Type u_1} [AddCommGroup V] [Module ℝ V] {D : MukaiChargeData A V} {S : WeakSlopeData A} {b : V →ₗ[ℝ] V →ₗ[ℝ] ℝ} {ω : V} (C : MukaiWeakSlopeCompat D S b ω) (hb : ∀ (x y : V), (b x) y = (b y) x) (β : V) {E : A} (h : S.rank E = 0) : (MukaiChargeData.charge b β ω D E).im = S.degree E

At rank zero the identity reads Im Z = degree, which is nonnegative for a nonzero object — and zero exactly for the skyscraper.

theorem CategoryTheory.Triangulated.MukaiWeakSlopeCompat.im_charge_eq_zero_of_rank_pos_of_slope_eq {A : Type u} [Category.{v, u} A] [Abelian A] {V : Type u_1} [AddCommGroup V] [Module ℝ V] {D : MukaiChargeData A V} {S : WeakSlopeData A} {b : V →ₗ[ℝ] V →ₗ[ℝ] ℝ} {ω : V} (C : MukaiWeakSlopeCompat D S b ω) (hb : ∀ (x y : V), (b x) y = (b y) x) (β : V) {E : A} (hrank : 0 < S.rank E) (heq : S.slope E = (b β) ω) : (MukaiChargeData.charge b β ω D E).im = 0

A positive-rank object exactly at the slope cutoff has zero imaginary Mukai charge.

theorem CategoryTheory.Triangulated.MukaiWeakSlopeCompat.im_charge_nonneg_of_mem_hnTors {A : Type u} [Category.{v, u} A] [Abelian A] {V : Type u_1} [AddCommGroup V] [Module ℝ V] {D : MukaiChargeData A V} {S : WeakSlopeData A} {b : V →ₗ[ℝ] V →ₗ[ℝ] ℝ} {ω : V} (C : MukaiWeakSlopeCompat D S b ω) (hb : ∀ (x y : V), (b x) y = (b y) x) (β : V) (hHN : S.toWeakStabilityFunction.HasHNProperty) {E : A} (hE : ¬Limits.IsZero E) (h : E ∈ S.toWeakStabilityFunction.hnTors ↑((b β) ω)) : 0 ≤ (MukaiChargeData.charge b β ω D E).im

The torsion class has nonnegative Im Z(β,ω).

Cases 1--3 of Lemma 6.2 conclude this, and the bound is sharp rather than strict: at rank zero Im Z is the degree, which vanishes on the skyscraper.

theorem CategoryTheory.Triangulated.MukaiWeakSlopeCompat.im_charge_pos_of_mem_hnTors_of_rank_pos {A : Type u} [Category.{v, u} A] [Abelian A] {V : Type u_1} [AddCommGroup V] [Module ℝ V] {D : MukaiChargeData A V} {S : WeakSlopeData A} {b : V →ₗ[ℝ] V →ₗ[ℝ] ℝ} {ω : V} (C : MukaiWeakSlopeCompat D S b ω) (hb : ∀ (x y : V), (b x) y = (b y) x) (β : V) (hHN : S.toWeakStabilityFunction.HasHNProperty) {E : A} (hE : ¬Limits.IsZero E) (hrank : 0 < S.rank E) (h : E ∈ S.toWeakStabilityFunction.hnTors ↑((b β) ω)) : 0 < (MukaiChargeData.charge b β ω D E).im

At positive rank the bound is strict, which is what cases 1--3 of Lemma 6.2 need: the charge lands in the open upper half plane.

theorem CategoryTheory.Triangulated.MukaiWeakSlopeCompat.rank_eq_zero_of_im_eq_zero_of_mem_hnTors {A : Type u} [Category.{v, u} A] [Abelian A] {V : Type u_1} [AddCommGroup V] [Module ℝ V] {D : MukaiChargeData A V} {S : WeakSlopeData A} {b : V →ₗ[ℝ] V →ₗ[ℝ] ℝ} {ω : V} (C : MukaiWeakSlopeCompat D S b ω) (hb : ∀ (x y : V), (b x) y = (b y) x) (β : V) (hHN : S.toWeakStabilityFunction.HasHNProperty) {E : A} (hE : ¬Limits.IsZero E) (h : E ∈ S.toWeakStabilityFunction.hnTors ↑((b β) ω)) (him : (MukaiChargeData.charge b β ω D E).im = 0) : S.rank E = 0 ∧ S.degree E = 0

The boundary of the torsion class is exactly the skyscraper.

An object of the torsion class with Im Z(β,ω) = 0 has rank zero and degree zero, so its μ-slope charge is 0. This is the case that has no phase, the case SlopeData cannot express, and the reason Z(β,ω) is only a weak stability function here.

theorem CategoryTheory.Triangulated.MukaiWeakSlopeCompat.im_charge_nonpos_of_mem_hnFree {A : Type u} [Category.{v, u} A] [Abelian A] {V : Type u_1} [AddCommGroup V] [Module ℝ V] {D : MukaiChargeData A V} {S : WeakSlopeData A} {b : V →ₗ[ℝ] V →ₗ[ℝ] ℝ} {ω : V} (C : MukaiWeakSlopeCompat D S b ω) (hb : ∀ (x y : V), (b x) y = (b y) x) (β : V) (hHN : S.toWeakStabilityFunction.HasHNProperty) {E : A} (hE : ¬Limits.IsZero E) (h : E ∈ S.toWeakStabilityFunction.hnFree ↑((b β) ω)) : (MukaiChargeData.charge b β ω D E).im ≤ 0

The sign statement for the torsion-free class.

Inhabitants

MukaiWeakSlopeCompat asserted a compatibility without exhibiting anything satisfying it, which is the shape scripts/check_single_instantiation.py exists to catch: an abstraction written for N cases and instantiated zero times. These are the constructions that discharge it.

The content is that the two fields constrain only the first two components of the Mukai class. The third — ch₂ + r on a surface — is free, and is carried here as an arbitrary additive s, which is why it appears as a parameter rather than being pinned to zero. A polarisation vector v normalised by b ω v = 1 is exactly what turns the ω-degree of the c₁ slot into the degree.

def CategoryTheory.Triangulated.WeakSlopeData.c₁Hom {A : Type u} [Category.{v, u} A] [Abelian A] {V : Type u_1} [AddCommGroup V] [Module ℝ V] (S : WeakSlopeData A) (v : V) : K₀Ab A →+ V

The c₁ slot of the Mukai class built from a weak slope datum: the degree, scaled into a chosen direction v.

Equations

• S.c₁Hom v = AddMonoidHom.mk' (fun (x : CategoryTheory.K₀Ab A) => S.degreeHom x • v) ⋯

@[simp]

theorem CategoryTheory.Triangulated.WeakSlopeData.c₁Hom_apply {A : Type u} [Category.{v, u} A] [Abelian A] {V : Type u_1} [AddCommGroup V] [Module ℝ V] (S : WeakSlopeData A) (v : V) (x : K₀Ab A) : (S.c₁Hom v) x = S.degreeHom x • v

def CategoryTheory.Triangulated.WeakSlopeData.toMukaiChargeData {A : Type u} [Category.{v, u} A] [Abelian A] {V : Type u_1} [AddCommGroup V] [Module ℝ V] (S : WeakSlopeData A) (v : V) (s : K₀Ab A →+ ℝ) : MukaiChargeData A V

A Mukai class map built from a weak slope datum: rank in the first slot, the degree scaled into v in the second, and an arbitrary additive s in the third.

Equations

• S.toMukaiChargeData v s = { mukai := ((Int.castAddHom ℝ).comp S.rankHom).prod ((S.c₁Hom v).prod s) }

@[simp]

theorem CategoryTheory.Triangulated.WeakSlopeData.toMukaiChargeData_mukai {A : Type u} [Category.{v, u} A] [Abelian A] {V : Type u_1} [AddCommGroup V] [Module ℝ V] (S : WeakSlopeData A) (v : V) (s : K₀Ab A →+ ℝ) (x : K₀Ab A) : (S.toMukaiChargeData v s).mukai x = (↑(S.rankHom x), S.degreeHom x • v, s x)

theorem CategoryTheory.Triangulated.MukaiWeakSlopeCompat.ofWeakSlopeData {A : Type u} [Category.{v, u} A] [Abelian A] {V : Type u_1} [AddCommGroup V] [Module ℝ V] (S : WeakSlopeData A) (b : V →ₗ[ℝ] V →ₗ[ℝ] ℝ) (ω v : V) (hv : (b ω) v = 1) (s : K₀Ab A →+ ℝ) : MukaiWeakSlopeCompat (S.toMukaiChargeData v s) S b ω

The compatibility is inhabited.

Given a weak slope datum and a direction v normalised against the polarisation by b ω v = 1, the Mukai class map of WeakSlopeData.toMukaiChargeData is compatible with it. The third component is arbitrary, which is the point: the two fields say nothing about it.

theorem CategoryTheory.Triangulated.MukaiWeakSlopeCompat.ofSlopeData {A : Type u} [Category.{v, u} A] [Abelian A] {V : Type u_1} [AddCommGroup V] [Module ℝ V] (D : SlopeData A) (b : V →ₗ[ℝ] V →ₗ[ℝ] ℝ) (ω v : V) (hv : (b ω) v = 1) (s : K₀Ab A →+ ℝ) : MukaiWeakSlopeCompat (D.toWeakSlopeData.toMukaiChargeData v s) D.toWeakSlopeData b ω

The curve case is inhabited too, through SlopeData.toWeakSlopeData.

A second instantiation, at a different hypothesis class: SlopeData carries degree_pos_of_rank_zero, the curve condition, and forgets to a WeakSlopeData by weakening it to 0 ≤. So everything proved from MukaiWeakSlopeCompat applies on a curve as well as on a surface, and neither case is the only one.