A multiquadratic field lies in a cyclotomic field

This file proves the explicit Kronecker–Weber theorem for multiquadratic fields: the field generated over ℚ by square roots of rational numbers d₁, …, dₙ is contained in a cyclotomic field. Concretely, inside any field L of characteristic zero holding a primitive N-th root of unity ζ with 0 < N, every square root of an integer m with 4 |m| ∣ N already lies in ℚ(ζ).

The engine is the prime case: a square root of a prime p is assembled from a root of unity whose order is divisible by 4p. For odd p the quadratic Gauss sum supplies a square root of the prime discriminant p* = ±p (exists_mem_sq_eq_oddPrimeDiscriminant), and the fourth root of unity corrects its sign when p ≡ 3 (mod 4); for p = 2 the eighth root of unity supplies √2 directly (exists_mem_sq_eq_two). Multiplying square roots along a prime factorization reaches every positive integer, the fourth root of unity reaches the negative ones, and clearing denominators reaches every rational number. Since the two square roots of an element differ by a sign, every square root of such an m lies in the field, not just the constructed one. A zero radicand is excluded automatically: 4 · 0 ∣ N forces N = 0.

Taking L = ℂ makes the statement unconditional, provided every radicand is nonzero: for d i ≠ 0 and N = 4 ∏ᵢ |num dᵢ · den dᵢ| one may use ζ = exp (2 π i / N), so ℚ(√d₁, …, √dₙ) ⊆ ℚ(ζ_N) for any choice of square roots. Nonvanishing of the radicands is what makes this N positive. The existential form below needs no such hypothesis: a zero radicand has only the square root 0, so those indices are discarded before the order is formed. The target ℚ(ζ_N) is the N-th cyclotomic field: IntermediateField.isCyclotomicExtension_singleton_iff_eq_adjoin identifies it as a cyclotomic extension of ℚ.

No presentation by radicals need be assumed of the input field: exponent-two Kummer theory (TauCeti.Multiquadratic.exists_root_adjoin_range_eq_top) writes any finite Galois extension of ℚ whose Galois group has exponent dividing two as ℚ(√d₁, …, √dₙ) for rational dᵢ, so such a field admits a ℚ-algebra embedding into a cyclotomic field.

This is the multiquadratic case of the Kronecker–Weber theorem, which it makes explicit: the cyclotomic field is named, not merely asserted to exist. The general theorem, for every abelian extension of ℚ, is not proved here. For the classical account see K. Ireland and M. Rosen, A Classical Introduction to Modern Number Theory, Chapter 6.

Main results

• TauCeti.Multiquadratic.mem_of_sq_eq_intCast: every square root of an integer m lies in an intermediate field holding a primitive N-th root of unity, provided 0 < N and 4 |m| ∣ N.
• TauCeti.Multiquadratic.mem_of_sq_eq_ratCast: the same for a rational number.
• TauCeti.Multiquadratic.adjoin_range_le_of_sq_eq_ratCast: a multiquadratic field with rational radicands is contained in any such intermediate field.
• TauCeti.Multiquadratic.adjoin_range_le_adjoin_exp: over ℂ, for nonzero radicands, ℚ(√d₁, …, √dₙ) ⊆ ℚ(ζ_N) for the root of unity ζ_N = exp (2 π i / N) and the order N = 4 ∏ᵢ |num dᵢ · den dᵢ|.
• TauCeti.Multiquadratic.exists_isCyclotomicExtension_and_adjoin_range_le: every multiquadratic field with rational radicands lies in a cyclotomic field.
• TauCeti.Multiquadratic.exists_isCyclotomicExtension_and_nonempty_algHom: the abstract form — a finite Galois extension of ℚ whose Galois group has exponent dividing two admits a ℚ-algebra embedding into a cyclotomic extension of ℚ.

theorem TauCeti.Multiquadratic.exists_mem_sq_eq_prime {L : Type u_1} [Field L] [CharZero L] {F : IntermediateField ℚ L} {ζ : L} {N : ℕ} (hN : 0 < N) (hζ : IsPrimitiveRoot ζ N) (hmem : ζ ∈ F) {p : ℕ} (hp : Nat.Prime p) (hdvd : 4 * p ∣ N) : ∃ x ∈ F, x ^ 2 = ↑p

A root of unity of order divisible by 4p carries a square root of the prime p. The primitive N-th root of unity ζ is powered down to the roots of unity the construction needs, which 4 * p ∣ N makes available. For an odd prime the Gauss sum gives a square root of p* = ±p, and a primitive fourth root of unity repairs the sign; for p = 2 a primitive eighth root of unity gives √2.

theorem TauCeti.Multiquadratic.exists_mem_sq_eq_natCast {L : Type u_1} [Field L] [CharZero L] {F : IntermediateField ℚ L} {ζ : L} {N : ℕ} (hN : 0 < N) (hζ : IsPrimitiveRoot ζ N) (hmem : ζ ∈ F) {n : ℕ} (hdvd : 4 * n ∣ N) : ∃ x ∈ F, x ^ 2 = ↑n

A root of unity of order divisible by 4n carries a square root of n. The square roots of the prime factors of n multiply together.

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

A root of unity of order divisible by 4 |m| carries a square root of the integer m. A primitive fourth root of unity turns the square root of |m| into one of m.

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

Every square root of an integer lies in a field of roots of unity of matching order. If the intermediate field F contains a primitive N-th root of unity of positive order N and 4 |m| ∣ N, then both square roots of the integer m lie in F: the constructed one does, and the two differ by a sign.

theorem TauCeti.Multiquadratic.mem_of_sq_eq_ratCast {L : Type u_1} [Field L] [CharZero L] {F : IntermediateField ℚ L} {ζ : L} {N : ℕ} (hN : 0 < N) (hζ : IsPrimitiveRoot ζ N) (hmem : ζ ∈ F) {q : ℚ} (hdvd : 4 * (q.num * ↑q.den).natAbs ∣ N) {x : L} (hx : x ^ 2 = ↑q) : x ∈ F

Every square root of a rational number lies in a field of roots of unity of matching order. Clearing the denominator of q turns it into the integer q.num * q.den, whose square class it shares.

theorem TauCeti.Multiquadratic.adjoin_range_le_of_sq_eq_ratCast {L : Type u_1} [Field L] [CharZero L] {F : IntermediateField ℚ L} {ζ : L} {N : ℕ} {ι : Type u_2} (hN : 0 < N) (hζ : IsPrimitiveRoot ζ N) (hmem : ζ ∈ F) {d : ι → ℚ} {r : ι → L} (hr : ∀ (i : ι), r i ^ 2 = ↑(d i)) (hdvd : ∀ (i : ι), 4 * ((d i).num * ↑(d i).den).natAbs ∣ N) : IntermediateField.adjoin ℚ (Set.range r) ≤ F

A multiquadratic field lies in any field of roots of unity of matching order. If the intermediate field F of L / ℚ contains a primitive N-th root of unity of positive order N and, for each radicand d i, the order N is divisible by 4 |num (d i) · den (d i)|, then every field generated over ℚ by square roots r i of the d i is contained in F.

theorem TauCeti.Multiquadratic.adjoin_range_le_of_sq_eq_intCast {L : Type u_1} [Field L] [CharZero L] {F : IntermediateField ℚ L} {ζ : L} {N : ℕ} {ι : Type u_2} (hN : 0 < N) (hζ : IsPrimitiveRoot ζ N) (hmem : ζ ∈ F) {d : ι → ℤ} {r : ι → L} (hr : ∀ (i : ι), r i ^ 2 = ↑(d i)) (hdvd : ∀ (i : ι), 4 * (d i).natAbs ∣ N) : IntermediateField.adjoin ℚ (Set.range r) ≤ F

A multiquadratic field with integer radicands lies in any field of roots of unity of matching order. The integer analogue of adjoin_range_le_of_sq_eq_ratCast: the divisibility condition reads 4 |d i| ∣ N.

Over ℂ no root of unity need be assumed

theorem TauCeti.Multiquadratic.adjoin_range_le_adjoin_exp {ι : Type u_2} [Fintype ι] {d : ι → ℚ} {r : ι → ℂ} (hd : ∀ (i : ι), d i ≠ 0) (hr : ∀ (i : ι), r i ^ 2 = ↑(d i)) : IntermediateField.adjoin ℚ (Set.range r) ≤ ℚ⟮Complex.exp (2 * ↑Real.pi * Complex.I / ↑(4 * ∏ i : ι, ((d i).num * ↑(d i).den).natAbs))⟯

A multiquadratic field lies in the explicitly named cyclotomic field. For a finite family of nonzero rational radicands d i and any choice of complex square roots r i, the field ℚ(√d₁, …, √dₙ) is contained in ℚ(exp (2 π i / N)) for N = 4 ∏ᵢ |num (dᵢ) · den (dᵢ)|.

theorem TauCeti.Multiquadratic.exists_isCyclotomicExtension_and_adjoin_range_le {ι : Type u_2} [Finite ι] {d : ι → ℚ} {r : ι → ℂ} (hr : ∀ (i : ι), r i ^ 2 = ↑(d i)) : ∃ (N : ℕ), 0 < N ∧ ∃ (G : IntermediateField ℚ ℂ), IsCyclotomicExtension {N} ℚ ↥G ∧ IntermediateField.adjoin ℚ (Set.range r) ≤ G

Every multiquadratic field lies in a cyclotomic field. For a finite family of rational radicands d i and any choice of complex square roots r i, the field ℚ(√d₁, …, √dₙ) is contained in a cyclotomic extension of ℚ. The order and the field are named explicitly in adjoin_range_le_adjoin_exp, from which this existential form is deduced after discarding the zero radicands, whose square roots are 0.

This is the explicit Kronecker–Weber theorem for multiquadratic fields.

theorem TauCeti.Multiquadratic.exists_isCyclotomicExtension_and_nonempty_algHom (E : Type u_2) [Field E] [Algebra ℚ E] [FiniteDimensional ℚ E] [IsGalois ℚ E] (hexp : Monoid.exponent Gal(E/ℚ) ∣ 2) : ∃ (N : ℕ), 0 < N ∧ ∃ (G : IntermediateField ℚ ℂ), IsCyclotomicExtension {N} ℚ ↥G ∧ Nonempty (E →ₐ[ℚ] ↥G)

Every multiquadratic field embeds in a cyclotomic field. Let E / ℚ be a finite Galois extension whose Galois group has exponent dividing two. Then there is a cyclotomic extension G of ℚ inside ℂ and a ℚ-algebra embedding of E into G.

This is the abstract form of the containment above: nothing is assumed about how E is presented, only about the shape of its Galois group. Exponent-two Kummer theory (exists_root_adjoin_range_eq_top) supplies rational radicands and square roots generating E, a complex embedding carries them into ℂ, and exists_isCyclotomicExtension_and_adjoin_range_le places the image in a cyclotomic field.