Milgram's theorem

For an even nondegenerate integral lattice L with signature (t₊, t₀, t₋), the Gauss-sum invariant sign q_L ∈ ℤ/8 of its discriminant quadratic form, defined by ∑_{a ∈ A_L} e^{2πi q_L(a)} = √#A_L · e^{2πi·sign(q_L)/8}, is

sign q_L ≡ t₊ - t₋ (mod 8).

This is Milgram's theorem (Nikulin, Theorem 1.3.3). In particular an even unimodular lattice, whose discriminant form is zero, has 8 ∣ t₊ - t₋.

The proof

Both sides are additive over orthogonal sums and invariant under isometry, and the left side is unchanged under passing to a full sublattice (TauCeti.IntegralLattice.gaussSign_discriminantQuadraticModule_restrictFull). A nondegenerate lattice of positive rank has a vector x of nonzero norm 2m, and the sublattice ℤx + (x^⊥ ∩ L) has finite index in L and is isometric to ⟨2m⟩ ⊥ (x^⊥ ∩ L). Induction on the rank therefore reduces the theorem to the rank-one lattices ⟨2m⟩. For those the Gauss sum is half of a classical quadratic Gauss sum of modulus 4|m|,

∑_{k < 2m} e^{2πi k² / (4m)} = (1 + i) √m = √(2m) · e^{2πi/8}     (m > 0),

by Gauss's evaluation (TauCeti.sum_range_two_mul_cexp_two_pi_I_sq_div_four_mul), and ⟨2m⟩ for m < 0 is the negative of ⟨-2m⟩.

Main results

• TauCeti.IntegralLattice.gaussSign_discriminantQuadraticModule_rankOne: the Gauss-sum invariant of ⟨2m⟩ is the sign of m.
• TauCeti.IntegralLattice.gaussSign_discriminantQuadraticModule_eq_sigPos_sub_sigNeg: Milgram's theorem.
• TauCeti.IntegralLattice.eight_dvd_sigPos_sub_sigNeg_of_isUnimodular: the signature of an even unimodular lattice is divisible by 8.
• TauCeti.IntegralLattice.eight_dvd_finrank_of_isEven_isUnimodular_isPosDef: the rank of a positive definite even unimodular lattice is divisible by 8.

References

• V. V. Nikulin, Integral symmetric bilinear forms and some of their applications, Theorem 1.3.3.
• J. Milnor and D. Husemoller, Symmetric Bilinear Forms, Appendix 4.
• J.-P. Serre, A Course in Arithmetic, Chapter V, §2.

The rank-one lattices ⟨2m⟩

theorem TauCeti.IntegralLattice.gaussSign_discriminantQuadraticModule_rankOne (m : ℤ) [NeZero m] : ((rankOne (2 * m)).discriminantQuadraticModule ⋯).gaussSign = ↑m.sign

Milgram's theorem for ⟨2m⟩: the discriminant form of the rank-one lattice ⟨2m⟩ has Gauss-sum invariant the sign of m.

Splitting off a vector of nonzero norm, up to finite index

Milgram's theorem

theorem TauCeti.IntegralLattice.gaussSign_discriminantQuadraticModule_eq_sigPos_sub_sigNeg {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) [L.IsNondegenerate] (hL : L.IsEven) : (L.discriminantQuadraticModule hL).gaussSign = ↑L.sigPos - ↑L.sigNeg

Milgram's theorem. The Gauss-sum invariant of the discriminant form of an even nondegenerate lattice is its signature t₊ - t₋ modulo 8.

theorem TauCeti.IntegralLattice.eight_dvd_sigPos_sub_sigNeg_of_isUnimodular {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) (hL : L.IsEven) (hU : L.IsUnimodular) : 8 ∣ ↑L.sigPos - ↑L.sigNeg

The signature of an even unimodular lattice is divisible by 8. Its discriminant form is zero, so Milgram's theorem gives t₊ - t₋ ≡ 0 (mod 8).

theorem TauCeti.IntegralLattice.eight_dvd_finrank_of_isEven_isUnimodular_isPosDef {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) (hE : L.IsEven) (hU : L.IsUnimodular) (hP : L.IsPosDef) : 8 ∣ Module.finrank ℚ V

The rank of any positive definite even unimodular integral lattice is divisible by eight.