The Mukai extension of a symmetric bilinear lattice

Given an additive group N carrying a symmetric ℤ-bilinear form b, the Mukai extension is ℤ × N × ℤ with

⟪(r, c, s), (r', c', s')⟫ = b c c' - r * s' - r' * s.

This is not the Mukai lattice of a K3 surface. It is the abstract lattice that lattice is an instance of. Taking N = NS(X) with the intersection form recovers the algebraic Mukai lattice H⁰ ⊕ NS ⊕ H⁴, but that identification needs D^b(Coh X), Chern characters and Hirzebruch–Riemann–Roch, none of which exist in Mathlib at the pin. It is geometry, it lives in the assumption frontier, and nothing here discharges it or depends on it.

This is the same discipline LinearAlgebra/Lattice/Numerical.lean applies to Fin 2 → ℤ: every theorem below is a theorem about an arbitrary symmetric bilinear ℤ-lattice, and is true whether or not any surface exists.

Naming

expectedDim v = ⟪v, v⟫ + 2 is a definition, not the Mukai dimension theorem. The statement that a moduli space of stable objects with primitive Mukai vector v has dimension ⟪v, v⟫ + 2 is geometry and is not asserted. The name records which numerical quantity is being tracked, nothing more.

Main results

• pairing_comm — the extension is symmetric when b is.
• even_selfPairing — the extension of an even lattice is even.
• pairing_rankUnit_corankUnit — the rank/co-rank plane is a hyperbolic plane: two isotropic generators pairing to -1.

@[reducible, inline]

abbrev Mukai.MukaiLattice (N : Type u_1) : Type u_1

The underlying group of the Mukai extension of N: triples (r, c, s).

The name is suggestive of the K3 case; the module docstring records that the identification with any geometric lattice is not made here.

Equations

• Mukai.MukaiLattice N = (ℤ × N × ℤ)

Bilinearity

Proved directly from the definition rather than inherited, so that every downstream rewrite has a named lemma to hit.

linter.unusedSimpArgs is disabled for this section, and the suppression is load-bearing rather than cosmetic. It flags LinearMap.add_apply and its siblings in the four left-hand lemmas as unused; removing them on that advice makes all four fail. The reason is asymmetry in the definition: on the right, b u.2.1 (v.2.1 + w.2.1) is closed by map_add on the applied form alone, whereas on the left b (u.2.1 + v.2.1) w.2.1 first becomes (b u.2.1 + b v.2.1) w.2.1 and needs LinearMap.add_apply to reach a goal ring can see. The linter judges the simp only call in isolation and does not know a ring follows it. Re-check this if the pin moves; do not delete the arguments on the warning alone.

theorem Mukai.pairing_add_left {N : Type u_1} [AddCommGroup N] (b : N →ₗ[ℤ] N →ₗ[ℤ] ℤ) (u v w : MukaiLattice N) : pairing b (u + v) w = pairing b u w + pairing b v w

theorem Mukai.pairing_add_right {N : Type u_1} [AddCommGroup N] (b : N →ₗ[ℤ] N →ₗ[ℤ] ℤ) (u v w : MukaiLattice N) : pairing b u (v + w) = pairing b u v + pairing b u w

theorem Mukai.pairing_smul_left {N : Type u_1} [AddCommGroup N] (b : N →ₗ[ℤ] N →ₗ[ℤ] ℤ) (a : ℤ) (v w : MukaiLattice N) : pairing b (a • v) w = a * pairing b v w

theorem Mukai.pairing_smul_right {N : Type u_1} [AddCommGroup N] (b : N →ₗ[ℤ] N →ₗ[ℤ] ℤ) (a : ℤ) (v w : MukaiLattice N) : pairing b v (a • w) = a * pairing b v w

theorem Mukai.pairing_neg_left {N : Type u_1} [AddCommGroup N] (b : N →ₗ[ℤ] N →ₗ[ℤ] ℤ) (v w : MukaiLattice N) : pairing b (-v) w = -pairing b v w

theorem Mukai.pairing_neg_right {N : Type u_1} [AddCommGroup N] (b : N →ₗ[ℤ] N →ₗ[ℤ] ℤ) (v w : MukaiLattice N) : pairing b v (-w) = -pairing b v w

theorem Mukai.pairing_sub_left {N : Type u_1} [AddCommGroup N] (b : N →ₗ[ℤ] N →ₗ[ℤ] ℤ) (u v w : MukaiLattice N) : pairing b (u - v) w = pairing b u w - pairing b v w

theorem Mukai.pairing_sub_right {N : Type u_1} [AddCommGroup N] (b : N →ₗ[ℤ] N →ₗ[ℤ] ℤ) (u v w : MukaiLattice N) : pairing b u (v - w) = pairing b u v - pairing b u w

@[simp]

theorem Mukai.pairing_zero_left {N : Type u_1} [AddCommGroup N] (b : N →ₗ[ℤ] N →ₗ[ℤ] ℤ) (w : MukaiLattice N) : pairing b 0 w = 0

@[simp]

theorem Mukai.pairing_zero_right {N : Type u_1} [AddCommGroup N] (b : N →ₗ[ℤ] N →ₗ[ℤ] ℤ) (v : MukaiLattice N) : pairing b v 0 = 0

The quadratic refinement, over ℤ

selfPairing itself is generic and lives above; these are the ℤ-lattice facts about it.

theorem Mukai.selfPairing_smul {N : Type u_1} [AddCommGroup N] (b : N →ₗ[ℤ] N →ₗ[ℤ] ℤ) (a : ℤ) (v : MukaiLattice N) : selfPairing b (a • v) = a ^ 2 * selfPairing b v

@[simp]

theorem Mukai.selfPairing_zero {N : Type u_1} [AddCommGroup N] (b : N →ₗ[ℤ] N →ₗ[ℤ] ℤ) : selfPairing b 0 = 0

theorem Mukai.selfPairing_neg {N : Type u_1} [AddCommGroup N] (b : N →ₗ[ℤ] N →ₗ[ℤ] ℤ) (v : MukaiLattice N) : selfPairing b (-v) = selfPairing b v

theorem Mukai.even_selfPairing {N : Type u_1} [AddCommGroup N] (b : N →ₗ[ℤ] N →ₗ[ℤ] ℤ) (heven : ∀ (x : N), Even ((b x) x)) (v : MukaiLattice N) : Even (selfPairing b v)

The Mukai extension of an even lattice is even.

For a K3 surface the intersection form on NS(X) is even, and this is the lattice-theoretic reason ⟪v, v⟫ is always even there. The hypothesis is stated, never assumed from geometry.

Distinguished classes

IsSpherical and IsIsotropic are the two numerical conditions the wall-classification literature is organised around. Both are conditions on a lattice vector alone.

def Mukai.IsSpherical {N : Type u_1} [AddCommGroup N] (b : N →ₗ[ℤ] N →ₗ[ℤ] ℤ) (v : MukaiLattice N) : Prop

⟪v, v⟫ = -2. In the K3 case these are the classes of spherical objects; here it is a numerical condition and nothing more.

Equations

• Mukai.IsSpherical b v = (Mukai.selfPairing b v = -2)

def Mukai.IsIsotropic {N : Type u_1} [AddCommGroup N] (b : N →ₗ[ℤ] N →ₗ[ℤ] ℤ) (v : MukaiLattice N) : Prop

⟪v, v⟫ = 0.

Equations

• Mukai.IsIsotropic b v = (Mukai.selfPairing b v = 0)

theorem Mukai.isSpherical_iff {N : Type u_1} [AddCommGroup N] (b : N →ₗ[ℤ] N →ₗ[ℤ] ℤ) (v : MukaiLattice N) : IsSpherical b v ↔ selfPairing b v = -2

theorem Mukai.isIsotropic_iff {N : Type u_1} [AddCommGroup N] (b : N →ₗ[ℤ] N →ₗ[ℤ] ℤ) (v : MukaiLattice N) : IsIsotropic b v ↔ selfPairing b v = 0

theorem Mukai.IsSpherical.neg {N : Type u_1} [AddCommGroup N] (b : N →ₗ[ℤ] N →ₗ[ℤ] ℤ) {v : MukaiLattice N} (h : IsSpherical b v) : IsSpherical b (-v)

theorem Mukai.IsIsotropic.neg {N : Type u_1} [AddCommGroup N] (b : N →ₗ[ℤ] N →ₗ[ℤ] ℤ) {v : MukaiLattice N} (h : IsIsotropic b v) : IsIsotropic b (-v)

theorem Mukai.not_isSpherical_and_isIsotropic {N : Type u_1} [AddCommGroup N] (b : N →ₗ[ℤ] N →ₗ[ℤ] ℤ) (v : MukaiLattice N) : ¬(IsSpherical b v ∧ IsIsotropic b v)

def Mukai.expectedDim {N : Type u_1} [AddCommGroup N] (b : N →ₗ[ℤ] N →ₗ[ℤ] ℤ) (v : MukaiLattice N) : ℤ

The numerical quantity ⟪v, v⟫ + 2.

A definition, not the Mukai dimension theorem. See the module docstring.

Equations

• Mukai.expectedDim b v = Mukai.selfPairing b v + 2

theorem Mukai.expectedDim_eq_zero_iff {N : Type u_1} [AddCommGroup N] (b : N →ₗ[ℤ] N →ₗ[ℤ] ℤ) (v : MukaiLattice N) : expectedDim b v = 0 ↔ IsSpherical b v

theorem Mukai.expectedDim_eq_two_iff {N : Type u_1} [AddCommGroup N] (b : N →ₗ[ℤ] N →ₗ[ℤ] ℤ) (v : MukaiLattice N) : expectedDim b v = 2 ↔ IsIsotropic b v

The hyperbolic plane in the rank / co-rank coordinates

The two outer summands span a copy of the hyperbolic plane U, independently of b. This is the lattice-theoretic content of "the Mukai lattice contains H⁰ ⊕ H⁴".

def Mukai.rankUnit {N : Type u_1} [AddCommGroup N] : MukaiLattice N

(1, 0, 0).

Equations

• Mukai.rankUnit = (1, 0, 0)

def Mukai.corankUnit {N : Type u_1} [AddCommGroup N] : MukaiLattice N

(0, 0, 1).

Equations

• Mukai.corankUnit = (0, 0, 1)

theorem Mukai.pairing_outer {N : Type u_1} [AddCommGroup N] (b : N →ₗ[ℤ] N →ₗ[ℤ] ℤ) (r s r' s' : ℤ) : pairing b (r, 0, s) (r', 0, s') = -(r * s' + r' * s)

Not @[simp]: pairing_mk together with map_zero already puts the left-hand side in normal form, and marking this would fail simpNF. It is kept as a readable statement of the outer-plane pairing.

theorem Mukai.isIsotropic_rankUnit {N : Type u_1} [AddCommGroup N] (b : N →ₗ[ℤ] N →ₗ[ℤ] ℤ) : IsIsotropic b rankUnit

theorem Mukai.isIsotropic_corankUnit {N : Type u_1} [AddCommGroup N] (b : N →ₗ[ℤ] N →ₗ[ℤ] ℤ) : IsIsotropic b corankUnit

theorem Mukai.pairing_rankUnit_corankUnit {N : Type u_1} [AddCommGroup N] (b : N →ₗ[ℤ] N →ₗ[ℤ] ℤ) : pairing b rankUnit corankUnit = -1

The two isotropic generators pair to -1: the outer plane is hyperbolic.

Bundled form

The pairing packaged as a ℤ-bilinear map, for downstream use with Mathlib's bilinear/quadratic-form API.

def Mukai.pairingBilin {N : Type u_1} [AddCommGroup N] (b : N →ₗ[ℤ] N →ₗ[ℤ] ℤ) : MukaiLattice N →ₗ[ℤ] MukaiLattice N →ₗ[ℤ] ℤ

The Mukai pairing as a bundled bilinear map.

Equations

• Mukai.pairingBilin b = LinearMap.mk₂ ℤ (Mukai.pairing b) ⋯ ⋯ ⋯ ⋯

@[simp]

theorem Mukai.pairingBilin_apply {N : Type u_1} [AddCommGroup N] (b : N →ₗ[ℤ] N →ₗ[ℤ] ℤ) (v w : MukaiLattice N) : ((pairingBilin b) v) w = pairing b v w