Theta series of even unimodular lattices

Let L be an even unimodular lattice in a real inner product space E of dimension n. This file proves that n is divisible by 8 and that, writing n = 2k, the theta series Θ_L is a modular form of weight k for SL(2, ℤ).

For a unimodular lattice L^∨ = L and covol L = 1, so the inversion law reads Θ_L ∣[k] S = (-i)^k Θ_L (ZLattice.IsUnimodular.thetaSeries_slash_S). The rank argument is the elementary one. If n ≡ 4 (mod 8), then k ≡ 2 (mod 4) and Θ_L ∣[k] S = -Θ_L, while Θ_L ∣[k] T = Θ_L because L is even. The relation S³ T S T S = T⁻¹ in SL(2, ℤ) then gives -Θ_L = Θ_L, which is impossible since Θ_L(i) ≠ 0. A general rank n reduces to this case: the orthogonal direct sums L ⊕ L and (L ⊕ L) ⊕ (L ⊕ L) are again even unimodular, of ranks 2n and 4n, and none of n, 2n, 4n being 4 modulo 8 forces 8 ∣ n.

Once 8 ∣ n, the factor (-i)^k is 1, so Θ_L is invariant under both generators S and T of SL(2, ℤ); with holomorphy and boundedness at i∞ this makes Θ_L a level-one modular form, ZLattice.thetaForm, built as Mathlib builds CuspForm.discriminant. Its q-expansion coefficients are the representation numbers r_L(2m) (ZLattice.qExpansion_thetaForm_coeff), it is nonzero since Θ_L(i) ≠ 0, it is not a cusp form since its value at ∞ is 1, it is invariant under linear isometries, and the theta form of an orthogonal direct sum L ⊕ M is the product of the theta forms of L and M, in weight k + k'.

Since 4 ∣ k, the theta series is then a unique combination of the products E₄ ^ a * Δ ^ b with 4 a + 12 b = k. Its q-expansion coefficients are the representation numbers r_L(2m), and those of E₄ and Δ are rational, so the coefficients of this combination are rational. This is the shape in which the theta series of a particular even unimodular lattice is identified inside the ring of level-one modular forms.

Main definitions

• ZLattice.thetaForm: the theta series of an even unimodular lattice of rank 2k, as a modular form of weight k for SL(2, ℤ).

Main statements

• ZLattice.IsEven.eight_dvd_finrank: the rank of an even unimodular lattice is divisible by 8.
• ZLattice.IsEven.thetaSeries_slash_S: Θ_L ∣[k] S = Θ_L for even unimodular L.
• ZLattice.qExpansion_thetaForm_coeff: the m-th q-expansion coefficient of Θ_L is r_L(2m).
• ZLattice.thetaForm_ne_zero: Θ_L is a nonzero modular form.
• ZLattice.not_isCuspForm_thetaForm: Θ_L is not a cusp form.
• ZLattice.thetaForm_comap: Θ_L is invariant under linear isometries.
• ZLattice.thetaForm_orthSum: Θ_{L ⊕ M} = Θ_L Θ_M as modular forms of weight k + k'.
• ZLattice.IsEven.existsUnique_finsupp_thetaSeries_eq_E₄_discriminant: for even unimodular L of rank 2k, Θ_L = ∑_{4 a + 12 b = k} c (a, b) • E₄ ^ a * Δ ^ b for a unique family of rational coefficients c (a, b).

References

• J.-P. Serre, A Course in Arithmetic, Ch. VII §6.
• W. Ebeling, Lattices and Codes, §3.2.

theorem ZLattice.IsEven.eight_dvd_finrank {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {L : Submodule ℤ E} [DiscreteTopology ↥L] [IsZLattice ℝ L] (hL : IsEven L) (hU : IsUnimodular L) : 8 ∣ Module.finrank ℝ E

The rank of an even unimodular lattice is divisible by 8.

theorem ZLattice.IsEven.thetaSeries_slash_S {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {L : Submodule ℤ E} [DiscreteTopology ↥L] [IsZLattice ℝ L] {k : ℕ} (hL : IsEven L) (hU : IsUnimodular L) (hk : Module.finrank ℝ E = 2 * k) : SlashAction.map (↑k) ModularGroup.S (thetaSeries L) = thetaSeries L

The inversion law of an even unimodular lattice: if L is even unimodular and dim E = 2k, then Θ_L ∣[k] S = Θ_L.

noncomputable def ZLattice.thetaForm {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {L : Submodule ℤ E} [DiscreteTopology ↥L] [IsZLattice ℝ L] {k : ℕ} (hL : IsEven L) (hU : IsUnimodular L) (hk : Module.finrank ℝ E = 2 * k) : ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range ↑k

The theta series of an even unimodular lattice is a level-one modular form: if L is even unimodular and dim E = 2k, then Θ_L is a modular form of weight k for SL(2, ℤ). Its coercion is thetaSeries L (ZLattice.coe_thetaForm).

@[simp]

theorem ZLattice.coe_thetaForm {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {L : Submodule ℤ E} [DiscreteTopology ↥L] [IsZLattice ℝ L] {k : ℕ} (hL : IsEven L) (hU : IsUnimodular L) (hk : Module.finrank ℝ E = 2 * k) : ⇑(thetaForm hL hU hk) = thetaSeries L

The coercion of ZLattice.thetaForm to a function is the theta series.

theorem ZLattice.qExpansion_thetaForm_coeff {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {L : Submodule ℤ E} [DiscreteTopology ↥L] [IsZLattice ℝ L] {k : ℕ} (hL : IsEven L) (hU : IsUnimodular L) (hk : Module.finrank ℝ E = 2 * k) (m : ℕ) : (PowerSeries.coeff m) (UpperHalfPlane.qExpansion 1 ⇑(thetaForm hL hU hk)) = ↑(representationNumber L (2 * ↑m))

The q-expansion coefficients of the theta form are representation numbers: the m-th coefficient in q = exp (2 π i τ) is the number r_L(2m) of vectors of L of squared norm 2m.

@[simp]

theorem ZLattice.thetaForm_ne_zero {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {L : Submodule ℤ E} [DiscreteTopology ↥L] [IsZLattice ℝ L] {k : ℕ} (hL : IsEven L) (hU : IsUnimodular L) (hk : Module.finrank ℝ E = 2 * k) : thetaForm hL hU hk ≠ 0

The theta series of an even unimodular lattice is a nonzero modular form.

@[simp]

theorem ZLattice.not_isCuspForm_thetaForm {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {L : Submodule ℤ E} [DiscreteTopology ↥L] [IsZLattice ℝ L] {k : ℕ} (hL : IsEven L) (hU : IsUnimodular L) (hk : Module.finrank ℝ E = 2 * k) : ¬(thetaForm hL hU hk).IsCuspForm

The theta series of an even unimodular lattice is not a cusp form: its value at ∞ is 1.

theorem ZLattice.thetaForm_comap {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {L : Submodule ℤ E} [DiscreteTopology ↥L] [IsZLattice ℝ L] {k : ℕ} {F : Type u_2} [NormedAddCommGroup F] [InnerProductSpace ℝ F] [FiniteDimensional ℝ F] (hL : IsEven L) (hU : IsUnimodular L) (hk : Module.finrank ℝ E = 2 * k) (e : F ≃ₗᵢ[ℝ] E) (hL' : IsEven (ZLattice.comap ℝ L ↑e.toLinearEquiv)) (hU' : IsUnimodular (ZLattice.comap ℝ L ↑e.toLinearEquiv)) (hk' : Module.finrank ℝ F = 2 * k) : thetaForm hL' hU' hk' = thetaForm hL hU hk

The theta form is invariant under linear isometries: pulling L back along a linear isometry equivalence e : F ≃ₗᵢ[ℝ] E does not change it.

theorem ZLattice.thetaForm_orthSum {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {L : Submodule ℤ E} [DiscreteTopology ↥L] [IsZLattice ℝ L] {k : ℕ} {F : Type u_2} [NormedAddCommGroup F] [InnerProductSpace ℝ F] [FiniteDimensional ℝ F] {M : Submodule ℤ F} [DiscreteTopology ↥M] [IsZLattice ℝ M] {k' : ℕ} (hL : IsEven L) (hU : IsUnimodular L) (hk : Module.finrank ℝ E = 2 * k) (hM : IsEven M) (hUM : IsUnimodular M) (hk' : Module.finrank ℝ F = 2 * k') : thetaForm ⋯ ⋯ ⋯ = ModularForm.mcast ⋯ ((thetaForm hL hU hk).mul (thetaForm hM hUM hk')) thetaForm_orthSum._proof_2

The theta form of an orthogonal direct sum of even unimodular lattices is the product of the theta forms of the summands, Θ_{L ⊕ M} = Θ_L Θ_M, as modular forms of weight k + k'.

theorem ZLattice.IsEven.existsUnique_finsupp_thetaSeries_eq_E₄_discriminant {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {L : Submodule ℤ E} [DiscreteTopology ↥L] [IsZLattice ℝ L] {k : ℕ} (hL : IsEven L) (hU : IsUnimodular L) (hk : Module.finrank ℝ E = 2 * k) : ∃! c : ℕ × ℕ →₀ ℚ, (∀ ab ∈ c.support, 4 * ab.1 + 12 * ab.2 = k) ∧ thetaSeries L = fun (τ : UpperHalfPlane) => c.sum fun (ab : ℕ × ℕ) (z : ℚ) => ↑z * ModularForm.E₄ τ ^ ab.1 * ModularForm.discriminant τ ^ ab.2

The theta series of an even unimodular lattice is a rational polynomial in E₄ and Δ. If L is even unimodular and dim E = 2k, then Θ_L = ∑_{4 a + 12 b = k} c (a, b) • E₄ ^ a * Δ ^ b for a unique finitely supported family of rational coefficients c (a, b).