The numerical Grothendieck lattice

The numerical Grothendieck group is the quotient by the radical of the Euler pairing. This file makes that construction explicit from NumericalVarietyData.chi₂ and records the precise finiteness input needed before the quotient is a lattice.

The Euler pairing supplied by NumericalVarietyData is ℚ-valued. Consequently the descended pairing below is also ℚ-valued; no integrality statement is silently assumed. The integral object is its underlying finite free ℤ-module.

Main results

• NumericalVarietyData.leftRadical and NumericalVarietyData.rightRadical are the two Euler radicals.
• NumericalVarietyData.leftRadical_eq_rightRadical identifies them when the Euler form is symmetric.
• NumericalVarietyData.NumericalQuotient is the quotient by the radical.
• NumericalVarietyData.numericalPairing is the descended, nondegenerate pairing.
• NumericalQuotient is finitely generated over ℤ whenever N is (instFiniteNumericalQuotient, from Module.Finite.quotient), and free whenever it is also torsion-free, by Mathlib's instance Module.free_of_finite_type_torsion_free'. The lattice structure is therefore Mathlib's [Module.Finite ℤ _] [Module.Free ℤ _]; the repository no longer carries a class for it.
• K3.numericalPairing_mk_eq_neg_mukaiPairing fixes the K3 sign convention.

noncomputable def AlgebraicGeometry.Numerical.NumericalVarietyData.eulerPairingRow {n : ℕ} {A : Type u} {N : Type v} [CommRing A] [Algebra ℚ A] [AddCommGroup N] (V : NumericalVarietyData n A N) (E : N) : N →+ ℚ

The Euler pairing with its second argument packaged as an additive homomorphism.

Equations

• V.eulerPairingRow E = AddMonoidHom.mk' (V.chi₂ E) ⋯

noncomputable def AlgebraicGeometry.Numerical.NumericalVarietyData.eulerPairing {n : ℕ} {A : Type u} {N : Type v} [CommRing A] [Algebra ℚ A] [AddCommGroup N] (V : NumericalVarietyData n A N) : N →+ N →+ ℚ

The Euler pairing as a biadditive homomorphism N →+ (N →+ ℚ).

Equations

• V.eulerPairing = AddMonoidHom.mk' V.eulerPairingRow ⋯

noncomputable def AlgebraicGeometry.Numerical.NumericalVarietyData.eulerPairingFlip {n : ℕ} {A : Type u} {N : Type v} [CommRing A] [Algebra ℚ A] [AddCommGroup N] (V : NumericalVarietyData n A N) : N →+ N →+ ℚ

The transposed Euler pairing as a biadditive homomorphism.

Equations

• V.eulerPairingFlip = AddMonoidHom.mk' (fun (F : N) => AddMonoidHom.mk' (fun (E : N) => V.chi₂ E F) ⋯) ⋯

@[simp]

theorem AlgebraicGeometry.Numerical.NumericalVarietyData.eulerPairing_apply {n : ℕ} {A : Type u} {N : Type v} [CommRing A] [Algebra ℚ A] [AddCommGroup N] (V : NumericalVarietyData n A N) (E F : N) : (V.eulerPairing E) F = V.chi₂ E F

Unbundling eulerPairing recovers the original numerical Euler form chi₂.

@[simp]

theorem AlgebraicGeometry.Numerical.NumericalVarietyData.eulerPairingFlip_apply {n : ℕ} {A : Type u} {N : Type v} [CommRing A] [Algebra ℚ A] [AddCommGroup N] (V : NumericalVarietyData n A N) (E F : N) : (V.eulerPairingFlip E) F = V.chi₂ F E

noncomputable def AlgebraicGeometry.Numerical.NumericalVarietyData.leftRadical {n : ℕ} {A : Type u} {N : Type v} [CommRing A] [Algebra ℚ A] [AddCommGroup N] (V : NumericalVarietyData n A N) : Submodule ℤ N

The left radical: classes pairing to zero against every class on the right.

Equations

• V.leftRadical = AddSubgroup.toIntSubmodule V.eulerPairing.ker

noncomputable def AlgebraicGeometry.Numerical.NumericalVarietyData.rightRadical {n : ℕ} {A : Type u} {N : Type v} [CommRing A] [Algebra ℚ A] [AddCommGroup N] (V : NumericalVarietyData n A N) : Submodule ℤ N

The right radical: classes pairing to zero against every class on the left.

Equations

• V.rightRadical = AddSubgroup.toIntSubmodule V.eulerPairingFlip.ker

theorem AlgebraicGeometry.Numerical.NumericalVarietyData.mem_leftRadical_iff {n : ℕ} {A : Type u} {N : Type v} [CommRing A] [Algebra ℚ A] [AddCommGroup N] (V : NumericalVarietyData n A N) (E : N) : E ∈ V.leftRadical ↔ ∀ (F : N), V.chi₂ E F = 0

Membership in the left radical is pointwise vanishing of the Euler pairing in the second argument.

theorem AlgebraicGeometry.Numerical.NumericalVarietyData.mem_rightRadical_iff {n : ℕ} {A : Type u} {N : Type v} [CommRing A] [Algebra ℚ A] [AddCommGroup N] (V : NumericalVarietyData n A N) (F : N) : F ∈ V.rightRadical ↔ ∀ (E : N), V.chi₂ E F = 0

Membership in the right radical is pointwise vanishing of the Euler pairing in the first argument.

def AlgebraicGeometry.Numerical.NumericalVarietyData.IsEulerPairingSymmetric {n : ℕ} {A : Type u} {N : Type v} [CommRing A] [Algebra ℚ A] [AddCommGroup N] (V : NumericalVarietyData n A N) : Prop

The symmetry hypothesis under which the project uses a single Euler radical.

Equations

• V.IsEulerPairingSymmetric = ∀ (E F : N), V.chi₂ E F = V.chi₂ F E

theorem AlgebraicGeometry.Numerical.NumericalVarietyData.leftRadical_eq_rightRadical {n : ℕ} {A : Type u} {N : Type v} [CommRing A] [Algebra ℚ A] [AddCommGroup N] (V : NumericalVarietyData n A N) (hSymm : V.IsEulerPairingSymmetric) : V.leftRadical = V.rightRadical

Symmetry turns vanishing against every right argument into vanishing against every left argument, so the two kernels used to define the numerical quotient coincide.

@[reducible, inline]

abbrev AlgebraicGeometry.Numerical.NumericalVarietyData.NumericalQuotient {n : ℕ} {A : Type u} {N : Type v} [CommRing A] [Algebra ℚ A] [AddCommGroup N] (V : NumericalVarietyData n A N) : Type v

The numerical Grothendieck quotient by the left Euler radical.

Under IsEulerPairingSymmetric, leftRadical_eq_rightRadical shows that this is equivalently the quotient by the right radical.

Equations

• V.NumericalQuotient = (N ⧸ V.leftRadical)

noncomputable def AlgebraicGeometry.Numerical.NumericalVarietyData.eulerPairingDescendRight {n : ℕ} {A : Type u} {N : Type v} [CommRing A] [Algebra ℚ A] [AddCommGroup N] (V : NumericalVarietyData n A N) (hSymm : V.IsEulerPairingSymmetric) (E : N) : V.NumericalQuotient →+ ℚ

Descend the right argument of the Euler pairing to the numerical quotient.

Equations

• V.eulerPairingDescendRight hSymm E = QuotientAddGroup.lift V.leftRadical.toAddSubgroup (V.eulerPairingRow E) ⋯

@[simp]

theorem AlgebraicGeometry.Numerical.NumericalVarietyData.eulerPairingDescendRight_mk {n : ℕ} {A : Type u} {N : Type v} [CommRing A] [Algebra ℚ A] [AddCommGroup N] (V : NumericalVarietyData n A N) (hSymm : V.IsEulerPairingSymmetric) (E F : N) : (V.eulerPairingDescendRight hSymm E) (Submodule.Quotient.mk F) = V.chi₂ E F

Evaluating the one-sided descent on a quotient representative recovers chi₂.

noncomputable def AlgebraicGeometry.Numerical.NumericalVarietyData.eulerPairingToQuotient {n : ℕ} {A : Type u} {N : Type v} [CommRing A] [Algebra ℚ A] [AddCommGroup N] (V : NumericalVarietyData n A N) (hSymm : V.IsEulerPairingSymmetric) : N →+ V.NumericalQuotient →+ ℚ

The Euler pairing with its right argument descended, still additive in the left argument.

Equations

• V.eulerPairingToQuotient hSymm = AddMonoidHom.mk' (V.eulerPairingDescendRight hSymm) ⋯

@[simp]

theorem AlgebraicGeometry.Numerical.NumericalVarietyData.eulerPairingToQuotient_mk {n : ℕ} {A : Type u} {N : Type v} [CommRing A] [Algebra ℚ A] [AddCommGroup N] (V : NumericalVarietyData n A N) (hSymm : V.IsEulerPairingSymmetric) (E F : N) : ((V.eulerPairingToQuotient hSymm) E) (Submodule.Quotient.mk F) = V.chi₂ E F

The left-additive one-sided descent still evaluates to chi₂ on representatives.

noncomputable def AlgebraicGeometry.Numerical.NumericalVarietyData.numericalPairing {n : ℕ} {A : Type u} {N : Type v} [CommRing A] [Algebra ℚ A] [AddCommGroup N] (V : NumericalVarietyData n A N) (hSymm : V.IsEulerPairingSymmetric) : V.NumericalQuotient →+ V.NumericalQuotient →+ ℚ

The Euler pairing descended to the numerical quotient in both arguments.

Equations

• V.numericalPairing hSymm = QuotientAddGroup.lift V.leftRadical.toAddSubgroup (V.eulerPairingToQuotient hSymm) ⋯

@[simp]

theorem AlgebraicGeometry.Numerical.NumericalVarietyData.numericalPairing_mk {n : ℕ} {A : Type u} {N : Type v} [CommRing A] [Algebra ℚ A] [AddCommGroup N] (V : NumericalVarietyData n A N) (hSymm : V.IsEulerPairingSymmetric) (E F : N) : ((V.numericalPairing hSymm) (Submodule.Quotient.mk E)) (Submodule.Quotient.mk F) = V.chi₂ E F

The fully descended numerical pairing is computed by chi₂ on representatives.

theorem AlgebraicGeometry.Numerical.NumericalVarietyData.numericalPairing_symm {n : ℕ} {A : Type u} {N : Type v} [CommRing A] [Algebra ℚ A] [AddCommGroup N] (V : NumericalVarietyData n A N) (hSymm : V.IsEulerPairingSymmetric) (x y : V.NumericalQuotient) : ((V.numericalPairing hSymm) x) y = ((V.numericalPairing hSymm) y) x

The descended pairing remains symmetric.

theorem AlgebraicGeometry.Numerical.NumericalVarietyData.numericalPairing_left_nondegenerate {n : ℕ} {A : Type u} {N : Type v} [CommRing A] [Algebra ℚ A] [AddCommGroup N] (V : NumericalVarietyData n A N) (hSymm : V.IsEulerPairingSymmetric) (x : V.NumericalQuotient) (hx : ∀ (y : V.NumericalQuotient), ((V.numericalPairing hSymm) x) y = 0) : x = 0

The descended pairing has zero left radical, by construction.

theorem AlgebraicGeometry.Numerical.NumericalVarietyData.numericalPairing_right_nondegenerate {n : ℕ} {A : Type u} {N : Type v} [CommRing A] [Algebra ℚ A] [AddCommGroup N] (V : NumericalVarietyData n A N) (hSymm : V.IsEulerPairingSymmetric) (y : V.NumericalQuotient) (hy : ∀ (x : V.NumericalQuotient), ((V.numericalPairing hSymm) x) y = 0) : y = 0

The descended pairing has zero right radical as well.

theorem AlgebraicGeometry.Numerical.NumericalVarietyData.numericalPairing_ker_eq_bot {n : ℕ} {A : Type u} {N : Type v} [CommRing A] [Algebra ℚ A] [AddCommGroup N] (V : NumericalVarietyData n A N) (hSymm : V.IsEulerPairingSymmetric) : (V.numericalPairing hSymm).ker = ⊥

The kernel of the descended pairing is zero.

instance AlgebraicGeometry.Numerical.NumericalVarietyData.instFiniteNumericalQuotient {n : ℕ} {A : Type u} {N : Type v} [CommRing A] [Algebra ℚ A] [AddCommGroup N] (V : NumericalVarietyData n A N) [Module.Finite ℤ N] : Module.Finite ℤ V.NumericalQuotient

Finite generation passes to the numerical quotient. Stated as an instance so that consumers do not repeat the explicit letI the former numericalZLattice theorem needed to reach Module.Finite.quotient.

Torsion-freeness does not pass to an arbitrary quotient, so a consumer that needs the quotient to be free supplies [Module.IsTorsionFree ℤ (NumericalQuotient V)] and obtains Module.Free ℤ (NumericalQuotient V) from Mathlib's instance Module.free_of_finite_type_torsion_free'; a finite free ℤ-module is the lattice, and no repository class stands in for that pair of hypotheses.

theorem AlgebraicGeometry.Numerical.K3.isEulerPairingSymmetric {A : Type u} {N : Type v} [CommRing A] [Algebra ℚ A] [AddCommGroup N] (V : NumericalVarietyData 2 A N) (hK3 : IsK3 V) : V.IsEulerPairingSymmetric

A K3 Euler pairing satisfies the symmetry hypothesis used by the numerical quotient.

theorem AlgebraicGeometry.Numerical.K3.leftRadical_eq_rightRadical {A : Type u} {N : Type v} [CommRing A] [Algebra ℚ A] [AddCommGroup N] (V : NumericalVarietyData 2 A N) (hK3 : IsK3 V) : V.leftRadical = V.rightRadical

On a K3, the two Euler radicals agree.

theorem AlgebraicGeometry.Numerical.K3.numericalPairing_mk_eq_neg_mukaiPairing {A : Type u} {N : Type v} [CommRing A] [Algebra ℚ A] [AddCommGroup N] (V : NumericalVarietyData 2 A N) (hK3 : IsK3 V) (E F : N) : ((V.numericalPairing ⋯) (Submodule.Quotient.mk E)) (Submodule.Quotient.mk F) = -mukaiPairing V E F

On representatives, the numerical quotient pairing is minus the Mukai pairing.

Thus quotienting and descending preserve exactly the sign convention fixed by chi₂_eq_neg_mukaiPairing.