Discriminant bilinear modules of integral lattices

For a nondegenerate integral lattice L, this file equips its finite discriminant group Lᵛ / L with the pairing

b_L (x + L) (y + L) = L.form x y mod ℤ.

Membership in Lᵛ makes the form change by an integer when either argument is translated by a vector of L; integrality embeds L in Lᵛ so that the quotient can be formed. Double duality for the embedded carrier proves that the resulting finite bilinear module is nondegenerate: a dual vector pairing integrally with every dual vector already lies in L. Integral-lattice isometries induce isometries of these discriminant bilinear modules.

The pairing b_L is B(x, y) mod ℤ; the even-lattice refinement q_L(x) = B(x, x) / 2 mod ℤ (the half-norm convention) will have this pairing as its polar form.

Main declarations

• TauCeti.IntegralLattice.discriminantPairing: the descended ℚ/ℤ-valued pairing.
• TauCeti.IntegralLattice.discriminantBilinearModule: the packaged finite bilinear module.
• TauCeti.IntegralLattice.isNondegenerate_discriminantBilinearModule: nondegeneracy of the discriminant pairing.
• TauCeti.IntegralLattice.Isometry.discriminantBilinearIsometry: functoriality under lattice isometry.

References

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

noncomputable def TauCeti.IntegralLattice.discriminantPairing {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) : L.DiscriminantGroup →ₗ[ℤ] L.DiscriminantGroup →ₗ[ℤ] AddCircle 1

The discriminant pairing b_L : A_L × A_L → ℚ/ℤ of an integral lattice.

Equations

• L.discriminantPairing = LinearMap.IsRefl.liftQ₂ (TauCeti.IntegralLattice.dualCarrierFormModOne✝ L) L.carrierInDual ⋯ ⋯

@[simp]

theorem TauCeti.IntegralLattice.discriminantPairing_mk {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) (x y : ↥L.dualCarrier) : (L.discriminantPairing (Submodule.Quotient.mk x)) (Submodule.Quotient.mk y) = ↑((L.form ↑x) ↑y)

On representatives, the discriminant pairing is the ambient rational form modulo ℤ.

theorem TauCeti.IntegralLattice.discriminantPairing_mk_eq_zero_iff {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) (x y : ↥L.dualCarrier) : (L.discriminantPairing (Submodule.Quotient.mk x)) (Submodule.Quotient.mk y) = 0 ↔ (L.form ↑x) ↑y ∈ 1

The discriminant pairing of two representatives vanishes exactly when the ambient form pairs them integrally.

theorem TauCeti.IntegralLattice.discriminantPairing_comm {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) (x y : L.DiscriminantGroup) : (L.discriminantPairing x) y = (L.discriminantPairing y) x

The discriminant pairing is symmetric.

noncomputable def TauCeti.IntegralLattice.discriminantBilinearModule {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) [L.IsNondegenerate] : FiniteBilinearModule

The finite discriminant group equipped with its canonical symmetric bilinear pairing.

The package is exposed so its dependent carrier and group-instance projections reduce to those of DiscriminantGroup; its pairing should be used through the characteristic theorem below.

Equations

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

@[simp]

theorem TauCeti.IntegralLattice.discriminantBilinearModule_pairing {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) [L.IsNondegenerate] (x y : L.DiscriminantGroup) : (L.discriminantBilinearModule.pairing x) y = (L.discriminantPairing x) y

The pairing of the discriminant bilinear module is the descended discriminant pairing.

theorem TauCeti.IntegralLattice.isNondegenerate_discriminantBilinearModule {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) [L.IsNondegenerate] : L.discriminantBilinearModule.IsNondegenerate

The discriminant bilinear module of a nondegenerate integral lattice is nondegenerate.

noncomputable def TauCeti.IntegralLattice.Isometry.discriminantBilinearIsometry {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] : L.discriminantBilinearModule.Isometry M.discriminantBilinearModule

An integral-lattice isometry induces an isometry of discriminant bilinear modules.

Equations

• e.discriminantBilinearIsometry = { toAddEquiv := e.discriminantGroupEquiv.toAddEquiv, map_pairing' := ⋯ }

@[simp]

theorem TauCeti.IntegralLattice.Isometry.discriminantBilinearIsometry_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] : e.discriminantBilinearIsometry.toAddEquiv = e.discriminantGroupEquiv.toAddEquiv

The underlying additive equivalence of the induced discriminant isometry is the one already carried by discriminantGroupEquiv.

@[simp]

theorem TauCeti.IntegralLattice.Isometry.discriminantBilinearIsometry_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] (x : L.DiscriminantGroup) : e.discriminantBilinearIsometry x = e.discriminantGroupEquiv x

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

theorem TauCeti.IntegralLattice.Isometry.discriminantBilinearIsometry_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] (x : ↥L.dualCarrier) : e.discriminantBilinearIsometry (Submodule.Quotient.mk x) = Submodule.Quotient.mk (e.dualCarrierEquiv x)

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

@[simp]

theorem TauCeti.IntegralLattice.Isometry.discriminantBilinearIsometry_refl {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) [L.IsNondegenerate] : (refl L).discriminantBilinearIsometry = FiniteBilinearModule.Isometry.refl L.discriminantBilinearModule

The identity lattice isometry induces the identity discriminant-bilinear isometry.

@[simp]

theorem TauCeti.IntegralLattice.Isometry.discriminantBilinearIsometry_symm {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] : e.symm.discriminantBilinearIsometry = e.discriminantBilinearIsometry.symm

Passing to the inverse lattice isometry passes to the inverse discriminant-bilinear isometry.

@[simp]

theorem TauCeti.IntegralLattice.Isometry.discriminantBilinearIsometry_symm_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] (y : ↥M.dualCarrier) : e.discriminantBilinearIsometry.symm (Submodule.Quotient.mk y) = Submodule.Quotient.mk (e.symm.dualCarrierEquiv y)

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

@[simp]

theorem TauCeti.IntegralLattice.Isometry.discriminantBilinearIsometry_trans {V : Type u} [AddCommGroup V] [Module ℚ V] {W : Type v} {U : Type w} [AddCommGroup W] [Module ℚ W] [AddCommGroup U] [Module ℚ U] {L : IntegralLattice V} {M : IntegralLattice W} {N : IntegralLattice U} (e : L.Isometry M) (f : M.Isometry N) [L.IsNondegenerate] [M.IsNondegenerate] [N.IsNondegenerate] : (e.trans f).discriminantBilinearIsometry = e.discriminantBilinearIsometry.trans f.discriminantBilinearIsometry

The discriminant-bilinear isometry induced by a composite is the composite of the induced isometries.