Unramified abelian extensions of quadratic fields are multiquadratic

Let M / ℚ be an abelian number-field extension and let F be a quadratic intermediate field. If M / F is unramified at every finite prime, then Gal(M / ℚ) has exponent dividing two and M is generated over ℚ by square roots of a square-class independent family of squarefree integers.

This is the first half of the maximality argument for the candidate genus field. Given an extension of a quadratic field unramified at every finite prime that is abelian over ℚ, the inertia subgroups of Gal(M / ℚ) generate the whole group. Unramifiedness over F makes each inertia subgroup disjoint from Gal(M / F), so every inertia element is killed by [F : ℚ] = 2. Thus the whole Galois group has exponent dividing two. Exponent-two Kummer theory then presents M as a multiquadratic extension of ℚ. Rational radicands are reduced to squarefree integers so the output is ready for the discriminant arithmetic in the next step.

The remaining half of maximality is arithmetic: identify the quadratic subfields in this presentation from their discriminants and embed them in the prime-discriminant compositum candidateGenusField hd. The discriminant constraints those subfields satisfy are TauCeti/NumberTheory/Multiquadratic/Unramified/Subfields.lean.

This is the classical reduction in the genus-field construction; see D. A. Cox, Primes of the Form x² + ny², §6.A, and F. Lemmermeyer, Reciprocity Laws: From Euler to Eisenstein, §2.2.

Main results

• exists_squarefree_root_adjoin_range_eq_top_of_isUnramifiedIn_over_quadratic: such a number field is generated by square roots of square-class independent squarefree integer radicands.

theorem TauCeti.Multiquadratic.exists_squarefree_root_adjoin_range_eq_top_of_isUnramifiedIn_over_quadratic {M : Type u_1} [Field M] [NumberField M] [IsAbelianGalois ℚ M] (F : IntermediateField ℚ M) (hF : Module.finrank ℚ ↥F = 2) (hunr : ∀ (q : Ideal (NumberField.RingOfIntegers ↥F)), q.IsPrime → q ≠ ⊥ → Algebra.IsUnramifiedIn (NumberField.RingOfIntegers M) q) : ∃ (n : ℕ) (a : Fin n → ℤ) (root : Fin n → M), (∀ (i : Fin n), Squarefree (a i)) ∧ (∀ (i : Fin n), root i ^ 2 = (algebraMap ℚ M) ↑(a i)) ∧ (∀ (S : Finset (Fin n)), S.Nonempty → ¬IsSquare (∏ i ∈ S, a i)) ∧ IntermediateField.adjoin ℚ (Set.range root) = ⊤ ∧ Module.finrank ℚ M = 2 ^ n

An abelian extension unramified over a quadratic field is generated by square roots of squarefree integers. Let M / ℚ be an abelian number-field extension containing a quadratic intermediate field F. If every finite prime of F is unramified in M, then there are square-class independent squarefree integers a₁, …, aₙ and chosen square roots in M which generate all of M; in particular [M : ℚ] = 2ⁿ. Independence is stated integrally: no nonempty subset product of the aᵢ is a square in ℤ.

This is the field-theoretic reduction in the maximality proof for the candidate genus field. The squarefree integral output is the form needed to compare the quadratic factors by their fundamental discriminants.