The level of an integral lattice

The level of a nondegenerate integral lattice L with Gram matrix G is classically the least positive integer N for which N • G⁻¹ is an integral matrix with even diagonal. Since G⁻¹ is the Gram matrix of the dual basis, this says that the form N • B is integral and even on the dual lattice Lᵛ. Evenness alone already forces integrality, by polarization, so this file defines the level intrinsically as the nonnegative generator of the ideal of integers N with

N · B(x, x) ∈ 2ℤ   for every x ∈ Lᵛ,

and then proves the classical description in every carrier basis.

For an even lattice, N · B(x, x) ∈ 2ℤ says that N kills the half-norm q_L(x) = B(x, x) / 2 modulo ℤ, so the level is the least N with N • q_L = 0 on the discriminant group. In general the level divides 2 · det L, and for a nondegenerate lattice it kills the discriminant group A_L = Lᵛ / L.

Main definitions and results

• TauCeti.IntegralLattice.level: the level of an integral lattice.
• TauCeti.IntegralLattice.level_dvd_iff: the level divides N exactly when N · B(x, x) is an even integer for every dual vector x.
• TauCeti.IntegralLattice.mul_form_mem_one_of_level_dvd: a multiple N of the level makes N · B integral on the dual lattice.
• TauCeti.IntegralLattice.level_dvd_iff_gramMatrix and TauCeti.IntegralLattice.isLeast_level: in every carrier basis with Gram matrix G, the level is the least positive N for which N • G⁻¹ is integral with even diagonal.
• TauCeti.IntegralLattice.IsEven.level_dvd_iff: for an even lattice, the level divides N exactly when N kills the discriminant quadratic form.
• TauCeti.IntegralLattice.IsEven.level_eq_addOrderOf: when the discriminant group is cyclic, the level is the additive order of the quadratic value of a generator.
• TauCeti.IntegralLattice.level_nsmul_mem_carrier and TauCeti.IntegralLattice.exponent_discriminantGroup_dvd_level: the level of a nondegenerate lattice kills A_L.
• TauCeti.IntegralLattice.level_dvd_two_mul_determinant: the level divides 2 · det L.
• TauCeti.IntegralLattice.level_pos: a nondegenerate lattice has positive level.
• TauCeti.IntegralLattice.level_eq_one_iff: a nondegenerate lattice has level one exactly when it is even and unimodular.
• TauCeti.IntegralLattice.IsUnimodular.level_eq_two_iff: a unimodular lattice has level two exactly when it is odd.
• TauCeti.IntegralLattice.Isometry.level_eq: the level is an isometry invariant.

References

• T. Miyake, Modular Forms, §4.9.
• W. Ebeling, Lattices and Codes, Chapter 3.

noncomputable def TauCeti.IntegralLattice.level {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) : ℕ

The level of an integral lattice: the nonnegative generator of the ideal of integers N such that N · B(x, x) is an even integer for every vector x of the dual lattice Lᵛ (level_dvd_iff). It is positive when L is nondegenerate (level_pos).

For a nondegenerate lattice this is the least positive N for which N • G⁻¹ is an integral matrix with even diagonal, G being a Gram matrix of L (isLeast_level).

Equations

• L.level = (Submodule.IsPrincipal.generator (TauCeti.IntegralLattice.levelIdeal✝ L)).natAbs

theorem TauCeti.IntegralLattice.level_dvd_iff {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) (N : ℤ) : ↑L.level ∣ N ↔ ∀ x ∈ L.dualCarrier, ∃ (k : ℤ), ↑N * L.norm x = 2 * ↑k

The defining property of the level: it divides N exactly when N · B(x, x) is an even integer for every dual vector x.

theorem TauCeti.IntegralLattice.mul_form_mem_one_of_level_dvd {V : Type u} [AddCommGroup V] [Module ℚ V] {L : IntegralLattice V} {N : ℤ} (hN : ↑L.level ∣ N) {x y : V} (hx : x ∈ L.dualCarrier) (hy : y ∈ L.dualCarrier) : ↑N * (L.form x) y ∈ 1

For a multiple N of the level, the form N · B is integral on the dual lattice.

The level kills the discriminant group

theorem TauCeti.IntegralLattice.level_nsmul_mem_carrier {V : Type u} [AddCommGroup V] [Module ℚ V] {L : IntegralLattice V} [L.IsNondegenerate] {x : V} (hx : x ∈ L.dualCarrier) : L.level • x ∈ L.carrier

A multiple of the level by a dual vector lies in the lattice, when L is nondegenerate.

theorem TauCeti.IntegralLattice.exponent_discriminantGroup_dvd_level {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) [L.IsNondegenerate] : AddMonoid.exponent L.DiscriminantGroup ∣ L.level

The exponent of the discriminant group of a nondegenerate lattice divides its level.

theorem TauCeti.IntegralLattice.level_dvd_two_mul_determinant {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) : ↑L.level ∣ 2 * L.determinant

The level divides twice the determinant.

theorem TauCeti.IntegralLattice.level_pos {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) [L.IsNondegenerate] : 0 < L.level

A nondegenerate lattice has positive level.

The level in a carrier basis

theorem TauCeti.IntegralLattice.level_dvd_iff_gramMatrix {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) [L.IsNondegenerate] {ι : Type v} [Fintype ι] [DecidableEq ι] (b : Module.Basis ι ℤ ↥L.carrier) (N : ℤ) : ↑L.level ∣ N ↔ ∃ (M : Matrix ι ι ℤ), (∀ (i : ι), Even (M i i)) ∧ M.map Int.cast = ↑N • ((L.gramMatrix b).map Int.cast)⁻¹

Basis independence of the level. In any carrier basis with Gram matrix G, the level of a nondegenerate lattice divides N exactly when N • G⁻¹ is an integral matrix with even diagonal.

theorem TauCeti.IntegralLattice.isLeast_level {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) [L.IsNondegenerate] {ι : Type v} [Fintype ι] [DecidableEq ι] (b : Module.Basis ι ℤ ↥L.carrier) : IsLeast {N : ℕ | 0 < N ∧ ∃ (M : Matrix ι ι ℤ), (∀ (i : ι), Even (M i i)) ∧ M.map Int.cast = ↑N • ((L.gramMatrix b).map Int.cast)⁻¹} L.level

The level as a least element. In any carrier basis with Gram matrix G, the level of a nondegenerate lattice is the least positive N for which N • G⁻¹ is an integral matrix with even diagonal.

Even lattices: the level annihilates the discriminant form

theorem TauCeti.IntegralLattice.IsEven.level_dvd_iff {V : Type u} [AddCommGroup V] [Module ℚ V] {L : IntegralLattice V} (hL : L.IsEven) (N : ℤ) : ↑L.level ∣ N ↔ ∀ (a : L.DiscriminantGroup), N • (L.discriminantQuadraticMap hL) a = 0

The level of an even lattice is the annihilator of its discriminant form: the level divides N exactly when N • q_L = 0 on the discriminant group.

theorem TauCeti.IntegralLattice.IsEven.level_eq_addOrderOf {V : Type u} [AddCommGroup V] [Module ℚ V] {L : IntegralLattice V} (hL : L.IsEven) (a : L.DiscriminantGroup) (ha : AddSubgroup.zmultiples a = ⊤) : L.level = addOrderOf ((L.discriminantQuadraticMap hL) a)

If a class generates the discriminant group of an even lattice, the level is the additive order of its quadratic value. No nondegeneracy hypothesis is needed.

Unimodular lattices

theorem TauCeti.IntegralLattice.level_eq_one_iff {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) [L.IsNondegenerate] : L.level = 1 ↔ L.IsEven ∧ L.IsUnimodular

A nondegenerate lattice has level one exactly when it is even and unimodular.

Nondegeneracy is needed: the zero form on ℤ has the whole rational line as its dual lattice, on which every norm vanishes, so its level is one although it is not unimodular.

theorem TauCeti.IntegralLattice.IsUnimodular.level_dvd_two {V : Type u} [AddCommGroup V] [Module ℚ V] {L : IntegralLattice V} (hL : L.IsUnimodular) : L.level ∣ 2

A unimodular lattice has level dividing two.

theorem TauCeti.IntegralLattice.IsUnimodular.level_eq_two_iff {V : Type u} [AddCommGroup V] [Module ℚ V] {L : IntegralLattice V} (hL : L.IsUnimodular) : L.level = 2 ↔ ¬L.IsEven

A unimodular lattice has level two exactly when it is odd, and level one otherwise.

Isometry invariance

theorem TauCeti.IntegralLattice.Isometry.level_eq {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.level = M.level

The level is an isometry invariant.