The rational model of an integral lattice in a real inner product space

Let L be a full integral lattice in a finite-dimensional real inner product space E. Its inner product is an integer-valued symmetric form ZLattice.IsIntegral.integralForm on L, and TauCeti.IntegralLattice.ofIntegralForm rationalizes it to an integral lattice in the rational vector space ℚ ⊗[ℤ] L. This is the rational model ZLattice.ratModel of L: an integral lattice in the sense of TauCeti.IntegralLattice, whose carrier is the image 1 ⊗ L of L.

The map ZLattice.ratModelMap L : ℚ ⊗[ℤ] L → E, q ⊗ x ↦ q • x, is injective, carries the rational form to the inner product of E, and carries the carrier of the rational model exactly onto L. Consequently the rational model is positive definite and nondegenerate, it has the rank of L, it is even exactly when L is, and it is unimodular exactly when L is; its determinant and its discriminant are both the determinant ZLattice.det L = covolume L ^ 2 of L.

The bridge extends to duals. The map ratModelMap carries the dual carrier of the rational model onto the dual lattice L^∨ (ZLattice.mem_ratModel_dualCarrier_iff; surjectivity uses that L has finite index in L^∨), which identifies the two duals (ZLattice.ratModelDualEquiv) and the two discriminant groups (ZLattice.ratModelDiscriminantGroupEquiv). Under this identification the discriminant pairing of the rational model is the inner product ⟪x, y⟫ of x, y ∈ L^∨ modulo ℤ, and, for even L, its discriminant quadratic map is the half-norm ‖x‖² / 2 modulo ℤ.

These comparisons let the arithmetic theory of rational integral lattices (discriminant forms, isometry classes, genus invariants) be applied to lattices in Euclidean space, such as those whose theta series are studied analytically.

Main definitions

• ZLattice.ratModelMap L: the map ℚ ⊗[ℤ] L → E, q ⊗ x ↦ q • x.
• ZLattice.ratModel hL: the rational model of an integral full lattice L.
• ZLattice.ratModelCarrierEquiv hL: the identification of L with the carrier of its rational model.
• ZLattice.ratModelDualEquiv hL: the identification of L^∨ with the dual carrier of the rational model.
• ZLattice.ratModelDiscriminantGroupEquiv hL: the identification of the discriminant group L^∨ ⧸ L with the discriminant group of the rational model.

Main results

• ZLattice.ratModelMap_injective: the map ℚ ⊗[ℤ] L → E is injective.
• ZLattice.ratModel_form_cast: the rational form is the inner product of E.
• ZLattice.mem_ratModel_carrier_iff: the carrier of the rational model is the preimage of L.
• ZLattice.isPosDef_ratModel, ZLattice.instIsNondegenerateRatModel: the rational model is positive definite and nondegenerate.
• ZLattice.finrank_ratModel, ZLattice.isEven_ratModel_iff, ZLattice.isUnimodular_ratModel_iff: rank, evenness and unimodularity agree.
• ZLattice.determinant_ratModel, ZLattice.discriminant_ratModel, ZLattice.IsIntegral.determinant_ratModel_eq_card_discriminantGroup: the determinant and the discriminant of the rational model are ZLattice.det L = |L^∨ ⧸ L|.
• ZLattice.mem_ratModel_dualCarrier_iff, ZLattice.exists_ratModelMap_eq_of_mem_dual: the dual carrier of the rational model is the preimage of L^∨, and ratModelMap maps it onto L^∨.
• ZLattice.discriminantPairing_ratModelDiscriminantGroupEquiv_mk_eq_coe_iff, ZLattice.discriminantQuadraticMap_ratModelDiscriminantGroupEquiv_mk_eq_coe_iff: the discriminant pairing and quadratic map of the rational model are ⟪x, y⟫ and ‖x‖² / 2 modulo ℤ, computed on representatives in L^∨.

Implementation notes

The space E carries no ℚ-module structure of its own, so ratModelMap is stated as a ℤ-linear map. Inside this file the ℚ-module structure restricted from ℝ is a local instance, used to build ratModelMap from LinearMap.liftBaseChange and to prove it injective.

References

• W. Ebeling, Lattices and Codes, Chapter 1.
• @sqrt-of-2, Tau Ceti PR #20950, an earlier formalization of this rational model whose approach is adapted here.

@[instance_reducible]

noncomputable def ZLattice.moduleRat {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] : Module ℚ E

Rational scalars act on E through their embedding into the real scalars.

theorem ZLattice.isScalarTower_rat_real {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] : IsScalarTower ℚ ℝ E

The restricted rational action is compatible with the real action.

noncomputable def ZLattice.ratModelMap {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (L : Submodule ℤ E) : TensorProduct ℤ ℚ ↥L →ₗ[ℤ] E

The canonical map ℚ ⊗[ℤ] L → E, q ⊗ x ↦ q • x, from the scalar extension of a lattice to its ambient real space.

@[simp]

theorem ZLattice.ratModelMap_tmul {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (L : Submodule ℤ E) (q : ℚ) (x : ↥L) : (ratModelMap L) (q ⊗ₜ[ℤ] x) = ↑q • ↑x

The map ratModelMap L sends a pure tensor q ⊗ x to the real multiple q • x.

theorem ZLattice.ratModelMap_injective {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {L : Submodule ℤ E} : Function.Injective ⇑(ratModelMap L)

The canonical map ℚ ⊗[ℤ] L → E is injective.

noncomputable def ZLattice.ratModel {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {L : Submodule ℤ E} [FiniteDimensional ℝ E] [DiscreteTopology ↥L] [IsZLattice ℝ L] (hL : IsIntegral L) : TauCeti.IntegralLattice (TensorProduct ℤ ℚ ↥L)

The rational model of an integral full lattice L: the integral lattice in ℚ ⊗[ℤ] L obtained by rationalizing the integer-valued inner product of L.

@[simp]

theorem ZLattice.ratModel_form {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {L : Submodule ℤ E} [FiniteDimensional ℝ E] [DiscreteTopology ↥L] [IsZLattice ℝ L] (hL : IsIntegral L) : (ratModel hL).form = LinearMap.BilinForm.baseChange ℚ hL.integralForm

The form of the rational model is the scalar extension of the integer-valued inner product.

theorem ZLattice.ratModel_form_cast {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {L : Submodule ℤ E} [FiniteDimensional ℝ E] [DiscreteTopology ↥L] [IsZLattice ℝ L] (hL : IsIntegral L) (x y : TensorProduct ℤ ℚ ↥L) : ↑(((ratModel hL).form x) y) = inner ℝ ((ratModelMap L) x) ((ratModelMap L) y)

The form of the rational model is the inner product of E, read through ratModelMap.

theorem ZLattice.norm_sq_ratModelMap {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {L : Submodule ℤ E} [FiniteDimensional ℝ E] [DiscreteTopology ↥L] [IsZLattice ℝ L] (hL : IsIntegral L) (x : TensorProduct ℤ ℚ ↥L) : ‖(ratModelMap L) x‖ ^ 2 = ↑((ratModel hL).norm x)

The squared real norm of a rational-model vector is its rational norm, cast to ℝ.

noncomputable def ZLattice.ratModelCarrierEquiv {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {L : Submodule ℤ E} [FiniteDimensional ℝ E] [DiscreteTopology ↥L] [IsZLattice ℝ L] (hL : IsIntegral L) : ↥L ≃ₗ[ℤ] ↥(ratModel hL).carrier

The identification of an integral full lattice L with the carrier of its rational model, x ↦ 1 ⊗ x.

@[simp]

theorem ZLattice.coe_ratModelCarrierEquiv {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {L : Submodule ℤ E} [FiniteDimensional ℝ E] [DiscreteTopology ↥L] [IsZLattice ℝ L] (hL : IsIntegral L) (x : ↥L) : ↑((ratModelCarrierEquiv hL) x) = 1 ⊗ₜ[ℤ] x

@[simp]

theorem ZLattice.ratModelCarrierEquiv_symm_tmul {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {L : Submodule ℤ E} [FiniteDimensional ℝ E] [DiscreteTopology ↥L] [IsZLattice ℝ L] (hL : IsIntegral L) (x : ↥L) (h : 1 ⊗ₜ[ℤ] x ∈ (ratModel hL).carrier) : (ratModelCarrierEquiv hL).symm ⟨1 ⊗ₜ[ℤ] x, h⟩ = x

The inverse carrier identification recovers a lattice vector from its unit pure tensor.

@[simp]

theorem ZLattice.integralForm_ratModelCarrierEquiv {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {L : Submodule ℤ E} [FiniteDimensional ℝ E] [DiscreteTopology ↥L] [IsZLattice ℝ L] (hL : IsIntegral L) (x y : ↥L) : ((ratModel hL).integralForm ((ratModelCarrierEquiv hL) x)) ((ratModelCarrierEquiv hL) y) = (hL.integralForm x) y

The carrier identification carries the integer-valued inner product of L to the integral form of the rational model.

@[simp]

theorem ZLattice.mem_ratModel_carrier_iff {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {L : Submodule ℤ E} [FiniteDimensional ℝ E] [DiscreteTopology ↥L] [IsZLattice ℝ L] (hL : IsIntegral L) (x : TensorProduct ℤ ℚ ↥L) : x ∈ (ratModel hL).carrier ↔ (ratModelMap L) x ∈ L

The carrier of the rational model is the preimage of L under ratModelMap.

theorem ZLattice.isPosDef_ratModel {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {L : Submodule ℤ E} [FiniteDimensional ℝ E] [DiscreteTopology ↥L] [IsZLattice ℝ L] (hL : IsIntegral L) : (ratModel hL).IsPosDef

The rational model of an integral full lattice is positive definite.

instance ZLattice.instIsNondegenerateRatModel {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {L : Submodule ℤ E} [FiniteDimensional ℝ E] [DiscreteTopology ↥L] [IsZLattice ℝ L] (hL : IsIntegral L) : (ratModel hL).IsNondegenerate

The rational model of an integral full lattice is nondegenerate.

@[simp]

theorem ZLattice.finrank_ratModel {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {L : Submodule ℤ E} [FiniteDimensional ℝ E] [DiscreteTopology ↥L] [IsZLattice ℝ L] (hL : IsIntegral L) : Module.finrank ℤ ↥(ratModel hL).carrier = Module.finrank ℝ E

The rank of the rational model is the rank of L, the dimension of E.

@[simp]

theorem ZLattice.isEven_ratModel_iff {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {L : Submodule ℤ E} [FiniteDimensional ℝ E] [DiscreteTopology ↥L] [IsZLattice ℝ L] (hL : IsIntegral L) : (ratModel hL).IsEven ↔ IsEven L

The rational model is even exactly when L is.

@[simp]

theorem ZLattice.determinant_ratModel {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {L : Submodule ℤ E} [FiniteDimensional ℝ E] [DiscreteTopology ↥L] [IsZLattice ℝ L] [MeasurableSpace E] [BorelSpace E] (hL : IsIntegral L) : ↑(ratModel hL).determinant = det L

The determinant of the rational model is the determinant covolume L ^ 2 of L.

@[simp]

theorem ZLattice.discriminant_ratModel {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {L : Submodule ℤ E} [FiniteDimensional ℝ E] [DiscreteTopology ↥L] [IsZLattice ℝ L] [MeasurableSpace E] [BorelSpace E] (hL : IsIntegral L) : ↑(ratModel hL).discriminant = det L

The discriminant of the rational model is the determinant covolume L ^ 2 of L.

theorem ZLattice.IsIntegral.determinant_ratModel_eq_card_discriminantGroup {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {L : Submodule ℤ E} [FiniteDimensional ℝ E] [DiscreteTopology ↥L] [IsZLattice ℝ L] (hL : IsIntegral L) : (ratModel hL).determinant = ↑(Nat.card (DiscriminantGroup L))

The determinant of the rational model of an integral full lattice is the order of its discriminant group.

theorem ZLattice.isUnimodular_ratModel_iff {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {L : Submodule ℤ E} [FiniteDimensional ℝ E] [DiscreteTopology ↥L] [IsZLattice ℝ L] (hL : IsIntegral L) : (ratModel hL).IsUnimodular ↔ IsUnimodular L

The rational model is unimodular exactly when L is.

The dual lattice and the discriminant group

@[simp]

theorem ZLattice.mem_ratModel_dualCarrier_iff {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {L : Submodule ℤ E} [FiniteDimensional ℝ E] [DiscreteTopology ↥L] [IsZLattice ℝ L] (hL : IsIntegral L) (x : TensorProduct ℤ ℚ ↥L) : x ∈ (ratModel hL).dualCarrier ↔ (ratModelMap L) x ∈ dual L

The dual carrier of the rational model is the preimage of the dual lattice L^∨ under ratModelMap.

theorem ZLattice.exists_ratModelMap_eq_of_mem_dual {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {L : Submodule ℤ E} [FiniteDimensional ℝ E] [DiscreteTopology ↥L] [IsZLattice ℝ L] (hL : IsIntegral L) {y : E} (hy : y ∈ dual L) : ∃ (x : TensorProduct ℤ ℚ ↥L), (ratModelMap L) x = y

Every vector of the dual lattice L^∨ of an integral full lattice L is in the image of ratModelMap: a multiple d • y with d ≠ 0 lies in L, since L^∨ ⧸ L is finite.

noncomputable def ZLattice.ratModelDualEquiv {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {L : Submodule ℤ E} [FiniteDimensional ℝ E] [DiscreteTopology ↥L] [IsZLattice ℝ L] (hL : IsIntegral L) : ↥(dual L) ≃ₗ[ℤ] ↥(ratModel hL).dualCarrier

The identification of the dual lattice L^∨ of an integral full lattice L with the dual carrier of its rational model; it is inverse to ratModelMap.

@[simp]

theorem ZLattice.ratModelMap_ratModelDualEquiv {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {L : Submodule ℤ E} [FiniteDimensional ℝ E] [DiscreteTopology ↥L] [IsZLattice ℝ L] (hL : IsIntegral L) (x : ↥(dual L)) : (ratModelMap L) ↑((ratModelDualEquiv hL) x) = ↑x

ratModelMap recovers a dual vector from its image under ratModelDualEquiv.

@[simp]

theorem ZLattice.coe_ratModelDualEquiv_symm {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {L : Submodule ℤ E} [FiniteDimensional ℝ E] [DiscreteTopology ↥L] [IsZLattice ℝ L] (hL : IsIntegral L) (x : ↥(ratModel hL).dualCarrier) : ↑((ratModelDualEquiv hL).symm x) = (ratModelMap L) ↑x

The inverse of ratModelDualEquiv is ratModelMap.

theorem ZLattice.ratModel_form_ratModelDualEquiv_cast {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {L : Submodule ℤ E} [FiniteDimensional ℝ E] [DiscreteTopology ↥L] [IsZLattice ℝ L] (hL : IsIntegral L) (x y : ↥(dual L)) : ↑(((ratModel hL).form ↑((ratModelDualEquiv hL) x)) ↑((ratModelDualEquiv hL) y)) = inner ℝ ↑x ↑y

The form of the rational model on the dual carrier is the inner product of L^∨.

theorem ZLattice.map_ratModelDualEquiv_submoduleOf {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {L : Submodule ℤ E} [FiniteDimensional ℝ E] [DiscreteTopology ↥L] [IsZLattice ℝ L] (hL : IsIntegral L) : Submodule.map (↑(ratModelDualEquiv hL)) (L.submoduleOf (dual L)) = (ratModel hL).carrierInDual

ratModelDualEquiv carries L, seen inside L^∨, onto the carrier of the rational model seen inside its dual carrier.

noncomputable def ZLattice.ratModelDiscriminantGroupEquiv {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {L : Submodule ℤ E} [FiniteDimensional ℝ E] [DiscreteTopology ↥L] [IsZLattice ℝ L] (hL : IsIntegral L) : DiscriminantGroup L ≃ₗ[ℤ] (ratModel hL).DiscriminantGroup

The identification of the discriminant group L^∨ ⧸ L of an integral full lattice L with the discriminant group of its rational model, induced by ratModelDualEquiv.

@[simp]

theorem ZLattice.ratModelDiscriminantGroupEquiv_mk {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {L : Submodule ℤ E} [FiniteDimensional ℝ E] [DiscreteTopology ↥L] [IsZLattice ℝ L] (hL : IsIntegral L) (x : ↥(dual L)) : (ratModelDiscriminantGroupEquiv hL) (Submodule.Quotient.mk x) = Submodule.Quotient.mk ((ratModelDualEquiv hL) x)

On representatives, ratModelDiscriminantGroupEquiv is ratModelDualEquiv.

theorem ZLattice.discriminantPairing_ratModelDiscriminantGroupEquiv_mk_eq_coe_iff {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {L : Submodule ℤ E} [FiniteDimensional ℝ E] [DiscreteTopology ↥L] [IsZLattice ℝ L] (hL : IsIntegral L) (x y : ↥(dual L)) (q : ℚ) : ((ratModel hL).discriminantPairing ((ratModelDiscriminantGroupEquiv hL) (Submodule.Quotient.mk x))) ((ratModelDiscriminantGroupEquiv hL) (Submodule.Quotient.mk y)) = ↑q ↔ ∃ (m : ℤ), inner ℝ ↑x ↑y = ↑q + ↑m

The discriminant pairing of the rational model, read on the classes of x, y ∈ L^∨, is the inner product ⟪x, y⟫ modulo ℤ: it takes the value q exactly when ⟪x, y⟫ - q ∈ ℤ.

theorem ZLattice.discriminantQuadraticMap_ratModelDiscriminantGroupEquiv_mk_eq_coe_iff {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {L : Submodule ℤ E} [FiniteDimensional ℝ E] [DiscreteTopology ↥L] [IsZLattice ℝ L] (hL : IsIntegral L) (hE : IsEven L) (x : ↥(dual L)) (q : ℚ) : ((ratModel hL).discriminantQuadraticMap ⋯) ((ratModelDiscriminantGroupEquiv hL) (Submodule.Quotient.mk x)) = ↑q ↔ ∃ (m : ℤ), ‖↑x‖ ^ 2 / 2 = ↑q + ↑m

For an even lattice L, the discriminant quadratic map of the rational model, read on the class of x ∈ L^∨, is the half-norm ‖x‖² / 2 modulo ℤ: it takes the value q exactly when ‖x‖² / 2 - q ∈ ℤ.