Gauss sums of prime-discriminant characters

The Gauss sum of the Dirichlet character primeDiscriminantChar P hP of a prime discriminant P, formed with a primitive |P|-th root of unity in a field of characteristic zero, squares to P. It is therefore an explicit square root of P built out of roots of unity, which is how the quadratic fields ℚ(√P) are located inside cyclotomic fields.

The computation is classical; see K. Ireland and M. Rosen, A Classical Introduction to Modern Number Theory, Chapter 6, and D. A. Cox, Primes of the Form x² + ny², §3.B.

Main results

• TauCeti.Multiquadratic.primeDiscriminantChar_neg_one: the character of P takes the value sign P at -1.
• TauCeti.Multiquadratic.gaussSumOfPrimitiveRoot_primeDiscriminantChar_sq: the Gauss sum of the character of a prime discriminant P squares to P.

@[simp]

theorem TauCeti.Multiquadratic.primeDiscriminantChar_neg_one {P : ℤ} (hP : IsPrimeDiscriminant P) : (primeDiscriminantChar P hP) (-1) = P.sign

The character of a prime discriminant P takes the value sign P at -1.

@[simp]

theorem TauCeti.Multiquadratic.gaussSumOfPrimitiveRoot_primeDiscriminantChar_sq {L : Type u_1} [Field L] [CharZero L] {P : ℤ} (hP : IsPrimeDiscriminant P) [NeZero P.natAbs] {ζ : L} (hζ : IsPrimitiveRoot ζ P.natAbs) : (primeDiscriminantChar P hP).gaussSumOfPrimitiveRoot hζ ^ 2 = ↑P

The Gauss sum of a prime discriminant squares to it. In any field of characteristic zero, the Gauss sum of the character of the prime discriminant P, formed with a primitive |P|-th root of unity, is a square root of P.