Degree of the candidate genus field

For a squarefree integer d, candidateGenusField hd is the compositum of the quadratic fields attached to the prime discriminants in genusPrimeDiscriminants hd. This file proves that this compositum has the full multiquadratic degree

[candidateGenusField hd : ℚ] = 2 ^ (genusPrimeDiscriminants hd).card.

The defining properties of genusPrimeDiscriminants hd say that its members are prime discriminants and that at most one is even. Their radicands are therefore square-class independent (not_isSquare_prod_genusPrimeDiscriminantRadicands), and the degree formula is the corresponding specialization of finrank_adjoin_range.

This is the degree step in proving that the candidate genus field is multiquadratic. For negative d, isGenusField_candidateGenusField identifies this candidate with the maximal extension satisfying the genus-field ramification conditions. The real case remains future work.

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

Main results

• TauCeti.Multiquadratic.not_isSquare_prod_genusPrimeDiscriminantRadicands: the radicands of the chosen prime discriminants are square-class independent.
• TauCeti.Multiquadratic.finiteDimensional_candidateGenusField: the candidate genus field is a finite extension of ℚ.
• TauCeti.Multiquadratic.finrank_candidateGenusField: its degree over ℚ is 2 to the number of prime discriminants in its chosen factorization.
• TauCeti.Multiquadratic.adjoin_range_candidateGenusFieldGen_eq_top: the chosen roots generate it: adjoining their range to ℚ gives all of it.

theorem TauCeti.Multiquadratic.not_isSquare_prod_genusPrimeDiscriminantRadicands {d : ℤ} (hd : Squarefree d) (S : Finset ↥(genusPrimeDiscriminants hd)) (hS : S.Nonempty) : ¬IsSquare (∏ P ∈ S, ↑(primeDiscriminantRadicand ↑P))

Square-class independence of the chosen radicands. No nonempty subset product of the radicands of the prime discriminants in genusPrimeDiscriminants hd is a rational square: the chosen factorization consists of distinct prime discriminants, at most one of them even.

instance TauCeti.Multiquadratic.finiteDimensional_candidateGenusField {d : ℤ} {hd : Squarefree d} : FiniteDimensional ℚ ↥(candidateGenusField hd)

The candidate genus field is finite-dimensional over ℚ.

instance TauCeti.Multiquadratic.numberField_candidateGenusField {d : ℤ} {hd : Squarefree d} : NumberField ↥(candidateGenusField hd)

The candidate genus field is a number field: a finite extension of ℚ (inside ℂ).

theorem TauCeti.Multiquadratic.finrank_candidateGenusField {d : ℤ} (hd : Squarefree d) : Module.finrank ℚ ↥(candidateGenusField hd) = 2 ^ (genusPrimeDiscriminants hd).card

Degree of the candidate genus field. If d is squarefree, adjoining the chosen square roots of the radicands of the prime discriminants in genusPrimeDiscriminants hd gives an extension of ℚ of degree 2 ^ (genusPrimeDiscriminants hd).card. Thus the candidate genus field has the full degree predicted by square-class independence.

theorem TauCeti.Multiquadratic.adjoin_range_candidateGenusFieldGen_eq_top {d : ℤ} (hd : Squarefree d) : IntermediateField.adjoin ℚ (Set.range (candidateGenusFieldGen hd)) = ⊤

The chosen roots generate the candidate genus field: adjoining their range to ℚ inside candidateGenusField hd gives all of it.