Maximality of the candidate genus field

Let d be a squarefree integer that is not a rational square, let M / ℚ be an abelian number field extension, and let y ∈ M be a square root of d generating a quadratic subfield F = ℚ(√d) of M. If M / F is unramified at every finite prime, then M embeds over ℚ into the candidate genus field candidateGenusField hd. Since that field is itself such an extension — it is abelian over ℚ, contains a square root of d, and is unramified over ℚ(√d) at every finite prime — this makes it the largest one, which is the maximality half of the genus-field characterisation.

The proof combines three inputs, one field-theoretic and two arithmetic.

• exists_squarefree_root_adjoin_range_eq_top_of_isUnramifiedIn_over_quadratic presents M as ℚ(√a₁, …, √aₙ) for square-class independent squarefree integers aᵢ.
• dvd_fundamentalDiscriminant_base_of_dvd_subfield and not_dvd_fundamentalDiscriminant_mul_of_dvd_subfield constrain each aᵢ: every prime ramifying in ℚ(√aᵢ) ramifies in ℚ(√d), and none of them ramifies in ℚ(√(aᵢ d)).
• subset_of_forall_prime_dvd_fundamentalDiscriminant turns those two constraints into the statement that the prime-discriminant factorization of fundamentalDiscriminant aᵢ is a subset of the chosen factorization genusPrimeDiscriminants hd, whence √aᵢ lies in the compositum.

An aᵢ in the square class of d is not covered by the second constraint — there ℚ(√(aᵢ d)) = ℚ — and is handled separately, by scaling the square root of d that the candidate genus field already contains.

Once every generator has a square root inside candidateGenusField hd, any embedding M →ₐ[ℚ] ℂ sends the generators to ± those square roots, hence lands inside the candidate genus field; comparing degrees gives [M : ℚ] ≤ 2 ^ t with t the number of primes ramifying in ℚ(√d).

This is the classical maximality argument for the genus field; 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

In the namespace TauCeti.Multiquadratic:

• exists_mem_candidateGenusField_sq_eq_intCast: a quadratic subfield ℚ(√a) of such an M has its square root inside the candidate genus field.
• nonempty_algHom_candidateGenusField: M embeds over ℚ into the candidate genus field.
• finrank_le_finrank_candidateGenusField: hence [M : ℚ] ≤ [K_gen : ℚ], and finrank_le_two_pow_card_genusPrimeDiscriminants reads that bound off as 2 ^ t.
• nonempty_algEquiv_candidateGenusField: an extension attaining the bound is ℚ-isomorphic to the candidate genus field.
• exists_isUnramifiedIn_and_finrank_eq_two_pow_card: the candidate genus field is itself such an extension, so the bound is attained and the uniqueness statement is not vacuous.

theorem TauCeti.Multiquadratic.exists_mem_candidateGenusField_sq_eq_intCast_of_subset {d a : ℤ} (hd : Squarefree d) {u : Finset ℤ} (huprod : ∏ P ∈ u, P = fundamentalDiscriminant a) (hsub : u ⊆ genusPrimeDiscriminants hd) : ∃ z ∈ candidateGenusField hd, z ^ 2 = ↑a

A subset of the chosen prime discriminants generates a square root inside the candidate genus field. If the prime discriminants in u ⊆ genusPrimeDiscriminants hd have product fundamentalDiscriminant a, then candidateGenusField hd contains an element squaring to a.

theorem TauCeti.Multiquadratic.exists_mem_candidateGenusField_sq_eq_intCast {M : Type u_1} [Field M] [NumberField M] [IsGalois ℚ M] {d a : ℤ} (hd : Squarefree d) (hnsqd : ¬IsSquare ↑d) (hsfa : Squarefree a) {x y : M} (hx : x ^ 2 = (algebraMap ℤ M) a) (hy : y ^ 2 = (algebraMap ℤ M) d) (hunr : ∀ (q : Ideal (NumberField.RingOfIntegers ↥ℚ⟮y⟯)), q.IsPrime → q ≠ ⊥ → Algebra.IsUnramifiedIn (NumberField.RingOfIntegers M) q) : ∃ z ∈ candidateGenusField hd, z ^ 2 = ↑a

A quadratic subfield of an unramified Galois extension lies in the candidate genus field. Let M / ℚ be Galois, let y ∈ M be a square root of a squarefree non-square d generating a quadratic subfield, and assume M is unramified over that subfield at every finite prime. Then for every squarefree a with a square root in M, the candidate genus field candidateGenusField hd contains an element squaring to a.

This is the arithmetic core of maximality: the discriminant of ℚ(√a) is a subproduct of the prime-discriminant factorization of the discriminant of ℚ(√d).

theorem TauCeti.Multiquadratic.nonempty_algHom_candidateGenusField {M : Type u_1} [Field M] [NumberField M] [IsAbelianGalois ℚ M] {d : ℤ} (hd : Squarefree d) (hnsqd : ¬IsSquare ↑d) {y : M} (hy : y ^ 2 = (algebraMap ℤ M) d) (hunr : ∀ (q : Ideal (NumberField.RingOfIntegers ↥ℚ⟮y⟯)), q.IsPrime → q ≠ ⊥ → Algebra.IsUnramifiedIn (NumberField.RingOfIntegers M) q) : Nonempty (M →ₐ[ℚ] ↥(candidateGenusField hd))

Maximality of the candidate genus field. Let M / ℚ be an abelian number-field extension containing a square root y of a squarefree non-square d that generates a quadratic subfield, and suppose M is unramified over that subfield at every finite prime. Then M admits a ℚ-embedding into candidateGenusField hd.

Together with the facts that candidateGenusField hd is itself abelian over ℚ, contains a square root of d, and is unramified over ℚ(√d) at every finite prime, this says it is the largest such extension — the maximality half of the genus-field characterisation.

theorem TauCeti.Multiquadratic.finrank_le_finrank_candidateGenusField {M : Type u_1} [Field M] [NumberField M] [IsAbelianGalois ℚ M] {d : ℤ} (hd : Squarefree d) (hnsqd : ¬IsSquare ↑d) {y : M} (hy : y ^ 2 = (algebraMap ℤ M) d) (hunr : ∀ (q : Ideal (NumberField.RingOfIntegers ↥ℚ⟮y⟯)), q.IsPrime → q ≠ ⊥ → Algebra.IsUnramifiedIn (NumberField.RingOfIntegers M) q) : Module.finrank ℚ M ≤ Module.finrank ℚ ↥(candidateGenusField hd)

The degree bound from maximality. Under the hypotheses of nonempty_algHom_candidateGenusField, the degree of M over ℚ is at most the degree of the candidate genus field.

theorem TauCeti.Multiquadratic.finrank_le_two_pow_card_genusPrimeDiscriminants {M : Type u_1} [Field M] [NumberField M] [IsAbelianGalois ℚ M] {d : ℤ} (hd : Squarefree d) (hnsqd : ¬IsSquare ↑d) {y : M} (hy : y ^ 2 = (algebraMap ℤ M) d) (hunr : ∀ (q : Ideal (NumberField.RingOfIntegers ↥ℚ⟮y⟯)), q.IsPrime → q ≠ ⊥ → Algebra.IsUnramifiedIn (NumberField.RingOfIntegers M) q) : Module.finrank ℚ M ≤ 2 ^ (genusPrimeDiscriminants hd).card

[M : ℚ] ≤ 2 ^ t. An abelian extension of ℚ that is unramified at every finite prime over its quadratic subfield ℚ(√d) has degree at most 2 ^ t, where t is the number of prime discriminants dividing fundamentalDiscriminant d — equivalently, by card_genusPrimeDiscriminants_eq_ncard_ramifiedPrimes, the number of rational primes ramifying in ℚ(√d). The bound is attained by the candidate genus field itself.

theorem TauCeti.Multiquadratic.nonempty_algEquiv_candidateGenusField {M : Type u_1} [Field M] [NumberField M] [IsAbelianGalois ℚ M] {d : ℤ} (hd : Squarefree d) (hnsqd : ¬IsSquare ↑d) {y : M} (hy : y ^ 2 = (algebraMap ℤ M) d) (hunr : ∀ (q : Ideal (NumberField.RingOfIntegers ↥ℚ⟮y⟯)), q.IsPrime → q ≠ ⊥ → Algebra.IsUnramifiedIn (NumberField.RingOfIntegers M) q) (hfr : Module.finrank ℚ M = 2 ^ (genusPrimeDiscriminants hd).card) : Nonempty (M ≃ₐ[ℚ] ↥(candidateGenusField hd))

Uniqueness at the maximal degree. An abelian extension of ℚ that is unramified at every finite prime over its quadratic subfield ℚ(√d) and attains the maximal degree 2 ^ t is ℚ-isomorphic to the candidate genus field: the embedding of nonempty_algHom_candidateGenusField is then forced to be onto.

theorem TauCeti.Multiquadratic.exists_isUnramifiedIn_and_finrank_eq_two_pow_card {d : ℤ} (hd : Squarefree d) (hnsq : ¬IsSquare ↑d) : ∃ (y : ↥(candidateGenusField hd)), y ^ 2 = (algebraMap ℤ ↥(candidateGenusField hd)) d ∧ Module.finrank ℚ ↥ℚ⟮y⟯ = 2 ∧ (∀ (q : Ideal (NumberField.RingOfIntegers ↥ℚ⟮y⟯)), q.IsPrime → q ≠ ⊥ → Algebra.IsUnramifiedIn (NumberField.RingOfIntegers ↥(candidateGenusField hd)) q) ∧ Module.finrank ℚ ↥(candidateGenusField hd) = 2 ^ (genusPrimeDiscriminants hd).card

The maximality bound is attained. The candidate genus field of ℚ(√d) is itself an abelian extension of ℚ of the kind the bound governs: its chosen square root of d generates a quadratic subfield over which it is unramified at every finite prime, and its degree over ℚ is exactly 2 ^ t. So the bound finrank_le_two_pow_card_genusPrimeDiscriminants is sharp, and nonempty_algEquiv_candidateGenusField applies to a nonempty class of extensions.