Discriminant quadratic modules of even integral lattices

For an even nondegenerate integral lattice L, the half-norm of a dual vector descends to its discriminant group:

q_L (x + L) = L.form x x / 2 mod Z.

Evenness is exactly what makes this independent of the representative. Indeed, translating x by a lattice vector l changes the half-norm by L.form x l + L.form l l / 2; the first term is integral because x lies in the dual lattice, and the second is integral because L is even. The polar of the descended quadratic map is the discriminant pairing b_L (x + L) (y + L) = L.form x y mod Z.

The construction uses Mathlib's QuadraticMap.lift: the half-norm first defines a quadratic map on the dual carrier, and evenness puts the original carrier in its quadratic radical. The final package reuses discriminantBilinearModule as its underlying finite bilinear module, so its nondegeneracy and its functoriality under lattice isometries are inherited from the bilinear construction.

Main declarations

• TauCeti.IntegralLattice.discriminantQuadraticMap: the descended half-norm on A_L.
• TauCeti.IntegralLattice.discriminantQuadraticModule: the packaged finite quadratic module.
• TauCeti.IntegralLattice.isNondegenerate_discriminantQuadraticModule: nondegeneracy of its polar pairing.
• TauCeti.IntegralLattice.Isometry.discriminantQuadraticIsometry: functoriality under lattice isometry.

References

• V. V. Nikulin, Integral symmetric bilinear forms and some of their applications, section 1.1.
• W. Ebeling, Lattices and Codes, Chapter 1.
• TauCetiRoadmap/IntegralLattices/README.md, Layer 3.

noncomputable def TauCeti.IntegralLattice.discriminantQuadraticMap {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) (hL : L.IsEven) : QuadraticMap ℤ L.DiscriminantGroup (AddCircle 1)

The discriminant quadratic map of an even integral lattice, in the half-norm convention.

The definition does not require nondegeneracy; that hypothesis is needed only to make the discriminant group finite and hence package it as a FiniteQuadraticModule.

Equations

• L.discriminantQuadraticMap hL = (TauCeti.IntegralLattice.dualCarrierHalfNormModOne✝ L).lift L.carrierInDual ⋯

@[simp]

theorem TauCeti.IntegralLattice.discriminantQuadraticMap_mk {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) (hL : L.IsEven) (x : ↥L.dualCarrier) : (L.discriminantQuadraticMap hL) (Submodule.Quotient.mk x) = ↑((L.form ↑x) ↑x / 2)

On a representative, the discriminant quadratic map is the ambient half-norm modulo Z.

theorem TauCeti.IntegralLattice.discriminantQuadraticMap_mk_eq_zero_iff {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) (hL : L.IsEven) (x : ↥L.dualCarrier) : (L.discriminantQuadraticMap hL) (Submodule.Quotient.mk x) = 0 ↔ ∃ (n : ℤ), (L.form ↑x) ↑x = ↑(2 * n)

The discriminant quadratic value of a representative vanishes exactly when the ambient self-pairing is twice an integer.

@[simp]

theorem TauCeti.IntegralLattice.polar_discriminantQuadraticMap {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) (hL : L.IsEven) (x y : L.DiscriminantGroup) : QuadraticMap.polar (⇑(L.discriminantQuadraticMap hL)) x y = (L.discriminantPairing x) y

The polar of the half-norm discriminant quadratic map is the discriminant pairing.

@[simp]

theorem TauCeti.IntegralLattice.polarBilin_discriminantQuadraticMap {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) (hL : L.IsEven) : (L.discriminantQuadraticMap hL).polarBilin = L.discriminantPairing

The polar bilinear map of the half-norm discriminant quadratic map is the discriminant pairing.

noncomputable def TauCeti.IntegralLattice.discriminantQuadraticModule {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) [L.IsNondegenerate] (hL : L.IsEven) : FiniteQuadraticModule

The discriminant group of an even nondegenerate integral lattice, equipped with its canonical half-norm quadratic map and discriminant polar pairing.

Equations

• L.discriminantQuadraticModule hL = { toFiniteBilinearModule := L.discriminantBilinearModule, quadratic := L.discriminantQuadraticMap hL, polar_eq_pairing' := ⋯ }

@[simp]

theorem TauCeti.IntegralLattice.discriminantQuadraticModule_quadratic {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) [L.IsNondegenerate] (hL : L.IsEven) (x : L.DiscriminantGroup) : (L.discriminantQuadraticModule hL).quadratic x = (L.discriminantQuadraticMap hL) x

The quadratic map of the discriminant quadratic module is the descended half-norm.

theorem TauCeti.IntegralLattice.discriminantQuadraticModule_toFiniteBilinearModule {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) [L.IsNondegenerate] (hL : L.IsEven) : (L.discriminantQuadraticModule hL).toFiniteBilinearModule = L.discriminantBilinearModule

The polar finite bilinear module of the discriminant quadratic module is the existing discriminant bilinear module.

theorem TauCeti.IntegralLattice.isNondegenerate_discriminantQuadraticModule {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) [L.IsNondegenerate] (hL : L.IsEven) : (L.discriminantQuadraticModule hL).IsNondegenerate

The discriminant quadratic module of an even nondegenerate lattice is nondegenerate.

noncomputable def TauCeti.IntegralLattice.Isometry.discriminantQuadraticIsometry {V : Type u} [AddCommGroup V] [Module ℚ V] {W : Type v} [AddCommGroup W] [Module ℚ W] {L : IntegralLattice V} {M : IntegralLattice W} (e : L.Isometry M) [L.IsNondegenerate] [M.IsNondegenerate] (hL : L.IsEven) : (L.discriminantQuadraticModule hL).Isometry (M.discriminantQuadraticModule ⋯)

An isometry of even nondegenerate integral lattices induces an isometry of their discriminant quadratic modules.

Equations

• e.discriminantQuadraticIsometry hL = { toLinearEquiv := e.discriminantGroupEquiv, map_app' := ⋯ }

@[simp]

theorem TauCeti.IntegralLattice.Isometry.discriminantQuadraticIsometry_toAddEquiv {V : Type u} [AddCommGroup V] [Module ℚ V] {W : Type v} [AddCommGroup W] [Module ℚ W] {L : IntegralLattice V} {M : IntegralLattice W} (e : L.Isometry M) [L.IsNondegenerate] [M.IsNondegenerate] (hL : L.IsEven) : (e.discriminantQuadraticIsometry hL).toAddEquiv = e.discriminantGroupEquiv.toAddEquiv

The underlying additive equivalence of the induced discriminant quadratic isometry is the discriminant-group equivalence.

@[simp]

theorem TauCeti.IntegralLattice.Isometry.discriminantQuadraticIsometry_apply {V : Type u} [AddCommGroup V] [Module ℚ V] {W : Type v} [AddCommGroup W] [Module ℚ W] {L : IntegralLattice V} {M : IntegralLattice W} (e : L.Isometry M) [L.IsNondegenerate] [M.IsNondegenerate] (hL : L.IsEven) (x : L.DiscriminantGroup) : (e.discriminantQuadraticIsometry hL) x = e.discriminantGroupEquiv x

The induced discriminant quadratic isometry acts through the discriminant-group equivalence.

theorem TauCeti.IntegralLattice.Isometry.discriminantQuadraticIsometry_mk {V : Type u} [AddCommGroup V] [Module ℚ V] {W : Type v} [AddCommGroup W] [Module ℚ W] {L : IntegralLattice V} {M : IntegralLattice W} (e : L.Isometry M) [L.IsNondegenerate] [M.IsNondegenerate] (hL : L.IsEven) (x : ↥L.dualCarrier) : (e.discriminantQuadraticIsometry hL) (Submodule.Quotient.mk x) = Submodule.Quotient.mk (e.dualCarrierEquiv x)

The induced discriminant quadratic isometry maps a representative through the dual-carrier equivalence.

@[simp]

theorem TauCeti.IntegralLattice.Isometry.discriminantQuadraticIsometry_toFiniteBilinearModule {V : Type u} [AddCommGroup V] [Module ℚ V] {W : Type v} [AddCommGroup W] [Module ℚ W] {L : IntegralLattice V} {M : IntegralLattice W} (e : L.Isometry M) [L.IsNondegenerate] [M.IsNondegenerate] (hL : L.IsEven) : (e.discriminantQuadraticIsometry hL).toFiniteBilinearModule = e.discriminantBilinearIsometry

Forgetting the quadratic map from the induced isometry recovers the discriminant bilinear isometry.