Documentation

TauCeti.Algebra.Module.ZLattice.FrickePartner

The Fricke partner of an even lattice #

Let L be an even full lattice in a finite-dimensional real inner product space E, of rank n and level N = level L. Its Fricke partner is the scaled dual lattice √N • L^∨. The Fricke involution τ ↦ -1 / (N τ) exchanges the theta series of L and of √N • L^∨, which is why the partner appears in the transformation law of Θ_L under the Fricke matrix !![0, -1; N, 0].

This file proves that the Fricke partner is again an even lattice, that its determinant is Nⁿ / det L, and computes its level. Since (√N • L^∨)^∨ = (√N)⁻¹ • L, an integer K is a multiple of the level of the partner exactly when N divides K ‖x‖² / 2 for every x ∈ L. So the level is governed by the content c_L of L, the greatest common divisor of the half-norms ‖x‖² / 2 of the vectors of L (ZLattice.content):

level (√N • L^∨) = N / gcd (N, c_L).

In particular the level of the partner divides N, and it equals N exactly when no prime dividing N divides every half-norm of L. Equality fails in general: the lattice 2 ℤ ⊆ ℝ has level 8 and content 2, and its Fricke partner √8 • ½ ℤ = √2 ℤ has level 4 (ZLattice.level_sqrt_level_smul_dual_span_two). Similarly √2 • E₈ has level 2 and content 2, while its Fricke partner is E₈, of level 1. More generally, in positive dimension an even unimodular lattice L scaled by √m has level exactly m and Fricke partner L: the level divides m because (√m • L)^∨ = (√m)⁻¹ • L, and it is at least m because the Fricke partner √N • (√m)⁻¹ • L, being integral, has determinant (N / m)ⁿ ≥ 1.

The content and its basic API live in TauCeti.Algebra.Module.ZLattice.Content.

Main statements #

References #

The Fricke partner #

source
theorem ZLattice.isEven_sqrt_level_smul_dual {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (L : Submodule ℤ E) :
IsEven (√↑(level L) • dual L)

The Fricke partner √N • L^∨ of a lattice L of level N is even: for x ∈ L^∨ the squared norm ‖√N • x‖² = N ‖x‖² is an even integer by the definition of the level.

source
theorem ZLattice.isIntegral_sqrt_level_smul_dual {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {L : Submodule ℤ E} :
IsIntegral (√↑(level L) • dual L)

The Fricke partner √N • L^∨ of a lattice L of level N is integral.

source
theorem ZLattice.det_sqrt_level_smul_dual {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {L : Submodule ℤ E} [FiniteDimensional ℝ E] [DiscreteTopology ↥L] [IsZLattice ℝ L] [MeasurableSpace E] [BorelSpace E] :
det (√↑(level L) • dual L) = ↑(level L) ^ Module.finrank ℝ E / det L

The Fricke partner of a full lattice L of level N and rank n has determinant det (√N • L^∨) = Nⁿ / det L.

source
theorem ZLattice.IsIntegral.mul_card_discriminantGroup_sqrt_level_smul_dual {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {L : Submodule ℤ E} [FiniteDimensional ℝ E] [DiscreteTopology ↥L] [IsZLattice ℝ L] (h : IsIntegral L) :
Nat.card (DiscriminantGroup L) * Nat.card (DiscriminantGroup (√↑(level L) • dual L)) = level L ^ Module.finrank ℝ E

For an integral full lattice L of rank n and level N, the orders of the discriminant groups of L and of its Fricke partner √N • L^∨ multiply to Nⁿ.

source
theorem ZLattice.IsEven.level_sqrt_level_smul_dual {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {L : Submodule ℤ E} [FiniteDimensional ℝ E] [DiscreteTopology ↥L] [IsZLattice ℝ L] (h : IsEven L) :
level (√↑(level L) • dual L) = level L / (level L).gcd (content L)

The level of the Fricke partner. For an even full lattice L of level N and content c_L (the greatest common divisor of its half-norms ‖x‖² / 2), the Fricke partner √N • L^∨ has level N / gcd (N, c_L).

source
theorem ZLattice.IsEven.level_sqrt_level_smul_dual_dvd {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {L : Submodule ℤ E} [FiniteDimensional ℝ E] [DiscreteTopology ↥L] [IsZLattice ℝ L] (h : IsEven L) :
level (√↑(level L) • dual L) ∣ level L

The level of the Fricke partner √N • L^∨ of an even full lattice of level N divides N.

source
theorem ZLattice.IsEven.level_sqrt_level_smul_dual_eq_level_iff {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {L : Submodule ℤ E} [FiniteDimensional ℝ E] [DiscreteTopology ↥L] [IsZLattice ℝ L] (h : IsEven L) :
level (√↑(level L) • dual L) = level L ↔ (level L).Coprime (content L)

The Fricke partner √N • L^∨ of an even full lattice of level N has level exactly N if and only if N is coprime to the content of L, that is, no prime dividing N divides every half-norm ‖x‖² / 2 of L.

Scaled even unimodular lattices #

source
theorem ZLattice.IsEven.level_sqrt_smul_of_isUnimodular {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {L : Submodule ℤ E} [FiniteDimensional ℝ E] [DiscreteTopology ↥L] [IsZLattice ℝ L] [Nontrivial E] (h : IsEven L) (hU : IsUnimodular L) {m : ℕ} (hm : m ≠ 0) :
level (√↑m • L) = m

Scaled even unimodular lattices. In positive dimension, scaling an even unimodular full lattice L by √m, for a positive integer m, gives an even lattice of level exactly m. For instance √2 • E₈ has level 2.

source
theorem ZLattice.IsEven.sqrt_level_smul_dual_sqrt_smul_of_isUnimodular {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {L : Submodule ℤ E} [FiniteDimensional ℝ E] [DiscreteTopology ↥L] [IsZLattice ℝ L] [Nontrivial E] (h : IsEven L) (hU : IsUnimodular L) {m : ℕ} (hm : m ≠ 0) :
√↑(level (√↑m • L)) • dual (√↑m • L) = L

In positive dimension, the Fricke partner of √m • L, for an even unimodular full lattice L and a positive integer m, is L itself: √m • (√m • L)^∨ = L. For instance the Fricke partner of √2 • E₈ is E₈, of level 1.

An example #

source
theorem ZLattice.level_sqrt_level_smul_dual_span_two :
level (√↑(level (ℤ ∙ 2)) • dual (ℤ ∙ 2)) = 4

The Fricke partner of 2 ℤ ⊆ ℝ, which has level 8, is √8 • ½ ℤ = √2 ℤ, of level 4: the level of the Fricke partner of an even lattice can be a proper divisor of the level. This agrees with IsEven.level_sqrt_level_smul_dual, since the content of 2 ℤ is 2 (content_span_two) and 8 / gcd (8, 2) = 4.