Constructing a square root of the radicand in the candidate genus field

For an integer d, the candidate genus field of ℚ(√d) is the compositum of the quadratic fields ℚ(√(radicand D*)) over the prime discriminants D* dividing the fundamental discriminant fundamentalDiscriminant d. This file proves the square-class fact underlying the genus-field construction: that compositum contains an element squaring to d. The canonical GenusField module identifies this compositum with the imaginary quadratic genus field; here we establish the square-root input used by that characterization.

The argument is a square-class computation. Writing M = adjoin ℚ (root) for the roots of the radicands, the product of all the roots squares to the product of the radicands, which — because each prime discriminant is its radicand or four times it, and fundamentalDiscriminant d = c² · d — lies in the square class of d. Scaling that product root by the appropriate rational produces an element of M squaring to d.

Combined with the degree theorem Prime/Discriminant/Independence (the compositum has degree 2ᵗ), this is a step toward exhibiting the genus field as a multiquadratic extension of ℚ(√d).

The description of the genus field as the compositum of the prime-discriminant quadratic fields is classical; see D. A. Cox, Primes of the Form x² + ny², and F. Lemmermeyer, Reciprocity Laws.

Main results

• TauCeti.Multiquadratic.exists_mem_adjoin_sq_eq_of_prod_primeDiscriminant_eq: for a finset of integers (in the application, prime discriminants) whose product is fundamentalDiscriminant d, the compositum of the roots of their radicands contains an element squaring to d.
• TauCeti.Multiquadratic.exists_finset_primeDiscriminant_and_exists_mem_adjoin_sq_eq_of_squarefree packages that with the factorization: for squarefree d, the prime-discriminant factorization of fundamentalDiscriminant d exists (with its at-most-one-even property) and its radicand compositum contains an element squaring to d.

theorem TauCeti.Multiquadratic.exists_prod_radicand_eq_sq_mul_of_prod_primeDiscriminant_eq {d : ℤ} {s : Finset ℤ} (hprod : ∏ P ∈ s, P = fundamentalDiscriminant d) : ∃ (a : ℚ), a ≠ 0 ∧ ∏ P ∈ s.attach, ↑(primeDiscriminantRadicand ↑P) = a ^ 2 * ↑d

The product of the radicands of a finset of integers (in the application, prime discriminants) whose product is fundamentalDiscriminant d is a nonzero rational square times d.

theorem TauCeti.Multiquadratic.exists_mem_adjoin_sq_eq_of_prod_primeDiscriminant_eq {d : ℤ} {s : Finset ℤ} (hprod : ∏ P ∈ s, P = fundamentalDiscriminant d) {L : Type u_1} [Field L] [Algebra ℚ L] (root : ↥s → L) (hroot : ∀ (P : ↥s), root P ^ 2 = (algebraMap ℚ L) ↑(primeDiscriminantRadicand ↑P)) : ∃ x ∈ IntermediateField.adjoin ℚ (Set.range root), x ^ 2 = (algebraMap ℚ L) ↑d

A square root of d in the prime-discriminant compositum. Let d : ℤ and let s be a finite set of integers whose product is the fundamental discriminant fundamentalDiscriminant d (in the application, the prime discriminants dividing it). For any chosen square roots root of the radicands of the members of s in a field L over ℚ, the compositum adjoin ℚ (Set.range root) contains an element squaring to d. This is the square-class containment underlying the genus-field construction.

theorem TauCeti.Multiquadratic.exists_finset_primeDiscriminant_and_exists_mem_adjoin_sq_eq_of_squarefree {d : ℤ} (hd : Squarefree d) : ∃ (s : Finset ℤ), (∀ P ∈ s, IsPrimeDiscriminant P) ∧ (∀ P ∈ s, ∀ Q ∈ s, IsEvenPrimeDiscriminant P → IsEvenPrimeDiscriminant Q → P = Q) ∧ ∏ P ∈ s, P = fundamentalDiscriminant d ∧ ∀ {L : Type u_1} [inst : Field L] [inst_1 : Algebra ℚ L] (root : ↥s → L), (∀ (P : ↥s), root P ^ 2 = (algebraMap ℚ L) ↑(primeDiscriminantRadicand ↑P)) → ∃ x ∈ IntermediateField.adjoin ℚ (Set.range root), x ^ 2 = (algebraMap ℚ L) ↑d

The prime-discriminant compositum of a squarefree radicand contains a square root of d. For squarefree d, the fundamental discriminant fundamentalDiscriminant d factors into a finite set s of prime discriminants, and for any roots of their radicands the compositum contains an element squaring to d. This packages exists_mem_adjoin_sq_eq_of_prod_primeDiscriminant_eq with the factorization Int.IsFundamentalDiscr.exists_finset_primeDiscriminant, so callers need only supply d squarefree.