Isometries, orthogonal sums and rescaling of theta series

An isometry preserves the theta series of a lattice and its translates. Multiplying a lattice and a translate by a nonzero real scalar multiplies the upper-half-plane parameter by its square. These statements use only reindexing, without discreteness or finite-dimensionality assumptions.

In the L² product WithLp 2 (E × F) we have ‖(x, y)‖² = ‖x‖² + ‖y‖², so each term of the theta series of an orthogonal direct sum L ⊕ M is the product of a term for L and a term for M, and the absolutely convergent series multiply: θ_{(γ, δ) + (L ⊕ M)} = θ_{γ+L} · θ_{δ+M} and Θ_{L ⊕ M} = Θ_L · Θ_M. For instance Θ_{E₈ ⊕ E₈} = Θ_{E₈}².

The reindexing uses Mathlib's ZLattice.comap_equiv and Submodule.equivMapOfInjective.

The theta series of an orthogonal direct sum L ⊕ M ⊆ WithLp 2 (E × F) (ZLattice.orthSum) is the product of the theta series of the summands, Θ_{L ⊕ M} = Θ_L Θ_M, and more generally θ_{(γ, δ) + (L ⊕ M)} = θ_{γ+L} θ_{δ+M} for every translate (γ, δ). Since ‖(x, y)‖² = ‖x‖² + ‖y‖², the term of index (v, w) ∈ L × M is the product of the terms of index v and w, and the double series is the product of the two series because both converge absolutely. Here L and M are discrete subgroups of finite-dimensional spaces, so that the series converge.

Main statements

• ZLattice.thetaCoset_comap, ZLattice.thetaSeries_comap: invariance under linear isometries.
• ZLattice.thetaCoset_smul, ZLattice.thetaSeries_smul: Θ_{c • L}(τ) = Θ_L(c² τ).
• ZLattice.thetaCoset_orthSum, ZLattice.thetaSeries_orthSum: Θ_{L ⊕ M} = Θ_L Θ_M.

References

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

@[simp]

theorem ZLattice.thetaCoset_comap {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedAddCommGroup F] [NormedSpace ℝ E] [NormedSpace ℝ F] (L : Submodule ℤ E) (e : F ≃ₗᵢ[ℝ] E) (γ : F) (τ : UpperHalfPlane) : thetaCoset (ZLattice.comap ℝ L ↑e.toLinearEquiv) γ τ = thetaCoset L (e γ) τ

Pulling a lattice and its translate back along a linear isometry preserves the theta series.

@[simp]

theorem ZLattice.thetaSeries_comap {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedAddCommGroup F] [NormedSpace ℝ E] [NormedSpace ℝ F] (L : Submodule ℤ E) (e : F ≃ₗᵢ[ℝ] E) (τ : UpperHalfPlane) : thetaSeries (ZLattice.comap ℝ L ↑e.toLinearEquiv) τ = thetaSeries L τ

Pulling a lattice back along a linear isometry preserves its theta series.

theorem ZLattice.thetaCoset_smul {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (L : Submodule ℤ E) {c : ℝ} (hc : c ≠ 0) (γ : E) (τ : UpperHalfPlane) : thetaCoset (c • L) (c • γ) τ = thetaCoset L γ (⟨c ^ 2, ⋯⟩ • τ)

Rescaling a lattice and a translate multiplies the parameter by the square of the scalar. The positive-real action on ℍ makes the domain of the rescaled parameter explicit.

theorem ZLattice.thetaSeries_smul {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (L : Submodule ℤ E) {c : ℝ} (hc : c ≠ 0) (τ : UpperHalfPlane) : thetaSeries (c • L) τ = thetaSeries L (⟨c ^ 2, ⋯⟩ • τ)

Rescaling a lattice by a nonzero real scalar multiplies the theta parameter by its square.

Orthogonal direct sums

@[simp]

theorem ZLattice.thetaCoset_orthSum {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedAddCommGroup F] [NormedSpace ℝ E] [NormedSpace ℝ F] [FiniteDimensional ℝ E] [FiniteDimensional ℝ F] (L : Submodule ℤ E) [DiscreteTopology ↥L] (M : Submodule ℤ F) [DiscreteTopology ↥M] (x : WithLp 2 (E × F)) : thetaCoset (orthSum L M) x = thetaCoset L x.fst * thetaCoset M x.snd

The theta series of a translate of an orthogonal direct sum is the product of the theta series of the translates of the summands: θ_{(γ, δ) + (L ⊕ M)} = θ_{γ+L} · θ_{δ+M}.

@[simp]

theorem ZLattice.thetaSeries_orthSum {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedAddCommGroup F] [NormedSpace ℝ E] [NormedSpace ℝ F] [FiniteDimensional ℝ E] [FiniteDimensional ℝ F] (L : Submodule ℤ E) [DiscreteTopology ↥L] (M : Submodule ℤ F) [DiscreteTopology ↥M] : thetaSeries (orthSum L M) = thetaSeries L * thetaSeries M

The theta series of an orthogonal direct sum is the product of the theta series of the summands: Θ_{L ⊕ M} = Θ_L · Θ_M.