Square roots of prime discriminants in a field of roots of unity

This file extracts the square roots of the prime discriminants from roots of unity. Let L be a field of characteristic zero and let F be an intermediate field of L / ℚ.

• if F contains a primitive p-th root of unity for an odd prime p, it contains a square root of the odd prime discriminant p* = (-1)^((p-1)/2) p;
• if F contains a primitive fourth root of unity, it contains a square root of -1;
• if F contains a primitive eighth root of unity, it contains square roots of 2 and -2.

Up to rational squares these are all the prime discriminants, since -4 = -1 · 2² and ±8 = ±2 · 2², and they are the arithmetic input to the containment of a multiquadratic field in a cyclotomic field.

The odd case is the classical quadratic Gauss sum g = ∑_{a} (a/p) ζ^a, whose square is p*. Mathlib's gaussSum_sq already computes g² as χ(-1) times the cardinality of the source, for any nontrivial quadratic character χ and primitive additive character ψ valued in a domain; specialising χ to the quadratic character of ZMod p pushed into L and ψ to the additive character attached to ζ (AddChar.zmodChar) turns that computation into the statement above, since (-1/p) = (-1)^((p-1)/2). Mathlib uses this only in positive characteristic, where the Gauss sum produces the quadratic reciprocity law; here the target is characteristic zero, where it produces a square root.

The even cases are direct computations: a primitive fourth root of unity squares to -1 (its square is a primitive square root of unity), and for a primitive eighth root of unity ζ the elements ζ + ζ⁷ and ζ + ζ³ square to 2 and -2, because ζ⁴ = -1.

For the classical account of the quadratic Gauss sum see K. Ireland and M. Rosen, A Classical Introduction to Modern Number Theory, Chapter 6.

Main results

• TauCeti.Multiquadratic.exists_mem_sq_eq_oddPrimeDiscriminant: a primitive p-th root of unity carries a square root of p*.
• TauCeti.Multiquadratic.exists_mem_sq_eq_neg_one: a primitive fourth root of unity is a square root of -1.
• TauCeti.Multiquadratic.exists_mem_sq_eq_two: a primitive eighth root of unity carries a square root of 2.
• TauCeti.Multiquadratic.exists_mem_sq_eq_neg_two: a primitive eighth root of unity carries a square root of -2.

theorem TauCeti.Multiquadratic.exists_mem_sq_eq_oddPrimeDiscriminant {L : Type u_1} [Field L] [CharZero L] {F : IntermediateField ℚ L} {ζ : L} {p : ℕ} (hp : Nat.Prime p) (hp2 : p ≠ 2) (hζ : IsPrimitiveRoot ζ p) (hmem : ζ ∈ F) : ∃ x ∈ F, x ^ 2 = ↑(oddPrimeDiscriminant p)

The quadratic Gauss sum is a square root of the prime discriminant. If an intermediate field F of L / ℚ contains a primitive p-th root of unity for an odd prime p, then it contains a square root of the odd prime discriminant p*.

The witness is the Gauss sum ∑_{a : ZMod p} (a/p) ζ^a, a ℤ-linear combination of powers of ζ; gaussSum_sq evaluates its square as (-1/p) · p, which is p*.

theorem TauCeti.Multiquadratic.exists_mem_sq_eq_neg_one {L : Type u_1} [Field L] [CharZero L] {F : IntermediateField ℚ L} {ζ : L} (hζ : IsPrimitiveRoot ζ 4) (hmem : ζ ∈ F) : ∃ x ∈ F, x ^ 2 = -1

A primitive fourth root of unity is a square root of -1.

theorem TauCeti.Multiquadratic.exists_mem_sq_eq_two {L : Type u_1} [Field L] [CharZero L] {F : IntermediateField ℚ L} {ζ : L} (hζ : IsPrimitiveRoot ζ 8) (hmem : ζ ∈ F) : ∃ x ∈ F, x ^ 2 = 2

A primitive eighth root of unity carries a square root of 2. The witness is ζ + ζ⁷ = ζ + ζ⁻¹, whose square is ζ² + 2 + ζ⁻², and ζ⁻² = -ζ² because ζ⁴ = -1.

theorem TauCeti.Multiquadratic.exists_mem_sq_eq_neg_two {L : Type u_1} [Field L] [CharZero L] {F : IntermediateField ℚ L} {ζ : L} (hζ : IsPrimitiveRoot ζ 8) (hmem : ζ ∈ F) : ∃ x ∈ F, x ^ 2 = -2

A primitive eighth root of unity carries a square root of -2. The witness is ζ + ζ³, whose square is ζ² + 2ζ⁴ + ζ⁶, and ζ⁶ = -ζ² because ζ⁴ = -1.