Gauss sums of even overlattices

For even nondegenerate lattices L ≤ M in the same rational quadratic space, the Gauss sums of their discriminant forms satisfy G(q_L) = [M : L] G(q_M). Their Gauss-sum invariants are consequently equal. The discriminant form of M is the orthogonal quotient along the quadratic-isotropic subgroup M / L, so these are applications of isotropic reduction to the canonical discriminant modules.

The invariance permits comparisons of discriminant Gauss sums through even overlattices without changing the rational quadratic space, as needed when comparing them to signature. Read from the other side, it says that restricting an even lattice to a full sublattice (TauCeti.IntegralLattice.restrictFull) does not change the Gauss-sum invariant. No definiteness hypothesis is required.

References

• V. V. Nikulin, Integral symmetric bilinear forms and some of their applications, §1.4.
• J. Milnor and D. Husemoller, Symmetric Bilinear Forms, Appendix 4.

theorem TauCeti.IntegralLattice.IntermediateCarrier.gaussSum_discriminantQuadraticModule_eq_index_mul {V : Type u_1} [AddCommGroup V] [Module ℚ V] {L : IntegralLattice V} [L.IsNondegenerate] {M : ↑L.IntermediateCarrier} (hL : L.IsEven) (hM : IsEven M) : (L.discriminantQuadraticModule hL).gaussSum = ↑(index M) * (⋯.toIntegralLattice.discriminantQuadraticModule ⋯).gaussSum

The Gauss sum of the discriminant form of an even lattice is the index of an even overlattice times the Gauss sum of that overlattice's discriminant form.

@[simp]

theorem TauCeti.IntegralLattice.IntermediateCarrier.gaussSign_discriminantQuadraticModule {V : Type u_1} [AddCommGroup V] [Module ℚ V] {L : IntegralLattice V} [L.IsNondegenerate] {M : ↑L.IntermediateCarrier} (hL : L.IsEven) (hM : IsEven M) : (⋯.toIntegralLattice.discriminantQuadraticModule ⋯).gaussSign = (L.discriminantQuadraticModule hL).gaussSign

Passing to an even overlattice preserves the Gauss-sum invariant of the discriminant quadratic form.

@[simp]

theorem TauCeti.IntegralLattice.gaussSign_discriminantQuadraticModule_restrictFull {V : Type u_1} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) [L.IsNondegenerate] (hL : L.IsEven) (N : Submodule ℤ V) (hN : N ≤ L.carrier) [Submodule.IsLattice ℚ N] : ((L.restrictFull N hN).discriminantQuadraticModule ⋯).gaussSign = (L.discriminantQuadraticModule hL).gaussSign

Passing to a full sublattice preserves the Gauss-sum invariant of the discriminant quadratic form of an even nondegenerate lattice.