√td_X read off a numerical realization, and Bridgeland's K3 charge

CentralCharge/Divisorial/Mukai.lean owns the Mukai vector and the Mukai charge on an abstract real divisor space, parameterized by a supplied SqrtTodd: the codimension-one class √td₁ and the number ∫√td₂. This file supplies that datum from geometry rather than by hand, using the sqrtToddComp of Numerical/Mukai/SqrtTodd.lean, and identifies the result on a K3.

Three things are proved.

• sqrtTodd_eq_k3: on a K3 the realized square root is SqrtTodd.k3, the formal content of √td(X) = 1 + [pt]. It rests on K3.sqrtToddComp_one and K3.degree_sqrtToddComp_two, both already proved from IsK3; nothing new is assumed.
• mukaiVector_snd_snd_of_isK3: the third coordinate of the Mukai vector is K3.mukaiS, the repository's existing s = rank + ∫ch₂, and hence K3.mukaiSInt = χ − rank once Hirzebruch--Riemann--Roch is supplied. This is what ties the new adapter to GrothendieckGroup/MukaiVector.lean and the K3 model of Models/Surface/K3Mukai.lean instead of leaving two unrelated notions of "Mukai vector" in the library.
• mukaiCharge_of_isK3: Bridgeland's charge is the ordinary divisorial charge minus the rank.

What this does not do, and what has since been done elsewhere

The statements below hold for any realization of any NumericalVarietyData 2 satisfying IsK3; this file constructs none.

Two gaps this section used to record are now closed, in the examples rather than here. Examples/Surface/RankOneRealization.lean constructs the numerical realization of the K3 model of Models/Surface/K3.lean, and Examples/Surface/K3MukaiComparison.lean compares the real Mukai extension used here with the integral Mukai.MukaiLattice of GrothendieckGroup/MukaiVector.lean, through the lattice map that Numerical/Mukai/Integral.lean asks for. Both remain outside this file, which stays free of any particular model.

noncomputable def AlgebraicGeometry.Numerical.Surface.NumericalRealization.sqrtTodd {A : Type u} {N : Type v} {D : Type w} [CommRing A] [Algebra ℚ A] [AddCommGroup N] [AddCommGroup D] [Module ℝ D] {V : NumericalVarietyData 2 A N} (R : NumericalRealization V.ring) : CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.Divisorial.SqrtTodd D

√td_X as a surface Mukai vector sees it: the realized codimension-one component and the integrated codimension-two component.

Equations

• R.sqrtTodd = { divisor := R.divisorClass ⟨V.sqrtToddComp 1, ⋯⟩, number := ↑(V.ring.degree (V.sqrtToddComp 2)) }

@[simp]

theorem AlgebraicGeometry.Numerical.Surface.NumericalRealization.sqrtTodd_divisor {A : Type u} {N : Type v} {D : Type w} [CommRing A] [Algebra ℚ A] [AddCommGroup N] [AddCommGroup D] [Module ℝ D] {V : NumericalVarietyData 2 A N} (R : NumericalRealization V.ring) : R.sqrtTodd.divisor = R.divisorClass ⟨V.sqrtToddComp 1, ⋯⟩

@[simp]

theorem AlgebraicGeometry.Numerical.Surface.NumericalRealization.sqrtTodd_number {A : Type u} {N : Type v} {D : Type w} [CommRing A] [Algebra ℚ A] [AddCommGroup N] [AddCommGroup D] [Module ℝ D] {V : NumericalVarietyData 2 A N} (R : NumericalRealization V.ring) : R.sqrtTodd.number = ↑(V.ring.degree (V.sqrtToddComp 2))

theorem AlgebraicGeometry.Numerical.Surface.NumericalRealization.sqrtTodd_eq_k3 {A : Type u} {N : Type v} {D : Type w} [CommRing A] [Algebra ℚ A] [AddCommGroup N] [AddCommGroup D] [Module ℝ D] {V : NumericalVarietyData 2 A N} (R : NumericalRealization V.ring) (hK3 : K3.IsK3 V) : R.sqrtTodd = CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.Divisorial.SqrtTodd.k3

On a K3 the realized square root is 1 + [pt]. This is K3.sqrtToddComp_one and K3.degree_sqrtToddComp_two in the shape the Mukai vector consumes.

theorem AlgebraicGeometry.Numerical.Surface.NumericalRealization.mukaiVector_of_isK3 {A : Type u} {N : Type v} {D : Type w} [CommRing A] [Algebra ℚ A] [AddCommGroup N] [AddCommGroup D] [Module ℝ D] {V : NumericalVarietyData 2 A N} (R : NumericalRealization V.ring) (hK3 : K3.IsK3 V) (E : N) : (R.chernCharacter.mukaiVector R.divisorSpace R.sqrtTodd) E = (↑(V.rank E), R.chernCharacter.chOne E, ↑(V.ring.degree (V.chComp E 2)) + ↑(V.rank E))

On a K3 the Mukai vector is (rank, c₁, ∫ch₂ + rank).

theorem AlgebraicGeometry.Numerical.Surface.NumericalRealization.mukaiVector_snd_snd_of_isK3 {A : Type u} {N : Type v} {D : Type w} [CommRing A] [Algebra ℚ A] [AddCommGroup N] [AddCommGroup D] [Module ℝ D] {V : NumericalVarietyData 2 A N} (R : NumericalRealization V.ring) (hK3 : K3.IsK3 V) (E : N) : ((R.chernCharacter.mukaiVector R.divisorSpace R.sqrtTodd) E).2.2 = ↑(K3.mukaiS V E)

The third Mukai coordinate is the repository's K3.mukaiS, namely s = rank + ∫ch₂. This is what identifies the vector built here with the one GrothendieckGroup/MukaiVector.lean already uses.

theorem AlgebraicGeometry.Numerical.Surface.NumericalRealization.mukaiVector_snd_snd_eq_mukaiSInt {A : Type u} {N : Type v} {D : Type w} [CommRing A] [Algebra ℚ A] [AddCommGroup N] [AddCommGroup D] [Module ℝ D] {V : NumericalVarietyData 2 A N} (R : NumericalRealization V.ring) (hHRR : V.SatisfiesHRR) (hK3 : K3.IsK3 V) (E : N) : ((R.chernCharacter.mukaiVector R.divisorSpace R.sqrtTodd) E).2.2 = ↑(K3.mukaiSInt V E)

The same coordinate, as the integer s = χ − rank of K3.mukaiSInt, once Hirzebruch--Riemann--Roch is supplied.

theorem AlgebraicGeometry.Numerical.Surface.NumericalRealization.mukaiCharge_of_isK3 {A : Type u} {N : Type v} {D : Type w} [CommRing A] [Algebra ℚ A] [AddCommGroup N] [AddCommGroup D] [Module ℝ D] {V : NumericalVarietyData 2 A N} (R : NumericalRealization V.ring) (hK3 : K3.IsK3 V) (P : CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.Divisorial.StabilityParameters D) (E : N) : (R.chernCharacter.mukaiCharge R.divisorSpace R.sqrtTodd P) E = (R.chernCharacter.centralCharge R.divisorSpace P) E - ↑↑(V.rank E)

Bridgeland's K3 charge is the ordinary divisorial charge minus the rank. The two presentations differ by an additive term linear in the class, not by a scalar, so their walls differ.