Documentation

TauCeti.NumberTheory.ModularForms.ThetaSeries.Reciprocity

The reciprocity law for Gauss sums of an even lattice #

Let L be an even lattice in a real inner product space E of even dimension n = 2k, and write e(x) = exp (2 π i x). For positive integers a and c, the Gauss sum G_L(a, c) = ∑_{y ∈ L/cL} e(a ‖y‖² / (2c)) (ZLattice.gaussSum) satisfies the reciprocity law

G_L(a, c) = (c/a)^k (covol L)⁻¹ e(n/8) ∑_{y ∈ L^∨/aL} e(-c ‖y‖² / (2a)),

which exchanges the modulus c and the coefficient a at the price of passing to the dual lattice L^∨. Here e(n/8) = i^k, and (covol L)⁻¹ = (det L)^{-1/2} is the inverse square root of the order of the discriminant group L^∨/L (ZLattice.IsIntegral.inv_covolume_eq_inv_sqrt_card_discriminantGroup). No coprimality of a and c is needed.

The proof is analytic. The behaviour of t^k Θ_L(a/c + i t) as t → 0⁺ is computed in two ways. Splitting L into its classes modulo cL gives the limit G_L(a, c) / (c^{2k} covol L) (ZLattice.IsEven.tendsto_pow_mul_thetaSeries_nhdsGT). On the other hand, the inversion law Θ_L(z) = (covol L)⁻¹ (-i)^k (-1/z)^k Θ_{L^∨}(-1/z) moves the point z = a/c + i t to -1/z = -c/a + ε, where ε = -1/w with w = -a/c + i a² / (c² t), so ε tends to the cusp 0 with im (-1/ε) → ∞. Splitting L^∨ into its classes modulo aL then gives the limit (a/c)^k i^k (∑_{y ∈ L^∨/aL} e(-c ‖y‖² / (2a))) / (a^{2k} covol(L)²), by the asymptotic ZLattice.IsEven.tendsto_pow_mul_thetaSeries_dual_vadd_comap_S. Comparing the two limits gives the law. The comparison is between limits of sums, not of their leading terms alone: G_L(a, c) may vanish while Θ_L(a/c + i t) does not.

At a = c = 1 the left side is 1, and complex conjugation gives Milgram's formula ∑_{γ ∈ L^∨/L} e(‖γ‖² / 2) = √|L^∨/L| · e(n/8) for a positive definite even lattice (ZLattice.IsEven.sum_discriminantQuadraticChar).

Main statements #

References #

theorem ZLattice.IsEven.gaussSum_eq_mul_dualGaussSum {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {L : Submodule ℤ E} [DiscreteTopology ↥L] [IsZLattice ℝ L] {k : ℕ} (hL : IsEven L) [MeasurableSpace E] [BorelSpace E] (hk : Module.finrank ℝ E = 2 * k) (a c : ℕ) [NeZero a] [NeZero c] [Fintype (↥(dual L) ⧸ (↑a • L).submoduleOf (dual L))] :
gaussSum L hL (↑a) c = (↑c / ↑a) ^ k * (↑(covolume L MeasureTheory.volume))⁻¹ * Complex.I ^ k * dualGaussSum L hL (-↑c) a

The reciprocity law for the Gauss sums of an even lattice. If L is an even lattice and dim E = 2k, then for positive integers a and c, G_L(a, c) = (c/a)^k (covol L)⁻¹ i^k ∑_{y ∈ L^∨/aL} e(-c ‖y‖² / (2a)). Here i^k = e(n/8) for n = 2k, and (covol L)⁻¹ = (det L)^{-1/2}.