Integral, even and unimodular lattices in a real inner product space

A ℤ-submodule L of a real inner product space E is

• integral (ZLattice.IsIntegral) if ⟪x, y⟫ ∈ ℤ for all x, y ∈ L, that is L ≤ L^∨, where L^∨ = ZLattice.dual L is the dual lattice;
• even (ZLattice.IsEven) if ‖x‖² ∈ 2ℤ for every x ∈ L;
• unimodular (ZLattice.IsUnimodular) if it is self-dual, L = L^∨.

The inner product is positive definite, so these are the classical notions for positive-definite lattices; no definiteness hypothesis appears. Evenness only involves the norm, so it is defined for ℤ-submodules of any seminormed additive commutative group. Integrality is recorded as the inclusion L ≤ dual L, with the elementwise form as ZLattice.isIntegral_iff.

In a real inner product space, an even lattice is integral, by polarization: 2⟪x, y⟫ = ‖x + y‖² - ‖x‖² - ‖y‖² (ZLattice.IsEven.isIntegral). The converse fails: ℤ ⊆ ℝ is unimodular, hence integral, but not even (ZLattice.not_isEven_span_one), while √2 ℤ ⊆ ℝ is even (ZLattice.isEven_span_sqrt_two). More generally the ℤ-span of an orthonormal basis, the lattice ℤⁿ ⊆ ℝⁿ, is unimodular (ZLattice.isUnimodular_span_orthonormalBasis).

All three predicates are invariant under linear isometry equivalences (ZLattice.isIntegral_comap_iff, ZLattice.isEven_comap_iff, ZLattice.isUnimodular_comap_iff), stated for the pull-back ZLattice.comap of Mathlib.

These are the hypotheses under which the theta series of a lattice is a modular form: an even unimodular lattice has a theta series of level one.

Main definitions

• ZLattice.IsIntegral L: the lattice L is integral, L ≤ dual L.
• ZLattice.IsEven L: every vector of L has even integral squared norm.
• ZLattice.IsUnimodular L: the lattice L is self-dual, L = dual L.
• ZLattice.IsIntegral.integralForm: the inner product of an integral lattice, as an integer-valued symmetric bilinear form on L.

Main statements

• ZLattice.isIntegral_iff: L is integral if and only if all inner products on L are integers.
• ZLattice.IsEven.isIntegral: an even lattice is integral.
• ZLattice.IsIntegral.discreteTopology: an integral lattice is discrete.
• ZLattice.IsUnimodular.span_eq_top: a unimodular lattice in a finite-dimensional space spans it.
• ZLattice.isEven_span_singleton_iff: the lattice ℤ v is even if and only if ‖v‖² ∈ 2ℤ.
• ZLattice.IsEven.exists_norm_add_sq_sub_norm_sq_eq, ZLattice.IsIntegral.exists_norm_add_sq_sub_norm_sq_eq: for γ ∈ L^∨ and v ∈ L, ‖γ + v‖² - ‖γ‖² lies in 2ℤ when L is even and in ℤ when L is integral, so ‖γ‖² / 2 is well defined modulo ℤ on L^∨ / L in the first case.
• ZLattice.IsEven.exists_natCast_mul_norm_add_sq_eq: for even L, γ ∈ L^∨ and N ‖γ‖² ∈ 2ℤ, N ‖γ + v‖² ∈ 2ℤ for every v ∈ L.

Even lattices

def ZLattice.IsEven {E : Type u_1} [SeminormedAddCommGroup E] (L : Submodule ℤ E) : Prop

A lattice is even if the squared norm of each of its vectors is an even integer.

theorem ZLattice.isEven_iff {E : Type u_1} [SeminormedAddCommGroup E] {L : Submodule ℤ E} : IsEven L ↔ ∀ x ∈ L, ∃ (m : ℤ), ‖x‖ ^ 2 = 2 * ↑m

theorem ZLattice.IsEven.mono {E : Type u_1} [SeminormedAddCommGroup E] {L M : Submodule ℤ E} (hM : IsEven M) (h : L ≤ M) : IsEven L

A sublattice of an even lattice is even.

theorem ZLattice.isEven_span_singleton_iff {E : Type u_1} [SeminormedAddCommGroup E] [NormSMulClass ℤ E] {v : E} : IsEven (ℤ ∙ v) ↔ ∃ (m : ℤ), ‖v‖ ^ 2 = 2 * ↑m

The lattice spanned by a single vector v is even if and only if ‖v‖² is an even integer.

theorem ZLattice.isEven_span_sqrt_two : IsEven (ℤ ∙ √2)

The lattice √2 ℤ ⊆ ℝ is even.

theorem ZLattice.not_isEven_span_one : ¬IsEven (ℤ ∙ 1)

The lattice ℤ ⊆ ℝ is not even: the vector 1 has squared norm 1.

@[simp]

theorem ZLattice.isEven_comap_iff {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedAddCommGroup F] [NormedSpace ℝ E] [NormedSpace ℝ F] (L : Submodule ℤ E) (e : F ≃ₗᵢ[ℝ] E) : IsEven (ZLattice.comap ℝ L ↑e.toLinearEquiv) ↔ IsEven L

Evenness is invariant under linear isometry equivalences.

Integral lattices

def ZLattice.IsIntegral {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (L : Submodule ℤ E) : Prop

A lattice is integral if it is contained in its dual, that is, if the inner product of any two of its vectors is an integer (isIntegral_iff).

theorem ZLattice.isIntegral_iff_le_dual {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {L : Submodule ℤ E} : IsIntegral L ↔ L ≤ dual L

theorem ZLattice.isIntegral_iff {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {L : Submodule ℤ E} : IsIntegral L ↔ ∀ x ∈ L, ∀ y ∈ L, ∃ (m : ℤ), inner ℝ x y = ↑m

A lattice is integral exactly when the inner product of any two of its vectors is an integer.

theorem ZLattice.IsIntegral.mono {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {L M : Submodule ℤ E} (hM : IsIntegral M) (h : L ≤ M) : IsIntegral L

A sublattice of an integral lattice is integral.

theorem ZLattice.IsIntegral.discreteTopology {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {L : Submodule ℤ E} (h : IsIntegral L) : DiscreteTopology ↥L

An integral lattice is discrete.

noncomputable def ZLattice.IsIntegral.integralForm {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {L : Submodule ℤ E} (hL : IsIntegral L) : LinearMap.BilinForm ℤ ↥L

The integer-valued inner product on an integral lattice, as a ℤ-bilinear form on L.

@[simp]

theorem ZLattice.IsIntegral.integralForm_cast {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {L : Submodule ℤ E} (hL : IsIntegral L) (x y : ↥L) : ↑((hL.integralForm x) y) = inner ℝ ↑x ↑y

The integer-valued inner product of an integral lattice is the inner product of E.

theorem ZLattice.IsIntegral.isSymm_integralForm {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {L : Submodule ℤ E} (hL : IsIntegral L) : hL.integralForm.IsSymm

The integer-valued inner product of an integral lattice is symmetric.

theorem ZLattice.IsIntegral.exists_norm_add_sq_sub_norm_sq_eq {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {L : Submodule ℤ E} (hL : IsIntegral L) {γ v : E} (hγ : γ ∈ dual L) (hv : v ∈ L) : ∃ (m : ℤ), ‖γ + v‖ ^ 2 - ‖γ‖ ^ 2 = ↑m

For an integral lattice L, the squared norm ‖γ‖² of a dual vector γ ∈ L^∨ is well defined modulo ℤ on the coset γ + L: ‖γ + v‖² - ‖γ‖² ∈ ℤ for v ∈ L.

theorem ZLattice.IsEven.isIntegral {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {L : Submodule ℤ E} (h : IsEven L) : IsIntegral L

An even lattice is integral, by polarization.

theorem ZLattice.IsEven.exists_norm_add_sq_sub_norm_sq_eq {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {L : Submodule ℤ E} (hL : IsEven L) {γ v : E} (hγ : γ ∈ dual L) (hv : v ∈ L) : ∃ (m : ℤ), ‖γ + v‖ ^ 2 - ‖γ‖ ^ 2 = 2 * ↑m

For an even lattice L, the half-norm ‖γ‖² / 2 of a dual vector γ ∈ L^∨ is well defined modulo ℤ on the coset γ + L: ‖γ + v‖² - ‖γ‖² ∈ 2ℤ for v ∈ L.

theorem ZLattice.IsEven.exists_natCast_mul_norm_add_sq_eq {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {L : Submodule ℤ E} (hL : IsEven L) {γ : E} (hγ : γ ∈ dual L) {N : ℕ} (hNγ : ∃ (n : ℤ), ↑N * ‖γ‖ ^ 2 = 2 * ↑n) {v : E} (hv : v ∈ L) : ∃ (m : ℤ), ↑N * ‖γ + v‖ ^ 2 = 2 * ↑m

For an even lattice L, γ ∈ L^∨ and N ‖γ‖² ∈ 2ℤ, the squared norms on the coset satisfy N ‖γ + v‖² ∈ 2ℤ for every v ∈ L.

Unimodular lattices

def ZLattice.IsUnimodular {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (L : Submodule ℤ E) : Prop

A lattice is unimodular if it is equal to its dual.

theorem ZLattice.isUnimodular_iff_eq_dual {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {L : Submodule ℤ E} : IsUnimodular L ↔ L = dual L

theorem ZLattice.IsUnimodular.dual_eq {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {L : Submodule ℤ E} (h : IsUnimodular L) : dual L = L

theorem ZLattice.IsUnimodular.isIntegral {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {L : Submodule ℤ E} (h : IsUnimodular L) : IsIntegral L

A unimodular lattice is integral.

theorem ZLattice.IsUnimodular.span_eq_top {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {L : Submodule ℤ E} (h : IsUnimodular L) : Submodule.span ℝ ↑L = ⊤

A unimodular lattice in a finite-dimensional real inner product space spans the space over ℝ; in particular it is a full lattice.

theorem ZLattice.IsIntegral.isUnimodular_iff {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {L : Submodule ℤ E} (h : IsIntegral L) : IsUnimodular L ↔ dual L ≤ L

An integral lattice is unimodular as soon as its dual is contained in it.

theorem ZLattice.isUnimodular_span_orthonormalBasis {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {ι : Type u_3} [Fintype ι] (b : OrthonormalBasis ι ℝ E) : IsUnimodular (Submodule.span ℤ (Set.range ⇑b))

The ℤ-span of an orthonormal basis is unimodular.

theorem ZLattice.isUnimodular_span_one : IsUnimodular (ℤ ∙ 1)

The lattice ℤ ⊆ ℝ is unimodular.

Invariance under isometries

@[simp]

theorem ZLattice.isIntegral_comap_iff {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedAddCommGroup F] [InnerProductSpace ℝ E] [InnerProductSpace ℝ F] (L : Submodule ℤ E) (e : F ≃ₗᵢ[ℝ] E) : IsIntegral (ZLattice.comap ℝ L ↑e.toLinearEquiv) ↔ IsIntegral L

Integrality is invariant under linear isometry equivalences.

@[simp]

theorem ZLattice.isUnimodular_comap_iff {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedAddCommGroup F] [InnerProductSpace ℝ E] [InnerProductSpace ℝ F] (L : Submodule ℤ E) (e : F ≃ₗᵢ[ℝ] E) : IsUnimodular (ZLattice.comap ℝ L ↑e.toLinearEquiv) ↔ IsUnimodular L

Unimodularity is invariant under linear isometry equivalences.