The level of a lattice

Let L be a lattice in a real inner product space E, with dual lattice L^∨ = ZLattice.dual L. The level of L is the least positive integer N such that N ‖x‖² / 2 is an integer for every x ∈ L^∨ (ZLattice.level). For an even lattice it is the order of the discriminant quadratic form q_L(x + L) = ‖x‖² / 2 mod ℤ on the discriminant group A_L = L^∨ ⧸ L, and it is the level N of the congruence subgroup Γ₀(N) governing the transformation law of the theta series of L (of weight n / 2, n the rank, with a character or multiplier system depending on L).

The integers N with N ‖x‖² ∈ 2ℤ for all x ∈ L^∨ form a subgroup of ℤ, and the level generates it: level L ∣ N exactly when N has this property (ZLattice.level_dvd_iff). This characterization holds for every lattice, since the level is defined as an unguarded infimum; no statement here depends on its value when no positive N works. That does not happen for a full integral lattice (ZLattice.IsIntegral.level_pos): there the order d of the finite group A_L kills A_L, so d x ∈ L and d ‖x‖² = ⟪x, d x⟫ ∈ ℤ for x ∈ L^∨, and level L ∣ 2 d. By polarization the level also controls the dual inclusion of a full lattice, level L • L^∨ ≤ L, so the exponent of A_L divides the level and |A_L| divides level L ^ n, n the rank, since A_L is generated by n elements (ZLattice.rank_discriminantGroup_le). For an integral lattice |A_L| = det L, so every prime dividing det L divides the level. The same characterization computes the level of an orthogonal direct sum: the dual of L ⊕ M is L^∨ ⊕ M^∨ and squared norms add, so level (L ⊕ M) = lcm (level L) (level M) (ZLattice.level_orthSum).

The level is neither the exponent of A_L nor det L. For an orthonormal basis b of a nonzero space and a positive integer m, the scaled cubic lattice √m • ℤ b has level 2 m (ZLattice.level_sqrt_smul_span_orthonormalBasis): its dual is (√m)⁻¹ • ℤ b, with squared norms ‖y‖² / m. Thus √2 ℤ ⊆ ℝ, which is even with A_L ≅ ℤ/2 and det L = 2, has level 4 (ZLattice.level_span_sqrt_two), and so has √2 ℤ², with A_L ≅ (ℤ/2)² and det L = 4; the odd unimodular lattice ℤⁿ has level 2. For an even lattice, level L = 1 exactly when L is unimodular (ZLattice.IsEven.level_eq_one_iff). Evenness is needed for this: the lattice ½ ℤ ⊆ ℝ has the even dual 2 ℤ, so it has level one, but it is neither even nor unimodular.

This is the level of the real model of a lattice, with the norm of E as its quadratic form. The rational model TauCeti.IntegralLattice has the analogous invariant TauCeti.IntegralLattice.level, defined by the same condition on its dual lattice, and this file follows its API. For a full integral lattice the two agree on the rational model ZLattice.ratModel (ZLattice.level_ratModel), which transports the descriptions proved there. Conversely the real model TauCeti.IntegralLattice.realModel of a positive definite rational lattice M has the level of M (TauCeti.IntegralLattice.level_realModel), so the levels computed on the rational side, such as those of the root lattices, hold verbatim for their real models. For even L the level divides N exactly when N kills the discriminant quadratic form (ZLattice.IsEven.level_dvd_iff_discriminantQuadraticMap), so it is the least N > 0 with this property (ZLattice.IsEven.isLeast_level_discriminantQuadraticMap), and when A_L is cyclic it is the additive order or rational denominator of the quadratic value of a generator. Consequently, for an even full lattice of level dividing N > 0 and x ∈ L^∨, the coset shell cosetShell L x t is empty unless t = 2m / N for some m : ℕ whose residue modulo N maps to q_L(x + L) under ZMod.toRatAddCircle N (ZLattice.IsEven.cosetShell_eq_empty_of_level_dvd, ZLattice.IsEven.cosetShell_eq_empty_of_level). For a ℤ-basis b of L with real Gram matrix G = (⟪b i, b j⟫), the level divides N exactly when N • G⁻¹ is an integral matrix with even diagonal (ZLattice.level_dvd_iff_gram), so it is the least N > 0 with this property (ZLattice.isLeast_level). Indeed G⁻¹ is the Gram matrix of the basis of L^∨ dual to b.

The approach and API here (the unguarded-infimum definition, the divisibility characterization, the dual inclusion and the discriminant-group bounds) are adapted from the earlier formalization by tauceti-ai-for-science in Tau Ceti PR #20694.

Main definitions

• ZLattice.level L: the least N > 0 with N ‖x‖² / 2 ∈ ℤ for every x ∈ L^∨.

Main statements

• ZLattice.level_dvd_iff: level L ∣ N if and only if N ‖x‖² ∈ 2ℤ for every x ∈ L^∨.
• ZLattice.level_dvd_two_mul_card_discriminantGroup, ZLattice.IsIntegral.level_pos: the level divides 2 |A_L|, which is 2 det L for a full integral lattice, and is then positive.
• ZLattice.level_nsmul_mem: level L • x ∈ L for x ∈ L^∨.
• ZLattice.exponent_discriminantGroup_dvd_level: the exponent of A_L divides the level.
• ZLattice.card_discriminantGroup_dvd_level_pow: for a full lattice |A_L| divides level L ^ n, ZLattice.prime_dvd_level: every prime dividing |A_L| divides the level, and ZLattice.coprime_card_discriminantGroup_of_coprime_level: every natural number coprime to level L is coprime to |A_L|.
• ZLattice.IsEven.level_eq_one_iff: an even lattice has level one exactly when it is unimodular.
• ZLattice.level_comap: the level is invariant under linear isometry equivalences.
• ZLattice.level_orthSum: the level of an orthogonal direct sum L ⊕ M is lcm (level L) (level M).
• ZLattice.level_ratModel: the level of a full integral lattice is the level of its rational model, and TauCeti.IntegralLattice.level_realModel: the level of the real model of a positive definite rational lattice is the level of that lattice.
• ZLattice.IsIntegral.isLeast_level_norm_sq, ZLattice.level_dvd_iff_gram, ZLattice.isLeast_level, ZLattice.IsEven.level_dvd_iff_discriminantQuadraticMap, ZLattice.IsEven.isLeast_level_discriminantQuadraticMap: the three equivalent IsLeast characterizations of level L (via dual norms, inverse Gram matrices, and the discriminant quadratic form).
• ZLattice.IsEven.cosetShell_eq_empty_of_level, ZLattice.IsEven.cosetRepresentationNumber_div_eq_zero_of_toRatAddCircle_ne: coset shells and coset representation numbers vanish outside the residue class of q_L(γ).
• ZLattice.level_sqrt_smul_span_orthonormalBasis: the lattice √m • ℤⁿ, n > 0, has level 2 m.

References

• W. Ebeling, Lattices and Codes, 3rd ed., Springer, 2013, Chapter 3.
• H. Iwaniec, Topics in Classical Automorphic Forms, AMS, 1997, Chapter 10.

noncomputable def ZLattice.level {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (L : Submodule ℤ E) : ℕ

The level of a lattice L: the least N > 0 such that N ‖x‖² / 2 is an integer for every x in the dual lattice. For an even lattice this is the order of the discriminant quadratic form ‖x‖² / 2 mod ℤ on L^∨ ⧸ L. The definition is the unguarded infimum, so it has a value on every lattice; level_dvd_iff characterizes it in general, and IsIntegral.level_pos shows that it is positive for a full integral lattice.

theorem ZLattice.exists_level_mul_norm_sq_eq {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {L : Submodule ℤ E} {x : E} (hx : x ∈ dual L) : ∃ (m : ℤ), ↑(level L) * ‖x‖ ^ 2 = 2 * ↑m

For x in the dual lattice, level L * ‖x‖² is an even integer.

theorem ZLattice.level_dvd_iff {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {L : Submodule ℤ E} {N : ℕ} : level L ∣ N ↔ ∀ x ∈ dual L, ∃ (m : ℤ), ↑N * ‖x‖ ^ 2 = 2 * ↑m

The level generates the subgroup of integers N with N ‖x‖² ∈ 2ℤ for every x ∈ L^∨: level L ∣ N exactly when N ‖x‖² / 2 is an integer for every x in the dual lattice.

@[simp]

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

The level is invariant under linear isometry equivalences.

@[simp]

theorem ZLattice.level_orthSum {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [NormedAddCommGroup F] [InnerProductSpace ℝ F] (L : Submodule ℤ E) (M : Submodule ℤ F) : level (orthSum L M) = (level L).lcm (level M)

The level of an orthogonal direct sum is the least common multiple of the levels of the summands.

theorem ZLattice.level_dvd_two_mul_card_discriminantGroup {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {L : Submodule ℤ E} : level L ∣ 2 * Nat.card (DiscriminantGroup L)

The level of a lattice divides twice the order of its discriminant group L^∨ ⧸ (L ∩ L^∨), which is det L for a full integral lattice. When the discriminant group is infinite its Nat.card is 0, and the statement is trivial.

Coset shells at multiples of the level

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

For an even lattice L, γ ∈ L^∨, v ∈ L and a multiple N of level L, N ‖γ + v‖² is an even integer.

theorem ZLattice.IsEven.cosetShell_eq_empty_of_not_exists_div_of_level_dvd {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {L : Submodule ℤ E} (hL : IsEven L) {γ : E} (hγ : γ ∈ dual L) {N : ℕ} (hN : 0 < N) (hdvd : level L ∣ N) {t : ℝ} (ht : ¬∃ (m : ℕ), t = 2 * ↑m / ↑N) : cosetShell L γ t = ∅

For an even lattice L, γ ∈ L^∨ and a positive multiple N of level L, every squared norm represented by γ + L has the form 2m / N with m : ℕ.

theorem ZLattice.IsEven.cosetRepresentationNumber_eq_zero_of_not_exists_div_of_level_dvd {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {L : Submodule ℤ E} (hL : IsEven L) {γ : E} (hγ : γ ∈ dual L) {N : ℕ} (hN : 0 < N) (hdvd : level L ∣ N) {t : ℝ} (ht : ¬∃ (m : ℕ), t = 2 * ↑m / ↑N) : cosetRepresentationNumber L γ t = 0

For an even lattice L, γ ∈ L^∨ and a positive multiple N of level L, r_{γ+L}(t) vanishes unless t = 2m / N for some m : ℕ.

Full lattices

theorem ZLattice.level_nsmul_mem {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {L : Submodule ℤ E} [FiniteDimensional ℝ E] [DiscreteTopology ↥L] [IsZLattice ℝ L] {x : E} (hx : x ∈ dual L) : level L • x ∈ L

The level controls the dual inclusion: level L • x ∈ L for every x ∈ L^∨, that is, level L • L^∨ ≤ L.

theorem ZLattice.exponent_discriminantGroup_dvd_level {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {L : Submodule ℤ E} [FiniteDimensional ℝ E] [DiscreteTopology ↥L] [IsZLattice ℝ L] : AddMonoid.exponent (DiscriminantGroup L) ∣ level L

The exponent of the discriminant group divides the level.

theorem ZLattice.IsIntegral.level_pos {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {L : Submodule ℤ E} [FiniteDimensional ℝ E] [DiscreteTopology ↥L] [IsZLattice ℝ L] (h : IsIntegral L) : 0 < level L

A full integral lattice has positive level.

theorem ZLattice.IsIntegral.isLeast_level_norm_sq {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {L : Submodule ℤ E} [FiniteDimensional ℝ E] [DiscreteTopology ↥L] [IsZLattice ℝ L] (hL : IsIntegral L) : IsLeast {N : ℕ | 0 < N ∧ ∀ x ∈ dual L, ∃ (m : ℤ), ↑N * ‖x‖ ^ 2 = 2 * ↑m} (level L)

For a full integral lattice L, the level is the least N > 0 such that N ‖x‖² / 2 is an integer for every x in the dual lattice.

theorem ZLattice.card_discriminantGroup_dvd_level_pow {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {L : Submodule ℤ E} [FiniteDimensional ℝ E] [DiscreteTopology ↥L] [IsZLattice ℝ L] : Nat.card (DiscriminantGroup L) ∣ level L ^ Module.finrank ℝ E

The order of the discriminant group of a full lattice of rank n divides level L ^ n. For an integral lattice this order is det L.

theorem ZLattice.prime_dvd_level {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {L : Submodule ℤ E} [FiniteDimensional ℝ E] [DiscreteTopology ↥L] [IsZLattice ℝ L] {p : ℕ} (hp : Nat.Prime p) (hpd : p ∣ Nat.card (DiscriminantGroup L)) : p ∣ level L

Every prime dividing the order of the discriminant group of a full lattice divides its level. For an integral lattice this order is det L.

theorem ZLattice.coprime_card_discriminantGroup_of_coprime_level {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {L : Submodule ℤ E} [FiniteDimensional ℝ E] [DiscreteTopology ↥L] [IsZLattice ℝ L] {a : ℕ} (ha : a.Coprime (level L)) : a.Coprime (Nat.card (DiscriminantGroup L))

Any natural number coprime to level L is coprime to the order of DiscriminantGroup L.

theorem ZLattice.IsEven.level_eq_one_iff {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {L : Submodule ℤ E} [FiniteDimensional ℝ E] [DiscreteTopology ↥L] [IsZLattice ℝ L] (h : IsEven L) : level L = 1 ↔ IsUnimodular L

An even full lattice has level one exactly when it is unimodular.

The rational model

@[simp]

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

The level of a full integral lattice is the level of its rational model.

theorem ZLattice.level_dvd_iff_gram {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {L : Submodule ℤ E} [FiniteDimensional ℝ E] [DiscreteTopology ↥L] [IsZLattice ℝ L] (hL : IsIntegral L) {ι : Type u_3} [Fintype ι] [DecidableEq ι] (b : Module.Basis ι ℤ ↥L) (N : ℕ) : level L ∣ N ↔ ∃ (M : Matrix ι ι ℤ), (∀ (i : ι), Even (M i i)) ∧ M.map Int.cast = ↑N • (Matrix.gram ℝ fun (i : ι) => ↑(b i))⁻¹

The level in a basis. For a full integral lattice L with a ℤ-basis b of real Gram matrix G = (⟪b i, b j⟫), the level divides N exactly when N • G⁻¹ is an integral matrix with even diagonal.

theorem ZLattice.isLeast_level {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {L : Submodule ℤ E} [FiniteDimensional ℝ E] [DiscreteTopology ↥L] [IsZLattice ℝ L] (hL : IsIntegral L) {ι : Type u_3} [Fintype ι] [DecidableEq ι] (b : Module.Basis ι ℤ ↥L) : IsLeast {N : ℕ | 0 < N ∧ ∃ (M : Matrix ι ι ℤ), (∀ (i : ι), Even (M i i)) ∧ M.map Int.cast = ↑N • (Matrix.gram ℝ fun (i : ι) => ↑(b i))⁻¹} (level L)

The level as a least element. For a full integral lattice L with a ℤ-basis b of real Gram matrix G = (⟪b i, b j⟫), the level is the least N > 0 for which N • G⁻¹ is an integral matrix with even diagonal.

The discriminant quadratic form and coset shells of an even lattice

theorem ZLattice.IsEven.level_dvd_iff_discriminantQuadraticMap {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {L : Submodule ℤ E} [FiniteDimensional ℝ E] [DiscreteTopology ↥L] [IsZLattice ℝ L] (hL : IsEven L) {N : ℕ} : level L ∣ N ↔ ∀ (γ : DiscriminantGroup L), N • ((ratModel ⋯).discriminantQuadraticMap ⋯) ((ratModelDiscriminantGroupEquiv ⋯) γ) = 0

The level of an even full lattice is the annihilator of its discriminant quadratic form: level L ∣ N if and only if N • q_L(γ) = 0 for every γ ∈ L^∨ ⧸ L, where q_L is read on the rational model.

@[simp]

theorem ZLattice.IsEven.level_nsmul_discriminantQuadraticMap {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {L : Submodule ℤ E} [FiniteDimensional ℝ E] [DiscreteTopology ↥L] [IsZLattice ℝ L] (hL : IsEven L) (γ : DiscriminantGroup L) : level L • ((ratModel ⋯).discriminantQuadraticMap ⋯) ((ratModelDiscriminantGroupEquiv ⋯) γ) = 0

The level of an even full lattice annihilates its discriminant quadratic form.

theorem ZLattice.IsEven.isLeast_level_discriminantQuadraticMap {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {L : Submodule ℤ E} [FiniteDimensional ℝ E] [DiscreteTopology ↥L] [IsZLattice ℝ L] (hL : IsEven L) : IsLeast {N : ℕ | 0 < N ∧ ∀ (γ : DiscriminantGroup L), N • ((ratModel ⋯).discriminantQuadraticMap ⋯) ((ratModelDiscriminantGroupEquiv ⋯) γ) = 0} (level L)

For an even full lattice L, the level is the least N > 0 that annihilates the discriminant quadratic form on L^∨ ⧸ L.

theorem ZLattice.IsEven.level_eq_addOrderOf_discriminantQuadraticMap {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {L : Submodule ℤ E} [FiniteDimensional ℝ E] [DiscreteTopology ↥L] [IsZLattice ℝ L] (hL : IsEven L) (γ : DiscriminantGroup L) (hγ : AddSubgroup.zmultiples γ = ⊤) : level L = addOrderOf (((ratModel ⋯).discriminantQuadraticMap ⋯) ((ratModelDiscriminantGroupEquiv ⋯) γ))

If γ generates the discriminant group of an even full lattice L, the level of L is the additive order of q_L(γ) in ℚ/ℤ.

theorem ZLattice.IsEven.level_eq_den_discriminantQuadraticMap {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {L : Submodule ℤ E} [FiniteDimensional ℝ E] [DiscreteTopology ↥L] [IsZLattice ℝ L] (hL : IsEven L) (γ : DiscriminantGroup L) (hγ : AddSubgroup.zmultiples γ = ⊤) {r : ℚ} (hr : ((ratModel ⋯).discriminantQuadraticMap ⋯) ((ratModelDiscriminantGroupEquiv ⋯) γ) = ↑r) : level L = r.den

If γ generates the discriminant group of an even full lattice L and q_L(γ) is the class of r : ℚ in ℚ/ℤ, the level of L is the denominator r.den.

theorem ZLattice.IsEven.existsUnique_toRatAddCircle_eq_discriminantQuadraticMap {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {L : Submodule ℤ E} [FiniteDimensional ℝ E] [DiscreteTopology ↥L] [IsZLattice ℝ L] (hL : IsEven L) {N : ℕ} (hN : 0 < N) (hdvd : level L ∣ N) (γ : DiscriminantGroup L) : ∃! a : ZMod N, (ZMod.toRatAddCircle N) a = ((ratModel ⋯).discriminantQuadraticMap ⋯) ((ratModelDiscriminantGroupEquiv ⋯) γ)

When 0 < N and level L ∣ N, every discriminant quadratic value q_L(γ) is the image under ZMod.toRatAddCircle N of a unique residue class modulo N (representing N q_L(γ) mod N).

theorem ZLattice.IsEven.existsUnique_toRatAddCircle_level_eq_discriminantQuadraticMap {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {L : Submodule ℤ E} [FiniteDimensional ℝ E] [DiscreteTopology ↥L] [IsZLattice ℝ L] (hL : IsEven L) (γ : DiscriminantGroup L) : ∃! a : ZMod (level L), (ZMod.toRatAddCircle (level L)) a = ((ratModel ⋯).discriminantQuadraticMap ⋯) ((ratModelDiscriminantGroupEquiv ⋯) γ)

Every discriminant quadratic value q_L(γ) of an even full lattice is the image under ZMod.toRatAddCircle (level L) of a unique residue class modulo level L.

theorem ZLattice.IsEven.toRatAddCircle_eq_discriminantQuadraticMap_of_mem_cosetShell {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {L : Submodule ℤ E} [FiniteDimensional ℝ E] [DiscreteTopology ↥L] [IsZLattice ℝ L] (hL : IsEven L) (x : ↥(dual L)) {N : ℕ} {m : ℤ} {v : E} (hv : v ∈ cosetShell L (↑x) (2 * ↑m / ↑N)) : (ZMod.toRatAddCircle N) ↑m = ((ratModel ⋯).discriminantQuadraticMap ⋯) ((ratModelDiscriminantGroupEquiv ⋯) (Submodule.Quotient.mk x))

If v belongs to the coset shell of x + L of squared norm 2m / N, then the residue of m modulo N maps to q_L(x + L) under ZMod.toRatAddCircle N.

theorem ZLattice.IsEven.cosetShell_div_eq_empty_of_toRatAddCircle_ne {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {L : Submodule ℤ E} [FiniteDimensional ℝ E] [DiscreteTopology ↥L] [IsZLattice ℝ L] (hL : IsEven L) (x : ↥(dual L)) {N : ℕ} {m : ℤ} (hm : (ZMod.toRatAddCircle N) ↑m ≠ ((ratModel ⋯).discriminantQuadraticMap ⋯) ((ratModelDiscriminantGroupEquiv ⋯) (Submodule.Quotient.mk x))) : cosetShell L (↑x) (2 * ↑m / ↑N) = ∅

For an even full lattice L and x ∈ L^∨, the coset shell of x + L of squared norm 2m / N is empty whenever m mod N does not map to q_L(x + L) under ZMod.toRatAddCircle N.

theorem ZLattice.IsEven.cosetRepresentationNumber_div_eq_zero_of_toRatAddCircle_ne {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {L : Submodule ℤ E} [FiniteDimensional ℝ E] [DiscreteTopology ↥L] [IsZLattice ℝ L] (hL : IsEven L) (x : ↥(dual L)) {N : ℕ} {m : ℤ} (hm : (ZMod.toRatAddCircle N) ↑m ≠ ((ratModel ⋯).discriminantQuadraticMap ⋯) ((ratModelDiscriminantGroupEquiv ⋯) (Submodule.Quotient.mk x))) : cosetRepresentationNumber L (↑x) (2 * ↑m / ↑N) = 0

For an even full lattice L and x ∈ L^∨, r_{x+L}(2m / N) vanishes whenever m mod N does not map to q_L(x + L) under ZMod.toRatAddCircle N.

theorem ZLattice.IsEven.cosetRepresentationNumberClass_div_eq_zero_of_toRatAddCircle_ne {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {L : Submodule ℤ E} [FiniteDimensional ℝ E] [DiscreteTopology ↥L] [IsZLattice ℝ L] (hL : IsEven L) (γ : DiscriminantGroup L) {N : ℕ} {m : ℤ} (hm : (ZMod.toRatAddCircle N) ↑m ≠ ((ratModel ⋯).discriminantQuadraticMap ⋯) ((ratModelDiscriminantGroupEquiv ⋯) γ)) : cosetRepresentationNumberClass L γ (2 * ↑m / ↑N) = 0

For an even full lattice L and γ : DiscriminantGroup L, r_γ(2m / N) vanishes whenever m mod N does not map to q_L(γ) under ZMod.toRatAddCircle N.

theorem ZLattice.IsEven.cosetRepresentationNumberClass_div_level_eq_zero_of_toRatAddCircle_ne {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {L : Submodule ℤ E} [FiniteDimensional ℝ E] [DiscreteTopology ↥L] [IsZLattice ℝ L] (hL : IsEven L) (γ : DiscriminantGroup L) {m : ℤ} (hm : (ZMod.toRatAddCircle (level L)) ↑m ≠ ((ratModel ⋯).discriminantQuadraticMap ⋯) ((ratModelDiscriminantGroupEquiv ⋯) γ)) : cosetRepresentationNumberClass L γ (2 * ↑m / ↑(level L)) = 0

For an even full lattice L and γ : DiscriminantGroup L, r_γ(2m / level L) vanishes whenever m mod level L does not map to q_L(γ) under ZMod.toRatAddCircle (level L).

theorem ZLattice.IsEven.cosetShell_eq_empty_of_level_dvd {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {L : Submodule ℤ E} [FiniteDimensional ℝ E] [DiscreteTopology ↥L] [IsZLattice ℝ L] (hL : IsEven L) (x : ↥(dual L)) {N : ℕ} (hN : 0 < N) (hdvd : level L ∣ N) {t : ℝ} (ht : ¬∃ (m : ℕ), t = 2 * ↑m / ↑N ∧ (ZMod.toRatAddCircle N) ↑m = ((ratModel ⋯).discriminantQuadraticMap ⋯) ((ratModelDiscriminantGroupEquiv ⋯) (Submodule.Quotient.mk x))) : cosetShell L (↑x) t = ∅

Coset shell support at a multiple of the level. For an even full lattice L, x ∈ L^∨, and a positive multiple N of level L, cosetShell L x t is empty unless t = 2m / N for some m : ℕ with ZMod.toRatAddCircle N (m : ZMod N) = q_L(x + L).

theorem ZLattice.IsEven.cosetShell_eq_empty_of_level {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {L : Submodule ℤ E} [FiniteDimensional ℝ E] [DiscreteTopology ↥L] [IsZLattice ℝ L] (hL : IsEven L) (x : ↥(dual L)) {t : ℝ} (ht : ¬∃ (m : ℕ), t = 2 * ↑m / ↑(level L) ∧ (ZMod.toRatAddCircle (level L)) ↑m = ((ratModel ⋯).discriminantQuadraticMap ⋯) ((ratModelDiscriminantGroupEquiv ⋯) (Submodule.Quotient.mk x))) : cosetShell L (↑x) t = ∅

Coset shell support at the level. For an even full lattice L and x ∈ L^∨, cosetShell L x t is empty unless t = 2m / level L for some m : ℕ with ZMod.toRatAddCircle (level L) (m : ZMod (level L)) = q_L(x + L).

theorem ZLattice.IsEven.cosetRepresentationNumber_eq_zero_of_level_dvd {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {L : Submodule ℤ E} [FiniteDimensional ℝ E] [DiscreteTopology ↥L] [IsZLattice ℝ L] (hL : IsEven L) (x : ↥(dual L)) {N : ℕ} (hN : 0 < N) (hdvd : level L ∣ N) {t : ℝ} (ht : ¬∃ (m : ℕ), t = 2 * ↑m / ↑N ∧ (ZMod.toRatAddCircle N) ↑m = ((ratModel ⋯).discriminantQuadraticMap ⋯) ((ratModelDiscriminantGroupEquiv ⋯) (Submodule.Quotient.mk x))) : cosetRepresentationNumber L (↑x) t = 0

For an even full lattice L, x ∈ L^∨ and a positive multiple N of level L, r_{x+L}(t) vanishes unless t = 2m / N for some m : ℕ with ZMod.toRatAddCircle N (m : ZMod N) = q_L(x + L).

theorem ZLattice.IsEven.cosetRepresentationNumber_eq_zero_of_level {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {L : Submodule ℤ E} [FiniteDimensional ℝ E] [DiscreteTopology ↥L] [IsZLattice ℝ L] (hL : IsEven L) (x : ↥(dual L)) {t : ℝ} (ht : ¬∃ (m : ℕ), t = 2 * ↑m / ↑(level L) ∧ (ZMod.toRatAddCircle (level L)) ↑m = ((ratModel ⋯).discriminantQuadraticMap ⋯) ((ratModelDiscriminantGroupEquiv ⋯) (Submodule.Quotient.mk x))) : cosetRepresentationNumber L (↑x) t = 0

For an even full lattice L and x ∈ L^∨, r_{x+L}(t) vanishes unless t = 2m / level L for some m : ℕ with ZMod.toRatAddCircle (level L) (m : ZMod (level L)) = q_L(x + L).

theorem ZLattice.IsEven.cosetRepresentationNumberClass_eq_zero_of_level_dvd {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {L : Submodule ℤ E} [FiniteDimensional ℝ E] [DiscreteTopology ↥L] [IsZLattice ℝ L] (hL : IsEven L) (γ : DiscriminantGroup L) {N : ℕ} (hN : 0 < N) (hdvd : level L ∣ N) {t : ℝ} (ht : ¬∃ (m : ℕ), t = 2 * ↑m / ↑N ∧ (ZMod.toRatAddCircle N) ↑m = ((ratModel ⋯).discriminantQuadraticMap ⋯) ((ratModelDiscriminantGroupEquiv ⋯) γ)) : cosetRepresentationNumberClass L γ t = 0

For an even full lattice L, γ : DiscriminantGroup L and a positive multiple N of level L, r_γ(t) vanishes unless t = 2m / N for some m : ℕ with ZMod.toRatAddCircle N (m : ZMod N) = q_L(γ).

theorem ZLattice.IsEven.cosetRepresentationNumberClass_eq_zero_of_level {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {L : Submodule ℤ E} [FiniteDimensional ℝ E] [DiscreteTopology ↥L] [IsZLattice ℝ L] (hL : IsEven L) (γ : DiscriminantGroup L) {t : ℝ} (ht : ¬∃ (m : ℕ), t = 2 * ↑m / ↑(level L) ∧ (ZMod.toRatAddCircle (level L)) ↑m = ((ratModel ⋯).discriminantQuadraticMap ⋯) ((ratModelDiscriminantGroupEquiv ⋯) γ)) : cosetRepresentationNumberClass L γ t = 0

For an even full lattice L and γ : DiscriminantGroup L, r_γ(t) vanishes unless t = 2m / level L for some m : ℕ with ZMod.toRatAddCircle (level L) (m : ZMod (level L)) = q_L(γ).

Scaled cubic lattices

theorem ZLattice.level_sqrt_smul_span_orthonormalBasis {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {ι : Type u_3} [Fintype ι] [Nonempty ι] (b : OrthonormalBasis ι ℝ E) {m : ℕ} (hm : m ≠ 0) : level (√↑m • Submodule.span ℤ (Set.range ⇑b)) = 2 * m

For an orthonormal basis b of a nonzero space and a positive integer m, the scaled cubic lattice √m • ℤ b has level 2 m: its dual (√m)⁻¹ • ℤ b has squared norms ‖y‖² / m with ‖y‖² ∈ ℤ, attaining 1 / m. For m = 2 and rank 2 this is the level 4 of √2 ℤ², whose determinant is also 4 but whose discriminant group (ℤ/2)² has exponent 2.

theorem ZLattice.level_span_sqrt_two : level (ℤ ∙ √2) = 4

The lattice √2 ℤ ⊆ ℝ has level 4, although its determinant is 2 and its discriminant group (1 / √2) ℤ ⧸ √2 ℤ has exponent 2.

The real model of a rational lattice

@[simp]

theorem TauCeti.IntegralLattice.level_realModel {V : Type u_1} [AddCommGroup V] [Module ℚ V] (M : IntegralLattice V) (hM : M.IsPosDef) : ZLattice.level (M.realModel hM) = M.level

The real model of a positive definite rational lattice M has the level of M.