Gauss sums under isotropic reduction

For a quadratic-isotropic subgroup H of a finite quadratic module A, the Gauss sum satisfies G(A) = |H| G(H⊥ / H). Averaging translations by H cancels the contributions outside H⊥, and each class in the quotient has |H| representatives. This identity requires isotropy for the quadratic form itself, rather than just for its polar pairing. It holds for degenerate modules too.

For nondegenerate A, the order identity |H⊥ / H| |H|² = |A| shows that the normalized Gauss sums agree, so isotropic reduction preserves the Gauss-sum invariant. This permits recursive calculations of Gauss sums of finite quadratic forms by reducing their exponents.

The reduction is most often applied to the n-torsion A[n], whose orthogonal complement in a nondegenerate module is nA. When A[n] is quadratic-isotropic this gives |A[n]| G(A) = ∑_y e^{2πi q(n y)}, with no quotient module to identify: if moreover q_A(n y) = q_B(r y) for a surjective homomorphism r : A → B onto a nondegenerate module B, then A and B have the same Gauss-sum invariant. For Nikulin's cyclic generators on ℤ/p^{k+2}, with k ≥ 1 when p = 2, taking n = p and r the reduction to ℤ/p^k lowers the exponent by two.

Main declarations

• TauCeti.FiniteQuadraticModule.gaussSum_eq_card_mul_gaussSum_orthogonalQuotient: G(A) = |H| G(H⊥ / H) for a quadratic-isotropic H.
• TauCeti.FiniteQuadraticModule.gaussSign_orthogonalQuotient: isotropic reduction preserves the Gauss-sum invariant.
• TauCeti.FiniteQuadraticModule.IsNondegenerate.natCard_ker_zsmul_mul_gaussSum: |A[n]| G(A) = ∑_y e^{2πi q(n y)} when A[n] is quadratic-isotropic.
• TauCeti.FiniteQuadraticModule.gaussSign_eq_of_quadratic_zsmul_eq: the Gauss-sum invariant is unchanged along multiplication by n followed by a reduction.

References

• C. T. C. Wall, Quadratic forms on finite groups, and related topics, Topology 2 (1963), 281–298.
• J. Milnor and D. Husemoller, Symmetric Bilinear Forms, Appendix 4.

theorem TauCeti.FiniteQuadraticModule.gaussSum_eq_card_mul_gaussSum_orthogonalQuotient (A : FiniteQuadraticModule) {H : AddSubgroup A.carrier} (hH : A.IsIsotropic H) : A.gaussSum = ↑(Nat.card ↥H) * (A.orthogonalQuotient H hH).gaussSum

Gauss sums under isotropic reduction. For a quadratic-isotropic subgroup H, G(A) = |H| G(H⊥ / H). Nondegeneracy is unnecessary.

@[simp]

theorem TauCeti.FiniteQuadraticModule.gaussSign_orthogonalQuotient (A : FiniteQuadraticModule) {H : AddSubgroup A.carrier} (hA : A.IsNondegenerate) (hH : A.IsIsotropic H) : (A.orthogonalQuotient H hH).gaussSign = A.gaussSign

Isotropic reduction preserves the Gauss-sum invariant of a nondegenerate finite quadratic module.

theorem TauCeti.FiniteQuadraticModule.IsNondegenerate.natCard_ker_zsmul_mul_gaussSum {A : FiniteQuadraticModule} [Fintype A.carrier] (hA : A.IsNondegenerate) (n : ℤ) (hH : A.IsIsotropic (zsmulAddGroupHom n).ker) : ↑(Nat.card ↥(zsmulAddGroupHom n).ker) * A.gaussSum = ∑ y : A.carrier, expCircle (A.quadratic (n • y))

Gauss sums under multiplication by n. If the n-torsion A[n] of a nondegenerate module is quadratic-isotropic, then |A[n]| G(A) = ∑_y e^{2πi q(n y)}. The orthogonal complement of A[n] is nA, so G(A) is the sum over nA, and y ↦ n y covers nA exactly |A[n]| times.

theorem TauCeti.FiniteQuadraticModule.gaussSign_eq_of_quadratic_zsmul_eq {A : FiniteQuadraticModule} {B : FiniteQuadraticModule} (hA : A.IsNondegenerate) (hB : B.IsNondegenerate) (n : ℤ) (hH : A.IsIsotropic (zsmulAddGroupHom n).ker) (r : A.carrier →+ B.carrier) (hr : Function.Surjective ⇑r) (hq : ∀ (y : A.carrier), A.quadratic (n • y) = B.quadratic (r y)) : A.gaussSign = B.gaussSign

The Gauss-sum invariant along multiplication by n. Let A and B be nondegenerate, let the n-torsion of A be quadratic-isotropic, and let r : A → B be a surjective homomorphism with q_A(n y) = q_B(r y). Then sign A = sign B, because both |A[n]| G(A) and |ker r| G(B) equal ∑_y e^{2πi q_A(n y)}.

For Nikulin's cyclic generators on A = ℤ/p^{k+2}, with k ≥ 1 when p = 2, taking n = p and r the reduction to B = ℤ/p^k lowers the exponent by two.