The exponential charge Z(β,ω) carried by a Mukai class map

Bridgeland's Lemma 6.2 (math/0307164, §6) says that Z(β,ω) is a stability function on the tilted heart 𝒜(β,ω). CentralCharge/Mukai/Positivity.lean (#742) proved the numerical core of the one hard case, with no category in sight. This file is the bridge: it carries a Mukai class map from an abelian category into the real Mukai extension, so that Z(β,ω) becomes a charge on objects.

What this file is, and what it is deliberately not

It is the mechanical half of #740 step 2 — map_zero, map_iso and additive, all of which follow from additivity of the charge in the class together with the corresponding property of the class map.

It is not the case analysis. MukaiChargeData carries only the class map and its three formal properties; it has no field asserting anything about torsion, rank, slope, or the Mukai square. That is deliberate. Bundling the case discriminants as hypotheses would make nonzero_mem a one-line case split over invented assumptions — it would compile, pass every gate, and prove nothing. The four cases of Lemma 6.2 have to be proved from the tilted heart's own description (hnTilt_heart_iff, mem_hnTors_of_rank_zero, degree_pos_of_rank_zero), and that work is not in this file.

So there is no toStabilityFunction here. SlopeData.toStabilityFunction exists because SlopeData's geometric fields genuinely discharge nonzero_mem; the analogous step for Z(β,ω) is the open part of #740.

The sign convention, which no gate catches

Bridgeland's §6 states every sign for the sheaf, not for the object of the heart. In the boundary case E is torsion-free with μ_ω(E) = β·ω, so E ∈ F(β) and the object of the tilted heart is E⟦1⟧, with Z(E⟦1⟧) = -Z(E). CentralCharge/Mukai/Positivity.lean concludes Re Z(E) > 0 for the sheaf; the heart object therefore has Im = 0 and Re < 0, which is the {z | z.im = 0 ∧ z.re < 0} half of semiClosedUpperHalfPlane. The two apparent sign reversals cancel, and getting this backwards yields a false statement that compiles.

Additivity of the charge

Mukai.expChargeHom owns additivity at the numerical layer. This file only composes that homomorphism with a Mukai class map and then evaluates it on Grothendieck classes of objects.

The following historical names remain in the categorical namespace for API stability. Their canonical numerical owners are now Mukai.expCharge_zero, Mukai.expCharge_add, and Mukai.expCharge_neg.

theorem CategoryTheory.Triangulated.expCharge_zero {V : Type u_1} [AddCommGroup V] [Module ℝ V] (b : V →ₗ[ℝ] V →ₗ[ℝ] ℝ) (β ω : V) : Mukai.expCharge b β ω 0 = 0

The exponential charge kills the zero class.

theorem CategoryTheory.Triangulated.expCharge_add {V : Type u_1} [AddCommGroup V] [Module ℝ V] (b : V →ₗ[ℝ] V →ₗ[ℝ] ℝ) (β ω : V) (v w : Mukai.RealExtension V) : Mukai.expCharge b β ω (v + w) = Mukai.expCharge b β ω v + Mukai.expCharge b β ω w

The exponential charge is additive in the Mukai class.

theorem CategoryTheory.Triangulated.expCharge_neg {V : Type u_1} [AddCommGroup V] [Module ℝ V] (b : V →ₗ[ℝ] V →ₗ[ℝ] ℝ) (β ω : V) (v : Mukai.RealExtension V) : Mukai.expCharge b β ω (-v) = -Mukai.expCharge b β ω v

The exponential charge negates on negated classes.

structure CategoryTheory.Triangulated.MukaiChargeData (A : Type u) [Category.{v, u} A] [Abelian A] (V : Type u_2) [AddCommGroup V] [Module ℝ V] : Type (max u u_2)

A Mukai class map, as a single hom out of the Grothendieck group.

This was three fields — mukai_zero, mukai_iso, mukai_additive — carried as data. They are the universal property of K₀Ab, so they are gone: one field remains, and the three formal properties come from AddMonoidHom and K₀Ab.of_isZero / of_iso / of_shortExact.

This generic carrier deliberately accepts any such hom. Concrete geometric consumers must construct it from their numerical class map; the K3 numerical lane does so in AlgebraicGeometry/Numerical/GrothendieckGroup/CategoricalChargeK3.lean, where the resulting charge is proved definitionally equal to numericalCharge.

• mukai : K₀Ab A →+ Mukai.RealExtension V

  The Mukai class, as a hom out of the Grothendieck group.

noncomputable def CategoryTheory.Triangulated.MukaiChargeData.chargeHom {V : Type u_1} [AddCommGroup V] [Module ℝ V] (b : V →ₗ[ℝ] V →ₗ[ℝ] ℝ) (β ω : V) {A : Type u} [Category.{v, u} A] [Abelian A] (D : MukaiChargeData A V) : K₀Ab A →+ ℂ

Z(β,ω) as an additive homomorphism on the heart's Grothendieck group.

Equations

• CategoryTheory.Triangulated.MukaiChargeData.chargeHom b β ω D = (Mukai.expChargeHom b β ω).comp D.mukai

@[simp]

theorem CategoryTheory.Triangulated.MukaiChargeData.chargeHom_apply {V : Type u_1} [AddCommGroup V] [Module ℝ V] (b : V →ₗ[ℝ] V →ₗ[ℝ] ℝ) (β ω : V) {A : Type u} [Category.{v, u} A] [Abelian A] (D : MukaiChargeData A V) (x : K₀Ab A) : (chargeHom b β ω D) x = Mukai.expCharge b β ω (D.mukai x)

noncomputable def CategoryTheory.Triangulated.MukaiChargeData.charge {V : Type u_1} [AddCommGroup V] [Module ℝ V] (b : V →ₗ[ℝ] V →ₗ[ℝ] ℝ) (β ω : V) {A : Type u} [Category.{v, u} A] [Abelian A] (D : MukaiChargeData A V) (E : A) : ℂ

Z(β,ω) as a charge on objects.

Equations

• CategoryTheory.Triangulated.MukaiChargeData.charge b β ω D E = (CategoryTheory.Triangulated.MukaiChargeData.chargeHom b β ω D) (CategoryTheory.K₀Ab.of E)

@[simp]

theorem CategoryTheory.Triangulated.MukaiChargeData.charge_apply {V : Type u_1} [AddCommGroup V] [Module ℝ V] (b : V →ₗ[ℝ] V →ₗ[ℝ] ℝ) (β ω : V) {A : Type u} [Category.{v, u} A] [Abelian A] (D : MukaiChargeData A V) (E : A) : charge b β ω D E = Mukai.expCharge b β ω (D.mukai (K₀Ab.of E))

theorem CategoryTheory.Triangulated.MukaiChargeData.charge_zero {V : Type u_1} [AddCommGroup V] [Module ℝ V] (b : V →ₗ[ℝ] V →ₗ[ℝ] ℝ) (β ω : V) {A : Type u} [Category.{v, u} A] [Abelian A] (D : MukaiChargeData A V) {E : A} (hE : Limits.IsZero E) : charge b β ω D E = 0

theorem CategoryTheory.Triangulated.MukaiChargeData.charge_iso {V : Type u_1} [AddCommGroup V] [Module ℝ V] (b : V →ₗ[ℝ] V →ₗ[ℝ] ℝ) (β ω : V) {A : Type u} [Category.{v, u} A] [Abelian A] (D : MukaiChargeData A V) {E F : A} (e : E ≅ F) : charge b β ω D E = charge b β ω D F

theorem CategoryTheory.Triangulated.MukaiChargeData.charge_additive {V : Type u_1} [AddCommGroup V] [Module ℝ V] (b : V →ₗ[ℝ] V →ₗ[ℝ] ℝ) (β ω : V) {A : Type u} [Category.{v, u} A] [Abelian A] (D : MukaiChargeData A V) (S : ShortComplex A) (hS : S.ShortExact) : charge b β ω D S.X₂ = charge b β ω D S.X₁ + charge b β ω D S.X₃