The translation law of theta series

Let L be a lattice in a real inner product space E, with dual lattice L^∨. The term of index v ∈ L of the coset theta series θ_{γ+L}(τ) = ∑_{v ∈ L} exp (π i ‖γ + v‖² τ) is multiplied by exp (π i ‖γ + v‖² t) when τ is translated by a real number t. This file shows that this factor is independent of v in the two arithmetic situations of interest, and deduces the behaviour of theta series under the translations T ^ n : τ ↦ τ + n of the modular group.

• If L is even and γ ∈ L^∨, then ‖γ + v‖² ≡ ‖γ‖² (mod 2), so for every integer n θ_{γ+L}(τ + n) = exp (π i n ‖γ‖²) θ_{γ+L}(τ). In the notation e(x) = exp (2 π i x) and q_L(γ) = ‖γ‖² / 2 mod ℤ, this is θ_{γ+L}(τ + 1) = e(q_L(γ)) θ_{γ+L}(τ). In particular Θ_L(τ + 1) = Θ_L(τ), that is Θ_L ∣[k] T = Θ_L in every weight k, and θ_{γ+L} is invariant under T ^ N as soon as N ‖γ‖² / 2 ∈ ℤ; when some N > 0 works for every γ ∈ L^∨ (for instance when L is a full lattice in a finite-dimensional space), the least one is the level of L (ZLattice.IsEven.thetaCoset_slash_T_pow_level).
• If L is only integral and γ ∈ L^∨, then ‖γ + v‖² ≡ ‖γ‖² (mod 1), which gives the same statements for even translations: θ_{γ+L}(τ + 2) = exp (2 π i ‖γ‖²) θ_{γ+L}(τ) and Θ_L ∣[k] T ^ 2 = Θ_L. Integrality does not give period 1: the theta series of ℤ ⊆ ℝ is the Jacobi theta function, of period 2 only (jacobiTheta_T_sq_smul).

The rank of L is arbitrary, and no discreteness or finite dimensionality is needed: the identities hold termwise.

Main statements

• ZLattice.thetaCoset_vadd_eq_mul: if (‖γ + v‖² - ‖γ‖²) t ∈ 2ℤ for every v ∈ L, then θ_{γ+L}(τ + t) = exp (π i ‖γ‖² t) θ_{γ+L}(τ).
• ZLattice.thetaCoset_vadd_eq_self: if h ‖γ + v‖² ∈ 2ℤ for every v ∈ L, then θ_{γ+L} has period h.
• ZLattice.IsEven.cexp_pi_mul_I_mul_norm_add_sq: for even L, the factor e(q_L(γ)) depends only on the coset γ + L.
• ZLattice.IsEven.thetaCoset_slash_T_zpow, ZLattice.IsEven.thetaSeries_slash_T: the translation law for even lattices.
• ZLattice.IsEven.thetaCoset_slash_T_zpow_eq_self, ZLattice.IsEven.thetaCoset_slash_T_pow_level: invariance of θ_{γ+L} under T ^ N when N ‖γ‖² / 2 ∈ ℤ, and in particular under T ^ level L.
• ZLattice.IsIntegral.thetaCoset_slash_T_zpow_two_mul, ZLattice.IsIntegral.thetaSeries_slash_T_sq: the translation law for integral lattices.

References

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

theorem ZLattice.thetaCoset_vadd_eq_mul {E : Type u_1} [NormedAddCommGroup E] (L : Submodule ℤ E) (γ : E) {t : ℝ} (h : ∀ v ∈ L, ∃ (m : ℤ), (‖γ + v‖ ^ 2 - ‖γ‖ ^ 2) * t = 2 * ↑m) (τ : UpperHalfPlane) : thetaCoset L γ (t +ᵥ τ) = Complex.exp (↑Real.pi * Complex.I * ↑(‖γ‖ ^ 2) * ↑t) * thetaCoset L γ τ

If (‖γ + v‖² - ‖γ‖²) t is an even integer for every v ∈ L, then translating τ by t multiplies the theta series of γ + L by exp (π i ‖γ‖² t).

theorem ZLattice.thetaCoset_vadd_eq_self {E : Type u_1} [NormedAddCommGroup E] (L : Submodule ℤ E) (γ : E) {h : ℝ} (hnorm : ∀ v ∈ L, ∃ (m : ℤ), h * ‖γ + v‖ ^ 2 = 2 * ↑m) (τ : UpperHalfPlane) : thetaCoset L γ (h +ᵥ τ) = thetaCoset L γ τ

If h ‖γ + v‖² is an even integer for every v ∈ L, then the theta series of γ + L has period h.

Even lattices

@[simp]

theorem ZLattice.IsEven.thetaSeries_intCast_vadd {E : Type u_1} [NormedAddCommGroup E] {L : Submodule ℤ E} (hL : IsEven L) (n : ℤ) (τ : UpperHalfPlane) : thetaSeries L (↑n +ᵥ τ) = thetaSeries L τ

The theta series of an even lattice has period 1.

@[simp]

theorem ZLattice.IsEven.thetaSeries_one_vadd {E : Type u_1} [NormedAddCommGroup E] {L : Submodule ℤ E} (hL : IsEven L) (τ : UpperHalfPlane) : thetaSeries L (1 +ᵥ τ) = thetaSeries L τ

The theta series of an even lattice has period 1: Θ_L(τ + 1) = Θ_L(τ).

@[simp]

theorem ZLattice.IsEven.thetaSeries_slash_T_zpow {E : Type u_1} [NormedAddCommGroup E] {L : Submodule ℤ E} (hL : IsEven L) (k n : ℤ) : SlashAction.map k (ModularGroup.T ^ n) (thetaSeries L) = thetaSeries L

The theta series of an even lattice is invariant under every power of T, in every weight.

@[simp]

theorem ZLattice.IsEven.thetaSeries_slash_T {E : Type u_1} [NormedAddCommGroup E] {L : Submodule ℤ E} (hL : IsEven L) (k : ℤ) : SlashAction.map k ModularGroup.T (thetaSeries L) = thetaSeries L

The theta series of an even lattice is invariant under T, in every weight: Θ_L ∣[k] T = Θ_L.

theorem ZLattice.IsEven.cexp_pi_mul_I_mul_norm_add_sq {E : Type u_1} [NormedAddCommGroup E] {L : Submodule ℤ E} [InnerProductSpace ℝ E] {γ : E} (hL : IsEven L) (hγ : γ ∈ dual L) {v : E} (hv : v ∈ L) : Complex.exp (↑Real.pi * Complex.I * ↑(‖γ + v‖ ^ 2)) = Complex.exp (↑Real.pi * Complex.I * ↑(‖γ‖ ^ 2))

For an even lattice L and γ ∈ L^∨, the factor e(q_L(γ)) = exp (π i ‖γ‖²) of the translation law depends only on the coset γ + L.

theorem ZLattice.IsEven.thetaCoset_intCast_vadd {E : Type u_1} [NormedAddCommGroup E] {L : Submodule ℤ E} [InnerProductSpace ℝ E] {γ : E} (hL : IsEven L) (hγ : γ ∈ dual L) (n : ℤ) (τ : UpperHalfPlane) : thetaCoset L γ (↑n +ᵥ τ) = Complex.exp (↑Real.pi * Complex.I * ↑(‖γ‖ ^ 2) * ↑n) * thetaCoset L γ τ

The translation law of the theta series of a coset of an even lattice: for γ ∈ L^∨ and an integer n, θ_{γ+L}(τ + n) = exp (π i n ‖γ‖²) θ_{γ+L}(τ).

theorem ZLattice.IsEven.thetaCoset_one_vadd {E : Type u_1} [NormedAddCommGroup E] {L : Submodule ℤ E} [InnerProductSpace ℝ E] {γ : E} (hL : IsEven L) (hγ : γ ∈ dual L) (τ : UpperHalfPlane) : thetaCoset L γ (1 +ᵥ τ) = Complex.exp (↑Real.pi * Complex.I * ↑(‖γ‖ ^ 2)) * thetaCoset L γ τ

The translation law of the theta series of a coset of an even lattice: for γ ∈ L^∨, θ_{γ+L}(τ + 1) = e(q_L(γ)) θ_{γ+L}(τ) with e(q_L(γ)) = exp (π i ‖γ‖²).

theorem ZLattice.IsEven.thetaCoset_slash_T_zpow {E : Type u_1} [NormedAddCommGroup E] {L : Submodule ℤ E} [InnerProductSpace ℝ E] {γ : E} (hL : IsEven L) (hγ : γ ∈ dual L) (k n : ℤ) : SlashAction.map k (ModularGroup.T ^ n) (thetaCoset L γ) = Complex.exp (↑Real.pi * Complex.I * ↑(‖γ‖ ^ 2) * ↑n) • thetaCoset L γ

The translation law of the theta series of a coset of an even lattice, in slash form: for γ ∈ L^∨, every weight k and every integer n, θ_{γ+L} ∣[k] T ^ n = exp (π i n ‖γ‖²) θ_{γ+L}.

theorem ZLattice.IsEven.thetaCoset_slash_T {E : Type u_1} [NormedAddCommGroup E] {L : Submodule ℤ E} [InnerProductSpace ℝ E] {γ : E} (hL : IsEven L) (hγ : γ ∈ dual L) (k : ℤ) : SlashAction.map k ModularGroup.T (thetaCoset L γ) = Complex.exp (↑Real.pi * Complex.I * ↑(‖γ‖ ^ 2)) • thetaCoset L γ

The translation law of the theta series of a coset of an even lattice, in slash form: for γ ∈ L^∨ and every weight k, θ_{γ+L} ∣[k] T = e(q_L(γ)) θ_{γ+L}.

theorem ZLattice.IsEven.thetaCoset_slash_T_zpow_eq_self {E : Type u_1} [NormedAddCommGroup E] {L : Submodule ℤ E} [InnerProductSpace ℝ E] {γ : E} (hL : IsEven L) (hγ : γ ∈ dual L) (k : ℤ) {N : ℤ} (hN : ∃ (m : ℤ), ↑N * ‖γ‖ ^ 2 = 2 * ↑m) : SlashAction.map k (ModularGroup.T ^ N) (thetaCoset L γ) = thetaCoset L γ

For an even lattice L and γ ∈ L^∨, the theta series of γ + L is invariant under T ^ N as soon as N ‖γ‖² / 2 is an integer. When L is even of level N, this holds for every γ ∈ L^∨.

theorem ZLattice.IsEven.thetaCoset_intCast_vadd_of_level_dvd {E : Type u_1} [NormedAddCommGroup E] {L : Submodule ℤ E} [InnerProductSpace ℝ E] {γ : E} (hL : IsEven L) (hγ : γ ∈ dual L) {N : ℤ} (hN : ↑(level L) ∣ N) (τ : UpperHalfPlane) : thetaCoset L γ (↑N +ᵥ τ) = thetaCoset L γ τ

For an even lattice L and γ ∈ L^∨, every integer multiple of level L is a period of θ_{γ+L}.

@[simp]

theorem ZLattice.IsEven.thetaCoset_level_vadd {E : Type u_1} [NormedAddCommGroup E] {L : Submodule ℤ E} [InnerProductSpace ℝ E] {γ : E} (hL : IsEven L) (hγ : γ ∈ dual L) (τ : UpperHalfPlane) : thetaCoset L γ (↑(level L) +ᵥ τ) = thetaCoset L γ τ

For an even lattice L and γ ∈ L^∨, θ_{γ+L} has period level L.

theorem ZLattice.IsEven.thetaCoset_slash_T_zpow_of_level_dvd {E : Type u_1} [NormedAddCommGroup E] {L : Submodule ℤ E} [InnerProductSpace ℝ E] {γ : E} (hL : IsEven L) (hγ : γ ∈ dual L) (k : ℤ) {N : ℤ} (hN : ↑(level L) ∣ N) : SlashAction.map k (ModularGroup.T ^ N) (thetaCoset L γ) = thetaCoset L γ

For an even lattice L and γ ∈ L^∨, θ_{γ+L} is invariant under T ^ N in every weight whenever (level L : ℤ) ∣ N.

theorem ZLattice.IsEven.thetaCoset_slash_T_zpow_level {E : Type u_1} [NormedAddCommGroup E] {L : Submodule ℤ E} [InnerProductSpace ℝ E] {γ : E} (hL : IsEven L) (hγ : γ ∈ dual L) (k : ℤ) : SlashAction.map k (ModularGroup.T ^ ↑(level L)) (thetaCoset L γ) = thetaCoset L γ

For an even lattice L and γ ∈ L^∨, θ_{γ+L} is invariant under T ^ (level L : ℤ) in every weight.

@[simp]

theorem ZLattice.IsEven.thetaCoset_slash_T_pow_level {E : Type u_1} [NormedAddCommGroup E] {L : Submodule ℤ E} [InnerProductSpace ℝ E] {γ : E} (hL : IsEven L) (hγ : γ ∈ dual L) (k : ℤ) : SlashAction.map k (ModularGroup.T ^ level L) (thetaCoset L γ) = thetaCoset L γ

For an even lattice L and γ ∈ L^∨, θ_{γ+L} is invariant under T ^ level L in every weight.

Integral lattices

theorem ZLattice.IsIntegral.thetaCoset_two_mul_intCast_vadd {E : Type u_1} [NormedAddCommGroup E] {L : Submodule ℤ E} [InnerProductSpace ℝ E] {γ : E} (hL : IsIntegral L) (hγ : γ ∈ dual L) (n : ℤ) (τ : UpperHalfPlane) : thetaCoset L γ (2 * ↑n +ᵥ τ) = Complex.exp (2 * ↑Real.pi * Complex.I * ↑(‖γ‖ ^ 2) * ↑n) * thetaCoset L γ τ

The translation law of the theta series of a coset of an integral lattice: for γ ∈ L^∨ and an integer n, θ_{γ+L}(τ + 2n) = exp (2 π i n ‖γ‖²) θ_{γ+L}(τ).

theorem ZLattice.IsIntegral.thetaCoset_two_vadd {E : Type u_1} [NormedAddCommGroup E] {L : Submodule ℤ E} [InnerProductSpace ℝ E] {γ : E} (hL : IsIntegral L) (hγ : γ ∈ dual L) (τ : UpperHalfPlane) : thetaCoset L γ (2 +ᵥ τ) = Complex.exp (2 * ↑Real.pi * Complex.I * ↑(‖γ‖ ^ 2)) * thetaCoset L γ τ

The translation law of the theta series of a coset of an integral lattice: for γ ∈ L^∨, θ_{γ+L}(τ + 2) = exp (2 π i ‖γ‖²) θ_{γ+L}(τ).

@[simp]

theorem ZLattice.IsIntegral.thetaSeries_two_mul_intCast_vadd {E : Type u_1} [NormedAddCommGroup E] {L : Submodule ℤ E} [InnerProductSpace ℝ E] (hL : IsIntegral L) (n : ℤ) (τ : UpperHalfPlane) : thetaSeries L (2 * ↑n +ᵥ τ) = thetaSeries L τ

The theta series of an integral lattice has period 2.

@[simp]

theorem ZLattice.IsIntegral.thetaSeries_two_vadd {E : Type u_1} [NormedAddCommGroup E] {L : Submodule ℤ E} [InnerProductSpace ℝ E] (hL : IsIntegral L) (τ : UpperHalfPlane) : thetaSeries L (2 +ᵥ τ) = thetaSeries L τ

The theta series of an integral lattice has period 2: Θ_L(τ + 2) = Θ_L(τ).

theorem ZLattice.IsIntegral.thetaCoset_slash_T_zpow_two_mul {E : Type u_1} [NormedAddCommGroup E] {L : Submodule ℤ E} [InnerProductSpace ℝ E] {γ : E} (hL : IsIntegral L) (hγ : γ ∈ dual L) (k n : ℤ) : SlashAction.map k (ModularGroup.T ^ (2 * n)) (thetaCoset L γ) = Complex.exp (2 * ↑Real.pi * Complex.I * ↑(‖γ‖ ^ 2) * ↑n) • thetaCoset L γ

The translation law of the theta series of a coset of an integral lattice, in slash form: for γ ∈ L^∨, every weight k and every integer n, θ_{γ+L} ∣[k] T ^ (2n) = exp (2 π i n ‖γ‖²) θ_{γ+L}.

@[simp]

theorem ZLattice.IsIntegral.thetaSeries_slash_T_sq {E : Type u_1} [NormedAddCommGroup E] {L : Submodule ℤ E} [InnerProductSpace ℝ E] (hL : IsIntegral L) (k : ℤ) : SlashAction.map k (ModularGroup.T ^ 2) (thetaSeries L) = thetaSeries L

The theta series of an integral lattice is invariant under T ^ 2, in every weight: Θ_L ∣[k] T ^ 2 = Θ_L.