The integral Mukai lattice inside the real extension

The wall-finiteness results take the lattice as the ℤ-span of an ℝ-basis of an abstract quadratic space. The Mukai lattice of a K3 is ℤ ⊕ NS(X) ⊕ ℤ with the integral pairing, which is what Lattice/Mukai/Basic.lean builds. This file connects them, so that "finitely many spherical walls" is a statement about integral classes rather than about an abstract ZSpan.

Three steps

• extendBasis — a basis of V induces one of ℝ × V × ℝ, namely (1,0,0), (0, vᵢ, 0), (0,0,1). The finiteness theorems want a basis of the whole space; this is it.
• span_range_extendBasis — its ℤ-span is the integral Mukai extension: integer rank and corank, lattice middle. This is what turns those theorems into statements about integral classes.
• realPairing_extendMap — for a lattice map f respecting the two forms, the induced map on Mukai extensions carries Mukai.pairing to Mukai.realPairing. This is the literal statement that the two files describe the same pairing, and it is where a factor or a sign error would surface.

The lattice is presented by a basis, not by a tensor product

N ⊗ ℝ would be the textbook construction and is not used: a basis gives everything below with no tensor-product plumbing, and the geometric input — that N(X) is free of finite rank and spans N(X) ⊗ ℝ — is exactly what a basis is.

V remains an arbitrary real bilinear space; no geometry is asserted.

Why this path

The cutover ledger's row 03 puts the Mukai vector, the integral structure and the surface realization under AlgebraicGeometry/Numerical/Mukai/, and this is the integral structure. The directory is numerical Mukai theory, not scheme-level geometry -- Pairing.lean and VectorClass.lean beside it mention no scheme either -- so a file that asserts no geometry is at home here.

Every consumer is already in this subtree: the two surface wall examples and GrothendieckGroup/CentralChargeK3.lean. Nothing under StabilityCondition/ reaches it, which is the evidence that it is not part of the charge bridge it travelled with; it is the comparison between the integral Mukai lattice and its real extension, plus the two finiteness statements that comparison exists to supply.

noncomputable def Mukai.extendBasis {ι : Type u_1} {V : Type u_2} [AddCommGroup V] [Module ℝ V] (v : Module.Basis ι ℝ V) : Module.Basis (Unit ⊕ ι ⊕ Unit) ℝ (RealExtension V)

The basis of the real Mukai extension induced by a basis of V.

Equations

• Mukai.extendBasis v = (Module.Basis.singleton Unit ℝ).prod (v.prod (Module.Basis.singleton Unit ℝ))

def Mukai.integralExtension {V : Type u_2} [AddCommGroup V] (Λ : Submodule ℤ V) : Submodule ℤ (RealExtension V)

The integral Mukai extension of a lattice in V: integral rank and corank, lattice middle.

Equations

• Mukai.integralExtension Λ = (ℤ ∙ 1).prod (Λ.prod (ℤ ∙ 1))

theorem Mukai.span_range_extendBasis {ι : Type u_1} {V : Type u_2} [AddCommGroup V] [Module ℝ V] (v : Module.Basis ι ℝ V) : Submodule.span ℤ (Set.range ⇑(extendBasis v)) = integralExtension (Submodule.span ℤ (Set.range ⇑v))

The ℤ-span of the extended basis is the integral Mukai extension.

def Mukai.extendMap {N : Type u_1} [AddCommGroup N] {V : Type u_2} [AddCommGroup V] (f : N →ₗ[ℤ] V) (u : MukaiLattice N) : RealExtension V

The map of Mukai extensions induced by a map of the middle summands.

Equations

• Mukai.extendMap f u = (↑u.1, f u.2.1, ↑u.2.2)

theorem Mukai.extendMap_add {N : Type u_1} [AddCommGroup N] {V : Type u_2} [AddCommGroup V] (f : N →ₗ[ℤ] V) (u w : MukaiLattice N) : extendMap f (u + w) = extendMap f u + extendMap f w

The induced map is additive: MukaiLattice addition is componentwise and each coordinate map is.

noncomputable def Mukai.extendMapHom {N : Type u_1} [AddCommGroup N] {V : Type u_2} [AddCommGroup V] (f : N →ₗ[ℤ] V) : MukaiLattice N →+ RealExtension V

extendMap as a bundled hom. It was proved additive and left as a bare function, which is what forces every consumer to re-prove additivity of whatever composite it sits in.

Equations

• Mukai.extendMapHom f = AddMonoidHom.mk' (Mukai.extendMap f) ⋯

theorem Mukai.realPairing_extendMap {N : Type u_1} [AddCommGroup N] {V : Type u_2} [AddCommGroup V] [Module ℝ V] (bZ : N →ₗ[ℤ] N →ₗ[ℤ] ℤ) (bR : V →ₗ[ℝ] V →ₗ[ℝ] ℝ) (f : N →ₗ[ℤ] V) (hf : ∀ (x y : N), (bR (f x)) (f y) = ↑((bZ x) y)) (u w : MukaiLattice N) : realPairing bR (extendMap f u) (extendMap f w) = ↑(pairing bZ u w)

The two pairings agree. For a map of middles that respects the forms, the integral Mukai pairing is the real one, cast.

theorem Mukai.isSphericalClass_extendMap {N : Type u_1} [AddCommGroup N] {V : Type u_2} [AddCommGroup V] [Module ℝ V] (bZ : N →ₗ[ℤ] N →ₗ[ℤ] ℤ) (bR : V →ₗ[ℝ] V →ₗ[ℝ] ℝ) (f : N →ₗ[ℤ] V) (hf : ∀ (x y : N), (bR (f x)) (f y) = ↑((bZ x) y)) (hb : ∀ (x y : V), (bR x) y = (bR y) x) {δ : MukaiLattice N} (hδ : IsSpherical bZ δ) : PeriodDomain.IsSphericalClass (realForm bR) (extendMap f δ)

A class of self-pairing -2 in the integral lattice is a spherical class of the real form. The -2 reads the same on both sides, which is the point of the halving convention in Mukai/RealForm.lean.

theorem Mukai.finite_sphericalOrthogonal_integralExtension {ι : Type u_1} [Finite ι] {V : Type u_2} [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ V] (b : V →ₗ[ℝ] V →ₗ[ℝ] ℝ) (hsig : PeriodDomain.HasSignatureTwo (realForm b)) {W : Submodule ℝ (RealExtension V)} (hW : PeriodDomain.IsPositivePlane (realForm b) W) (v : Module.Basis ι ℝ V) : (PeriodDomain.sphericalOrthogonal (realForm b) W ∩ ↑(integralExtension (Submodule.span ℤ (Set.range ⇑v)))).Finite

Finitely many integral spherical classes are orthogonal to a positive plane, stated over the integral Mukai extension of the lattice rather than over an abstract ZSpan.

theorem Mukai.finite_orthogonalClasses_integralExtension {ι : Type u_1} [Finite ι] {V : Type u_2} [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ V] (b : V →ₗ[ℝ] V →ₗ[ℝ] ℝ) (R : PeriodDomain.PlaneRegion (realForm b)) (v : Module.Basis ι ℝ V) : (R.orthogonalClasses ∩ ↑(integralExtension (Submodule.span ℤ (Set.range ⇑v)))).Finite

The region-wise form of the same statement.