Documentation

TauCeti.LinearAlgebra.FiniteBilinearModule.Dyadic.GaussSum

Gauss sums of the dyadic generators #

Nikulin's dyadic generators are the cyclic forms q_θ^{(2)}(2^k) on ℤ/2^k, for odd θ and k ≥ 1, with q(x) = θx² / 2^{k+1}, and the rank-two forms u^{(2)}(2^k) and v^{(2)}(2^k) on (ℤ/2^k)², with q(x) = x₁x₂ / 2^k and q(x) = (x₁² + x₁x₂ + x₂²) / 2^k. This file computes their Gauss-sum invariants, which are the dyadic values of Nikulin's Proposition 1.11.2:

sign q_θ^{(2)}(2^k) ≡ θ + 4kω(θ),   where ω(θ) = (θ² - 1) / 8,
sign u^{(2)}(2^k)   ≡ 0,
sign v^{(2)}(2^k)   ≡ 4k            (mod 8),

together with the Gauss sums 2^k of u^{(2)}(2^k) and (-2)^k of v^{(2)}(2^k).

The first coordinate axis of u^{(2)}(2^k) is a quadratic Lagrangian, so that module is metabolic. Isotropy for the polar pairing alone would not suffice to determine the Gauss sum.

The other two families are reduced by two in the exponent. In q_θ^{(2)}(2^{k+2}), with k ≥ 1, and in v^{(2)}(2^{k+2}), the 2-torsion is quadratic-isotropic, and q(2y) is the form of the same generator of exponent 2^k evaluated on the reduction of y; by TauCeti.FiniteQuadraticModule.gaussSign_eq_of_quadratic_zsmul_eq the invariant does not change. The base cases are explicit sums: q_θ^{(2)}(2) has Gauss sum 1 + e^{2πiθ/4}, which is the Gauss sum of the discriminant form of ⟨2⟩ or of its negative according to θ modulo 4; q_θ^{(2)}(4) has Gauss sum 2e^{2πiθ/8}; v^{(2)}(1) is trivial; and v^{(2)}(2) has Gauss sum -2, because its form takes the value 1/2 on the three nonzero elements of (ℤ/2)².

Main declarations #

References #

source
@[simp]
theorem TauCeti.FiniteQuadraticModule.gaussSum_dyadicU (k : ℕ) :
(dyadicU k).gaussSum = 2 ^ k

The Gauss sum of u^{(2)}(2^k) is 2^k, in the half-norm convention.

source
@[simp]
theorem TauCeti.FiniteQuadraticModule.gaussSign_dyadicU (k : ℕ) :
(dyadicU k).gaussSign = 0

Nikulin's Gauss-sum invariant of u^{(2)}(2^k) is zero.

Reduction of the exponent by two #

Base cases #

The values on the dyadic generators #

source
@[simp]
theorem TauCeti.FiniteQuadraticModule.gaussSign_dyadicCyclic (k : ℕ) [NeZero k] {θ : ℤ} (hθ : Odd θ) :
(dyadicCyclic k θ).gaussSign = ↑(θ + 4 * ↑k * ((θ ^ 2 - 1) / 8))

The Gauss-sum invariant of q_θ^{(2)}(2^k) is θ + 4kω(θ) for odd θ and k ≥ 1, where ω(θ) = (θ² - 1) / 8. This is Nikulin's value sign q_θ^{(2)}(2^k) ≡ θ + 4kω(θ) (mod 8); it depends only on θ modulo 8 and on the parity of k.

source
theorem TauCeti.FiniteQuadraticModule.gaussSign_dyadicCyclic_one_eq_one_or_eq_neg_one {θ : ℤ} (hθ : Odd θ) :
(dyadicCyclic 1 θ).gaussSign = 1 ∨ (dyadicCyclic 1 θ).gaussSign = -1

The Gauss-sum invariant of q_θ^{(2)}(2) is ±1 for odd θ: it is 1 for θ ≡ 1 (mod 4) and -1 for θ ≡ 3 (mod 4).

source
@[simp]
theorem TauCeti.FiniteQuadraticModule.gaussSign_dyadicV (k : ℕ) :
(dyadicV k).gaussSign = 4 * ↑k

The Gauss-sum invariant of v^{(2)}(2^k) is 4k. This is Nikulin's value sign v^{(2)}(2^k) ≡ 4k (mod 8); it also holds at k = 0, where the module is trivial.

source
@[simp]
theorem TauCeti.FiniteQuadraticModule.gaussSum_dyadicV (k : ℕ) :
(dyadicV k).gaussSum = (-2) ^ k

The Gauss sum of v^{(2)}(2^k) is (-2)^k, in the half-norm convention.

Scaled Gauss sums of the rank-two generators #

source
theorem TauCeti.FiniteQuadraticModule.scaledGaussSum_dyadicU_pow_add (j e : ℕ) :
(dyadicU (j + e)).scaledGaussSum (2 ^ j) = 2 ^ (2 * j) * (dyadicU e).gaussSum

The 2^j-scaled Gauss sum of u^{(2)}(2^{j+e}) is 2^{2j} times the Gauss sum of u^{(2)}(2^e): coordinatewise reduction modulo 2^e has 2^{2j} elements in every fiber.

source
theorem TauCeti.FiniteQuadraticModule.scaledGaussSum_dyadicV_pow_add (j e : ℕ) :
(dyadicV (j + e)).scaledGaussSum (2 ^ j) = 2 ^ (2 * j) * (dyadicV e).gaussSum

The 2^j-scaled Gauss sum of v^{(2)}(2^{j+e}) is 2^{2j} times the Gauss sum of v^{(2)}(2^e): coordinatewise reduction modulo 2^e has 2^{2j} elements in every fiber.