A quadratic field lies in the cyclotomic field of its discriminant

Let D be a fundamental discriminant. The quadratic field ℚ(√D) lies in the cyclotomic field ℚ(ζ_|D|): inside any field L of characteristic zero, an intermediate field of L / ℚ holding a primitive N-th root of unity with |D| ∣ N contains both square roots of D. For a squarefree integer d this says ℚ(√d) ⊆ ℚ(ζ_|D|) with D = fundamentalDiscriminant d, which is d or 4d. The same level carries the whole genus field: the compositum of the quadratic fields of the prime discriminants dividing D also lies in ℚ(ζ_|D|).

This sharpens TauCeti.Multiquadratic.mem_of_sq_eq_intCast, which asks for the order 4 |m| for a square root of an integer m. That order is never needed for a fundamental discriminant: √-3 already lies in ℚ(ζ₃) and √5 in ℚ(ζ₅), where the cruder bound asks for ζ₁₂ and ζ₂₀. Classically |D| is the conductor of ℚ(√D), the least such level; this file proves the containment only, not the minimality.

The proof is factor by factor. A fundamental discriminant is a product of prime discriminants (Int.IsFundamentalDiscr.exists_finset_primeDiscriminant), each of which divides it. An odd prime discriminant p* has a square root in ℚ(ζ_p), namely a quadratic Gauss sum (exists_mem_sq_eq_oddPrimeDiscriminant); the even prime discriminants -4, 8, -8 have square roots in ℚ(ζ₄) and ℚ(ζ₈) (exists_mem_sq_eq_neg_one, exists_mem_sq_eq_two, exists_mem_sq_eq_neg_two). Multiplying these square roots together gives one of D.

For the classical account 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², §6.A.

Main results

• TauCeti.Multiquadratic.mem_of_sq_eq_primeDiscriminantRadicand: the square roots of the radicand of a prime discriminant P lie in any field holding a primitive N-th root of unity with |P| ∣ N.
• TauCeti.Multiquadratic.mem_of_sq_eq_of_isFundamentalDiscr: the square roots of a fundamental discriminant D lie in any field holding a primitive N-th root of unity with |D| ∣ N.
• TauCeti.Multiquadratic.mem_of_sq_eq_of_squarefree: the square roots of a squarefree integer d lie in any such field with |fundamentalDiscriminant d| ∣ N.
• TauCeti.Multiquadratic.candidateGenusField_le_of_isPrimitiveRoot: the same containment for the prime-discriminant compositum candidateGenusField.
• TauCeti.Multiquadratic.adjoin_simple_le_adjoin_exp_of_isFundamentalDiscr and TauCeti.Multiquadratic.candidateGenusField_le_adjoin_exp: over ℂ, the quadratic field and the prime-discriminant compositum lie in ℚ(exp (2πi / |D|)).

theorem TauCeti.Multiquadratic.exists_mem_sq_eq_primeDiscriminantRadicand {L : Type u_1} [Field L] [CharZero L] {F : IntermediateField ℚ L} {ζ : L} {N : ℕ} (hN : 0 < N) (hζ : IsPrimitiveRoot ζ N) (hmem : ζ ∈ F) {P : ℤ} (hP : IsPrimeDiscriminant P) (hdvd : P.natAbs ∣ N) : ∃ x ∈ F, x ^ 2 = ↑(primeDiscriminantRadicand P)

A root of unity of order divisible by |P| carries a square root of the radicand of the prime discriminant P. The radicands of -4, 8, -8 are -1, 2, -2, whose square roots come from a primitive fourth or eighth root of unity; the radicand of an odd prime discriminant p* is p* itself, whose square root is a Gauss sum over a primitive p-th root of unity.

theorem TauCeti.Multiquadratic.mem_of_sq_eq_primeDiscriminantRadicand {L : Type u_1} [Field L] [CharZero L] {F : IntermediateField ℚ L} {ζ : L} {N : ℕ} (hN : 0 < N) (hζ : IsPrimitiveRoot ζ N) (hmem : ζ ∈ F) {P : ℤ} (hP : IsPrimeDiscriminant P) (hdvd : P.natAbs ∣ N) {x : L} (hx : x ^ 2 = ↑(primeDiscriminantRadicand P)) : x ∈ F

Every square root of the radicand of a prime discriminant P lies in a field of roots of unity of order divisible by |P|.

theorem TauCeti.Multiquadratic.exists_mem_sq_eq_of_isPrimeDiscriminant {L : Type u_1} [Field L] [CharZero L] {F : IntermediateField ℚ L} {ζ : L} {N : ℕ} (hN : 0 < N) (hζ : IsPrimitiveRoot ζ N) (hmem : ζ ∈ F) {P : ℤ} (hP : IsPrimeDiscriminant P) (hdvd : P.natAbs ∣ N) : ∃ x ∈ F, x ^ 2 = ↑P

A root of unity of order divisible by |P| carries a square root of the prime discriminant P. The prime discriminant is its radicand, or four times its radicand in the even cases.

theorem TauCeti.Multiquadratic.exists_mem_sq_eq_of_isFundamentalDiscr {L : Type u_1} [Field L] [CharZero L] {F : IntermediateField ℚ L} {ζ : L} {N : ℕ} (hN : 0 < N) (hζ : IsPrimitiveRoot ζ N) (hmem : ζ ∈ F) {D : ℤ} (hD : D.IsFundamentalDiscr) (hdvd : D.natAbs ∣ N) : ∃ x ∈ F, x ^ 2 = ↑D

A root of unity of order divisible by |D| carries a square root of the fundamental discriminant D. The square roots of the prime-discriminant factors of D multiply together; each factor divides D, so its absolute value divides the order.

theorem TauCeti.Multiquadratic.mem_of_sq_eq_of_isFundamentalDiscr {L : Type u_1} [Field L] [CharZero L] {F : IntermediateField ℚ L} {ζ : L} {N : ℕ} (hN : 0 < N) (hζ : IsPrimitiveRoot ζ N) (hmem : ζ ∈ F) {D : ℤ} (hD : D.IsFundamentalDiscr) (hdvd : D.natAbs ∣ N) {x : L} (hx : x ^ 2 = ↑D) : x ∈ F

Every square root of a fundamental discriminant D lies in a field of roots of unity of order divisible by |D|. In particular ℚ(√D) ⊆ ℚ(ζ_|D|).

theorem TauCeti.Multiquadratic.mem_of_sq_eq_of_squarefree {L : Type u_1} [Field L] [CharZero L] {F : IntermediateField ℚ L} {ζ : L} {N : ℕ} (hN : 0 < N) (hζ : IsPrimitiveRoot ζ N) (hmem : ζ ∈ F) {d : ℤ} (hd : Squarefree d) (hdvd : (fundamentalDiscriminant d).natAbs ∣ N) {x : L} (hx : x ^ 2 = ↑d) : x ∈ F

Every square root of a squarefree integer d lies in a field of roots of unity of order divisible by the absolute value of its fundamental discriminant. Since fundamentalDiscriminant d = c² d with c ∈ {1, 2}, a square root x of d gives the square root c x of the fundamental discriminant.

theorem TauCeti.Multiquadratic.candidateGenusField_le_of_isPrimitiveRoot {N : ℕ} {d : ℤ} (hd : Squarefree d) {F : IntermediateField ℚ ℂ} {ζ : ℂ} (hN : 0 < N) (hζ : IsPrimitiveRoot ζ N) (hmem : ζ ∈ F) (hdvd : (fundamentalDiscriminant d).natAbs ∣ N) : candidateGenusField hd ≤ F

The candidate genus field of ℚ(√d) lies in any field of roots of unity of order divisible by the absolute value of the fundamental discriminant of d. Each of its generators is a square root of the radicand of a prime discriminant dividing fundamentalDiscriminant d.

Over ℂ: the cyclotomic field ℚ(exp (2πi / |D|))

theorem TauCeti.Multiquadratic.adjoin_simple_le_adjoin_exp_of_isFundamentalDiscr {D : ℤ} (hD : D.IsFundamentalDiscr) {x : ℂ} (hx : x ^ 2 = ↑D) : ℚ⟮x⟯ ≤ ℚ⟮Complex.exp (2 * ↑Real.pi * Complex.I / ↑D.natAbs)⟯

A quadratic field lies in the cyclotomic field of its discriminant. For a fundamental discriminant D and a complex square root x of D, ℚ(x) ⊆ ℚ(exp (2πi / |D|)).

theorem TauCeti.Multiquadratic.candidateGenusField_le_adjoin_exp {d : ℤ} (hd : Squarefree d) : candidateGenusField hd ≤ ℚ⟮Complex.exp (2 * ↑Real.pi * Complex.I / ↑(fundamentalDiscriminant d).natAbs)⟯

The candidate genus field of ℚ(√d) lies in the cyclotomic field of the discriminant. For squarefree d with fundamental discriminant D, the compositum of the quadratic fields of the prime discriminants dividing D is contained in ℚ(exp (2πi / |D|)).

Inside a cyclotomic subfield of ℂ of level |D|

theorem TauCeti.Multiquadratic.genusFieldRoot_mem_of_isCyclotomicExtension {d : ℤ} (hd : Squarefree d) (K : IntermediateField ℚ ℂ) [IsCyclotomicExtension {(∏ P ∈ genusPrimeDiscriminants hd, P).natAbs} ℚ ↥K] (P : ↥(genusPrimeDiscriminants hd)) : genusFieldRoot hd P ∈ K

Every chosen root of the candidate genus field lies in a cyclotomic subfield of ℂ of level |D|.

noncomputable def TauCeti.Multiquadratic.genusFieldRootOfPrimeDiscriminant {d : ℤ} (hd : Squarefree d) (K : IntermediateField ℚ ℂ) [IsCyclotomicExtension {(∏ P ∈ genusPrimeDiscriminants hd, P).natAbs} ℚ ↥K] (P : ↥(genusPrimeDiscriminants hd)) : ↥K

A square root of the prime discriminant P itself, inside the cyclotomic field K.

@[simp]

theorem TauCeti.Multiquadratic.genusFieldRootOfPrimeDiscriminant_sq {d : ℤ} (hd : Squarefree d) (K : IntermediateField ℚ ℂ) [IsCyclotomicExtension {(∏ P ∈ genusPrimeDiscriminants hd, P).natAbs} ℚ ↥K] (P : ↥(genusPrimeDiscriminants hd)) : genusFieldRootOfPrimeDiscriminant hd K P ^ 2 = ↑↑P

The rescaled root squares to the prime discriminant.

theorem TauCeti.Multiquadratic.map_adjoin_range_genusFieldRootOfPrimeDiscriminant {d : ℤ} (hd : Squarefree d) (K : IntermediateField ℚ ℂ) [IsCyclotomicExtension {(∏ P ∈ genusPrimeDiscriminants hd, P).natAbs} ℚ ↥K] : IntermediateField.map K.val (IntermediateField.adjoin ℚ (Set.range (genusFieldRootOfPrimeDiscriminant hd K))) = candidateGenusField hd

The rescaled roots generate the candidate genus field. Viewed in ℂ, the compositum of the square roots of the prime discriminants dividing D is the candidate genus field of ℚ(√d): each rescaled root is a rational multiple of a chosen root and conversely.