The categorical Mukai charge is the numerical charge of the object's class

MukaiChargeData C W carries a hom K₀Ab A →+ RealExtension W and nothing ties it to any geometry: an arbitrary hom typechecks, so charge need not be the charge of anything. Separately, AdditiveMukaiData.numericalCharge computes the same shape from a numerical class in N, and the two were never related by any lemma.

That gap is why the support-property theorems proved on the numerical side — numericalCharge_ne_zero_of_nonneg, mukaiForm_neg_of_numericalCharge_eq_zero, mem_wall_iff_numericalCharge_eq_zero — were unreachable from an object of a heart, which is exactly what a stability function's positivity obligation holds.

What this file does

toMukaiChargeData builds the class map as a composition of homs

K₀Ab A --cl--> N --mukaiVectorHom--> MukaiLattice Λ --extendMapHom--> RealExtension W

so charge_toMukaiChargeData is definitional: the categorical charge of an object is the numerical charge of its class. Nothing along the chain re-proves additivity, and a MukaiChargeData built this way cannot be unrelated to the geometry, because the geometry is what it is made of.

What is still supplied, not proved

cl : K₀Ab A →+ N is an argument. Nothing in this repository constructs one — The generic K₀.Realization root likewise treats such a class map as supplied, so this file makes the comparison available without pretending it exists.

The numerical quotient is also still bypassed. N is documented as K(X)/≡, but the lane quotients it again by leftRadical, and the only geometric class map in the tree lands in that quotient while numericalCharge is defined on N. Until leftRadical ≤ ker mukaiVectorHom is proved, the support-property theorems keep their extendMap … ≠ 0 hypotheses instead of the E ≠ 0 a consumer can actually discharge.

noncomputable def AlgebraicGeometry.Numerical.K3.AdditiveMukaiData.toMukaiChargeData {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {R : Type u_1} {N : Type u_2} {Λ : Type u_3} [CommRing R] [Algebra ℚ R] [AddCommGroup N] [AddCommGroup Λ] {V : NumericalVarietyData 2 R N} {W : Type w'} [NormedAddCommGroup W] [NormedSpace ℝ W] (D : AdditiveMukaiData V Λ) (f : Λ →ₗ[ℤ] W) (cl : CategoryTheory.K₀Ab C →+ N) : CategoryTheory.Triangulated.MukaiChargeData C W

The categorical Mukai charge carrier built from numerical data.

The class map is the composite of three homs, so the three formal properties a charge needs are inherited rather than restated.

Equations

• D.toMukaiChargeData f cl = { mukai := (Mukai.extendMapHom f).comp (D.mukaiVectorHom.comp cl) }

@[simp]

theorem AlgebraicGeometry.Numerical.K3.AdditiveMukaiData.toMukaiChargeData_mukai {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {R : Type u_1} {N : Type u_2} {Λ : Type u_3} [CommRing R] [Algebra ℚ R] [AddCommGroup N] [AddCommGroup Λ] {V : NumericalVarietyData 2 R N} {W : Type w'} [NormedAddCommGroup W] [NormedSpace ℝ W] (D : AdditiveMukaiData V Λ) (f : Λ →ₗ[ℤ] W) (cl : CategoryTheory.K₀Ab C →+ N) (x : CategoryTheory.K₀Ab C) : (D.toMukaiChargeData f cl).mukai x = Mukai.extendMap f (D.mukaiVectorHom (cl x))

theorem AlgebraicGeometry.Numerical.K3.AdditiveMukaiData.charge_toMukaiChargeData {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {R : Type u_1} {N : Type u_2} {Λ : Type u_3} [CommRing R] [Algebra ℚ R] [AddCommGroup N] [AddCommGroup Λ] {V : NumericalVarietyData 2 R N} {W : Type w'} [NormedAddCommGroup W] [NormedSpace ℝ W] (D : AdditiveMukaiData V Λ) (f : Λ →ₗ[ℤ] W) (cl : CategoryTheory.K₀Ab C →+ N) (bR : W →ₗ[ℝ] W →ₗ[ℝ] ℝ) (β ω : W) (E : C) : CategoryTheory.Triangulated.MukaiChargeData.charge bR β ω (D.toMukaiChargeData f cl) E = D.numericalCharge bR f β ω (cl (CategoryTheory.K₀Ab.of E))

The lemma that was missing: the categorical charge of an object is the numerical charge of its class.

Definitional, because the class map is a composition of homs rather than a separately-postulated function. Its use is that every support-property theorem stated about numericalCharge now applies to an object of an abelian category through its class.

theorem AlgebraicGeometry.Numerical.K3.AdditiveMukaiData.mem_wall_iff_numericalCharge_eq_zero {R : Type u_1} {N : Type u_2} {Λ : Type u_3} [CommRing R] [Algebra ℚ R] [AddCommGroup N] [AddCommGroup Λ] {V : NumericalVarietyData 2 R N} {W : Type w'} [NormedAddCommGroup W] [NormedSpace ℝ W] {D : AdditiveMukaiData V Λ} {f : Λ →ₗ[ℤ] W} {bR : W →ₗ[ℝ] W →ₗ[ℝ] ℝ} {β ω : W} (hb : ∀ (x y : W), (bR x) y = (bR y) x) (hω : 0 < (bR ω) ω) (E : N) : PeriodDomain.pairSpan (Mukai.expRe bR β ω) (Mukai.expIm bR β ω) ∈ PeriodDomain.orthogonalityLocus (Mukai.realForm bR) (Mukai.extendMap f (D.mukaiVectorHom E)) ↔ D.numericalCharge bR f β ω E = 0

A wall is a vanishing charge, for the class of an object. This interpretation lives in the categorical stability adapter so the underlying numerical charge remains independent of wall loci.