The integral and real Mukai structures of the K3 model agree

The degree-2d K3 model carries two Mukai structures that had nothing to do with each other.

• K3Mukai.lean builds the integral one: k3IntegralMukaiData, with lattice ℤ, form ⟪x, y⟫ = 2d·x·y, and mukaiVector E = (r, c, χ − r) in Mukai.MukaiLattice ℤ. Sphericality there is ⟪v, v⟫ = -2 over ℤ, and isSpherical_mukaiVector_iff characterises it.
• RankOneRealization.lean builds the real one: the divisor line ℝ with form 2d·x·y, whose real Mukai extension is where every wall statement of Divisorial/Signature.lean and Divisorial/Region.lean lives. Sphericality there is PeriodDomain.IsSphericalClass.

Numerical/Mukai/Integral.lean has carried the general comparison for some time — extendMap, realPairing_extendMap, isSphericalClass_extendMap — waiting on a lattice map that respects both forms. On this model that map is the inclusion ℤ → ℝ, and the forms agree on the nose.

Why this matters beyond tidiness

Every wall-finiteness statement proved for this model counts real spherical classes. The geometric content is about integral ones: ⟪v, v⟫ = -2 in the Mukai lattice, which GrothendieckGroup/MukaiVector.lean relates to χ₂ and to the expected dimension of a moduli space. k3_isSphericalClass_of_isSpherical is the link, so k3_finite_walls_meeting_box and its siblings become statements about the classes the geometry cares about rather than about a real approximation of them.

k3_mukaiVector_eq_extendMap is the identification that carries it: the real Mukai vector of a numerical class is the integral one, extended.

What is not claimed

Nothing here identifies either carrier with K_num(X) for a geometric K3, and no Riemann--Roch input is added: mukaiVector_k3 already evaluated the integral vector, and this file only compares.

The lattice map

def AlgebraicGeometry.Numerical.Examples.k3LatticeMap : ℤ →ₗ[ℤ] SurfaceDivisor

The inclusion of the rank-one Néron--Severi lattice ℤ·H into the real divisor line, sending H to the unit vector.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem AlgebraicGeometry.Numerical.Examples.k3LatticeMap_apply (n : ℤ) : k3LatticeMap n = ↑n

theorem AlgebraicGeometry.Numerical.Examples.k3LatticeMap_pairing (d : ℕ) (x y : ℤ) : ((surfaceDivisorSpace (2 * ↑d)).intersection (k3LatticeMap x)) (k3LatticeMap y) = ↑(((k3MukaiForm d) x) y)

The two forms agree. This is the hypothesis every theorem of Numerical/Mukai/Integral.lean waits on, and on this model it is a cast.

The two pairings, and the two Mukai vectors

theorem AlgebraicGeometry.Numerical.Examples.k3_realPairing_extendMap (d : ℕ) (u w : Mukai.MukaiLattice ℤ) : Mukai.realPairing (surfaceDivisorSpace (2 * ↑d)).intersection (Mukai.extendMap k3LatticeMap u) (Mukai.extendMap k3LatticeMap w) = ↑(Mukai.pairing (k3MukaiForm d) u w)

The integral Mukai pairing is the real one.

theorem AlgebraicGeometry.Numerical.Examples.k3_mukaiVector_eq_extendMap (d : ℕ) (hd : d ≠ 0) (E : SurfaceNum) : ((k3Realization d).chernCharacter.mukaiVector (k3Realization d).divisorSpace (k3Realization d).sqrtTodd) E = Mukai.extendMap k3LatticeMap ((k3IntegralMukaiData d).mukaiVector E)

The real Mukai vector is the integral one, extended.

The left side is CentralCharge/Divisorial/Mukai.lean read through the realization of RankOneRealization.lean; the right side is GrothendieckGroup/MukaiVector.lean read through k3IntegralMukaiData. They are the same triple.

Integral sphericality is real sphericality

theorem AlgebraicGeometry.Numerical.Examples.k3_isSphericalClass_of_isSpherical (d : ℕ) {δ : Mukai.MukaiLattice ℤ} (hδ : Mukai.IsSpherical (k3MukaiForm d) δ) : PeriodDomain.IsSphericalClass (Mukai.realForm (surfaceDivisorSpace (2 * ↑d)).intersection) (Mukai.extendMap k3LatticeMap δ)

An integral spherical class of the Mukai lattice is a spherical class of the real form.

The -2 reads the same on both sides, which is what the halving convention of Mukai/RealForm.lean exists for. This is the link that makes the wall statements about integral classes.

theorem AlgebraicGeometry.Numerical.Examples.k3_isSphericalClass_mukaiVector (d : ℕ) (hd : d ≠ 0) {E : SurfaceNum} (hE : Mukai.IsSpherical (k3MukaiForm d) ((k3IntegralMukaiData d).mukaiVector E)) : PeriodDomain.IsSphericalClass (Mukai.realForm (surfaceDivisorSpace (2 * ↑d)).intersection) (((k3Realization d).chernCharacter.mukaiVector (k3Realization d).divisorSpace (k3Realization d).sqrtTodd) E)

The Mukai vector of a numerical class is a real spherical class exactly when the integral criterion holds.

isSpherical_mukaiVector_iff states that criterion in terms of χ₂, so this is where the real wall theory meets the numerical invariants.

The integral Mukai extension is the lattice of the wall statements

theorem AlgebraicGeometry.Numerical.Examples.k3_extendMap_mem_integralExtension (δ : Mukai.MukaiLattice ℤ) : Mukai.extendMap k3LatticeMap δ ∈ Mukai.integralExtension (Submodule.span ℤ (Set.range ⇑surfaceDivisorBasis))

The extension of an integral class lands in the integral Mukai extension of ℤ·H, which is the lattice k3_finite_walls_integral and k3_finite_walls_meeting_box are stated against.

The spherical chart's integral comparison

def AlgebraicGeometry.Numerical.Examples.k3IntegralComparison (d : ℕ) : CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.Spherical.IntegralComparison (surfaceDivisorSpace (2 * ↑d)).intersection (k3MukaiForm d)

The first witness for Spherical.IntegralComparison.

Walls/Spherical/Basic.lean says of that structure: "it is supplied, never constructed — producing one is the geometric obligation of exhibiting NS(X) with its intersection form", and nothing in the tree constructed one, so pairing_map, selfPairing_map and isSpherical_map_iff were all vacuous.

On the degree-2d K3 the obligation is discharged by the rank-one lattice ℤ·H: the map is the inclusion of ℤ into the divisor line and the forms agree by k3LatticeMap_pairing.

Note this is a different structure from the Mukai comparison above. Its compat field is stated on all of ℤ, not on the image of a first Chern class, so it is a genuine comparison of forms rather than a constraint on one map.

Equations

• AlgebraicGeometry.Numerical.Examples.k3IntegralComparison d = { toFun := AlgebraicGeometry.Numerical.Examples.k3LatticeMap.toAddMonoidHom, compat := ⋯ }

@[simp]

theorem AlgebraicGeometry.Numerical.Examples.k3IntegralComparison_toFun (d : ℕ) (n : ℤ) : (k3IntegralComparison d).toFun n = ↑n

theorem AlgebraicGeometry.Numerical.Examples.k3_isSpherical_map_iff (d : ℕ) (v : Mukai.MukaiLattice ℤ) : CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.Spherical.IsSpherical (surfaceDivisorSpace (2 * ↑d)).intersection ((k3IntegralComparison d).map v) ↔ Mukai.IsSpherical (k3MukaiForm d) v

Integral and real sphericality agree in the (β, ω) chart, on the K3 model. This is isSpherical_map_iff with the witness supplied.

theorem AlgebraicGeometry.Numerical.Examples.k3IntegralComparison_map_eq_extendMap (d : ℕ) (v : Mukai.MukaiLattice ℤ) : (k3IntegralComparison d).map v = Mukai.extendMap k3LatticeMap v

The spherical chart's comparison agrees with the period-domain one: both send an integral class to the same real triple.

Wall finiteness, over integral classes

theorem AlgebraicGeometry.Numerical.Examples.extendMap_k3LatticeMap_injective : Function.Injective (Mukai.extendMap k3LatticeMap)

The extension map is injective, because the integer cast is.

theorem AlgebraicGeometry.Numerical.Examples.k3_finite_integral_spherical_walls (d : ℕ) (hd : d ≠ 0) (b₀ t₀ t₁ : ℝ) (ht₀ : 0 < t₀) : {δ : Mukai.MukaiLattice ℤ | Mukai.IsSpherical (k3MukaiForm d) δ ∧ ∃ p ∈ parameterBox b₀ t₀ t₁, (surfaceDivisorSpace (2 * ↑d)).expPlane p.1 p.2 ∈ PeriodDomain.orthogonalityLocus (Mukai.realForm (surfaceDivisorSpace (2 * ↑d)).intersection) (Mukai.extendMap k3LatticeMap δ)}.Finite

Only finitely many integral spherical classes of the Mukai lattice have a wall meeting the parameter box.

This is k3_finite_walls_meeting_box said over Mukai.MukaiLattice ℤ instead of over the real extension. It is the statement the geometry wants: the classes counted are those with ⟪v, v⟫ = -2 in the integral lattice, which isSpherical_mukaiVector_iff reads off χ₂.

Nothing new is assumed — only d > 0 and t₀ > 0, as before.