Gauss sums on a translate of a bilinear Lagrangian #
Let H be a Lagrangian for the polar pairing of a finite quadratic module. If the quadratic
form is constant on a + H, its Gauss sum is #H · expCircle (q(a)). The subgroup need not
be isotropic for the quadratic form. The phase on its translate records the characteristic
norm in the discriminant form of the even sublattice of an odd unimodular lattice.
The character-averaging argument follows
TauCeti.FiniteQuadraticModule.gaussSum_restrict_orthogonalComplement.
References #
- J. Milnor and D. Husemoller, Symmetric Bilinear Forms, Appendix 4.
theorem
TauCeti.FiniteQuadraticModule.gaussSum_eq_natCard_mul_expCircle_of_bilinear_isLagrangian
{A : FiniteQuadraticModule}
{H : AddSubgroup A.carrier}
(a : A.carrier)
(hH : A.IsLagrangian H)
(ha : ∀ (h : ↥H), A.quadratic (a + ↑h) = A.quadratic a)
:
If the quadratic form is constant on a translate of a Lagrangian for its polar pairing, the Gauss sum is the subgroup's order times the exponential of that constant.