Quadratic subfields of a prime-discriminant compositum

Let D i be distinct prime discriminants, with at most one even member, and let root i be square roots of their radicands. Every quadratic subfield of the multiquadratic compositum ℚ(root i : i) is generated by a product of a unique nonempty subset of the roots. This file combines the field-generic subset-product classification of Subfield/Classification with the arithmetic of prime discriminants: the discriminant of the subfield indexed by S is exactly ∏ i ∈ S, D i.

The arithmetic input is that a subset product of prime-discriminant radicands is squarefree and has fundamental discriminant ∏ i ∈ S, D i. The at-most-one-even hypothesis is what rules out the pair 8, -8, whose radicands are not coprime.

The prime-discriminant description is classical; 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

• TauCeti.Multiquadratic.fundamentalDiscriminant_prod_primeDiscriminantRadicands: the fundamental discriminant of a subset product of prime-discriminant radicands is the product of the corresponding prime discriminants; the companion squarefree_prod_primeDiscriminantRadicands_of_forall_isEvenPrimeDiscriminant_eq records that such a product is squarefree.
• TauCeti.Multiquadratic.discr_adjoin_prod_root_primeDiscriminants: the quadratic subfield generated by a subset product has that product as its field discriminant.
• TauCeti.Multiquadratic.exists_finset_discr_eq_of_finrank_two_primeDiscriminants: every quadratic subfield of the compositum arises in this way.

theorem TauCeti.Multiquadratic.squarefree_prod_primeDiscriminantRadicands_of_forall_isEvenPrimeDiscriminant_eq {ι : Type u_1} {D : ι → ℤ} {S : Finset ι} (hD : ∀ i ∈ S, IsPrimeDiscriminant (D i)) (hinj : Set.InjOn D ↑S) (heven : ∀ i ∈ S, ∀ j ∈ S, IsEvenPrimeDiscriminant (D i) → IsEvenPrimeDiscriminant (D j) → D i = D j) : Squarefree (∏ i ∈ S, primeDiscriminantRadicand (D i))

Products of radicands indexed by distinct prime discriminants with at most one even member are squarefree. The at-most-one-even condition excludes the sole non-coprime pair of distinct prime-discriminant radicands, those attached to 8 and -8.

theorem TauCeti.Multiquadratic.fundamentalDiscriminant_prod_primeDiscriminantRadicands {ι : Type u_1} {D : ι → ℤ} {S : Finset ι} (hD : ∀ i ∈ S, IsPrimeDiscriminant (D i)) (hinj : Set.InjOn D ↑S) (heven : ∀ i ∈ S, ∀ j ∈ S, IsEvenPrimeDiscriminant (D i) → IsEvenPrimeDiscriminant (D j) → D i = D j) : fundamentalDiscriminant (∏ i ∈ S, primeDiscriminantRadicand (D i)) = ∏ i ∈ S, D i

Fundamental discriminant of a subset product of prime-discriminant radicands. For a distinct family of prime discriminants with at most one even member,

fundamentalDiscriminant (∏ i ∈ S, radicand (D i)) = ∏ i ∈ S, D i.

The even factor is the load-bearing point: if it is present, it contributes the unique factor 4 removed by primeDiscriminantRadicand; all other factors are odd and congruent to 1 modulo 4. If no even factor is present, every radicand is already its prime discriminant.

theorem TauCeti.Multiquadratic.discr_adjoin_prod_root_primeDiscriminants {ι : Type u_1} {D : ι → ℤ} {S : Finset ι} {L : Type u_2} [Field L] [CharZero L] {root : ι → L} (hS : S.Nonempty) (hD : ∀ i ∈ S, IsPrimeDiscriminant (D i)) (hinj : Set.InjOn D ↑S) (heven : ∀ i ∈ S, ∀ j ∈ S, IsEvenPrimeDiscriminant (D i) → IsEvenPrimeDiscriminant (D j) → D i = D j) (hroot : ∀ i ∈ S, root i ^ 2 = (algebraMap ℚ L) ↑(primeDiscriminantRadicand (D i))) : have hxint := ⋯; NumberField.discr ↥ℚ⟮∏ i ∈ S, root i⟯ = ∏ i ∈ S, D i

Discriminant of a subset-product quadratic subfield. The quadratic subfield generated by ∏ i ∈ S, root i has field discriminant ∏ i ∈ S, D i. Only the members of S are constrained: the discriminants indexed by S must be distinct prime discriminants with at most one even member, and root i must be a square root of the radicand of D i for i ∈ S. The ambient field need only have characteristic zero; the subfield is a number field because the product root is integral.

theorem TauCeti.Multiquadratic.exists_finset_discr_eq_of_finrank_two_primeDiscriminants {ι : Type u_1} (D : ι → ℤ) {L : Type u_2} [Field L] [CharZero L] (hD : ∀ (i : ι), IsPrimeDiscriminant (D i)) (hinj : Function.Injective D) (heven : ∀ (i j : ι), IsEvenPrimeDiscriminant (D i) → IsEvenPrimeDiscriminant (D j) → D i = D j) (root : ι → L) (hroot : ∀ (i : ι), root i ^ 2 = (algebraMap ℚ L) ↑(primeDiscriminantRadicand (D i))) [NumberField L] [Finite ι] (htop : IntermediateField.adjoin ℚ (Set.range root) = ⊤) (F : IntermediateField ℚ L) (hF : Module.finrank ℚ ↥F = 2) : ∃ (S : Finset ι), S.Nonempty ∧ F = ℚ⟮∏ i ∈ S, root i⟯ ∧ NumberField.discr ↥F = ∏ i ∈ S, D i

Quadratic subfields of a prime-discriminant compositum. Suppose the chosen roots generate the ambient number field. Every quadratic intermediate field is generated by the product of a nonempty subset of those roots, and its field discriminant is the product of the corresponding prime discriminants.