Square-class independence of prime discriminants

The genus-field layer of the multiquadratic roadmap builds the genus field of ℚ(√d) as the compositum of the quadratic fields ℚ(√D*) over the prime discriminants D* dividing the discriminant of ℚ(√d). To know this compositum is multiquadratic of full degree 2ᵗ (and so to apply the degree theorem TauCeti.Multiquadratic.finrank_adjoin_range), one needs the prime discriminants to be square-class independent: no nonempty subset product of their radicands is a rational square.

This file supplies that independence. The natural prime-discriminant criterion is that the family is injective and does not contain all three even prime discriminants -4, 8, and -8: those three radicands multiply to the square 4, while every proper subfamily of the even radicands is independent. The fundamental-discriminant specialization has at most one even factor, hence satisfies this criterion automatically.

Main results

• TauCeti.Multiquadratic.squarefree_prod_primeDiscriminantRadicands_of_pairwise_isCoprime: a subset product of pairwise coprime prime-discriminant radicands is squarefree.
• TauCeti.Multiquadratic.isCoprime_primeDiscriminantRadicand: the radicands of two distinct prime discriminants are coprime except for the pair 8, -8.
• TauCeti.Multiquadratic.not_isSquare_prod_primeDiscriminantRadicands: for an injective family of prime discriminants not containing all of -4, 8, and -8, no nonempty subset product of their radicands is a rational square — square-class independence in the form the degree theorem consumes.
• TauCeti.Multiquadratic.finrank_adjoin_roots_primeDiscriminantRadicands: the multiquadratic compositum of the roots of radicand D i over such a family has degree 2^|ι|.
• The _of_forall_isEvenPrimeDiscriminant_eq variants: the same independence and degree theorems under an at most one even prime discriminant hypothesis.

theorem TauCeti.Multiquadratic.squarefree_prod_primeDiscriminantRadicands_of_pairwise_isCoprime {ι : Type u_1} {D : ι → ℤ} {S : Finset ι} (hD : ∀ i ∈ S, IsPrimeDiscriminant (D i)) (hcop : ∀ i ∈ S, ∀ j ∈ S, i ≠ j → IsCoprime (primeDiscriminantRadicand (D i)) (primeDiscriminantRadicand (D j))) : Squarefree (∏ i ∈ S, primeDiscriminantRadicand (D i))

Squarefreeness of a subset product of prime-discriminant radicands. A product over S of prime-discriminant radicands is squarefree as soon as the selected radicands are pairwise coprime. Only the discriminants indexed by S are constrained.

Apart from the squarefreeness theorem, the block of helpers above is intentionally local to this file; the public API continues with the coprimality theorem below.

theorem TauCeti.Multiquadratic.isCoprime_primeDiscriminantRadicand {D E : ℤ} (hD : IsPrimeDiscriminant D) (hE : IsPrimeDiscriminant E) (hDE : D ≠ E) (hnot : ¬(D = 8 ∧ E = -8 ∨ D = -8 ∧ E = 8)) : IsCoprime (primeDiscriminantRadicand D) (primeDiscriminantRadicand E)

Coprimality of distinct prime-discriminant radicands. The radicands of two distinct prime discriminants are coprime except for the ordered exceptional pairs 8, -8 and -8, 8. Their absolute values are 1, 2 (the even radicands), or distinct odd primes (the odd ones); the only non-coprime distinct even radicands are 2 and -2.

theorem TauCeti.Multiquadratic.not_isSquare_prod_primeDiscriminantRadicands {ι : Type u_1} (D : ι → ℤ) (hD : ∀ (i : ι), IsPrimeDiscriminant (D i)) (hinj : Function.Injective D) (heven : ¬((∃ (i : ι), D i = -4) ∧ (∃ (i : ι), D i = 8) ∧ ∃ (i : ι), D i = -8)) (S : Finset ι) : S.Nonempty → ¬IsSquare (∏ i ∈ S, ↑(primeDiscriminantRadicand (D i)))

Square-class independence of prime discriminants. Let D : ι → ℤ be an injective family of prime discriminants which does not contain all three even prime discriminants -4, 8, and -8. Then no nonempty subset product of the radicands primeDiscriminantRadicand (D i) is a rational square. This is the hindep hypothesis the multiquadratic degree theorem finrank_adjoin_range consumes, applied to the genus-field generators.

theorem TauCeti.Multiquadratic.not_all_three_evenPrimeDiscriminants_of_forall_isEvenPrimeDiscriminant_eq {ι : Type u_1} {D : ι → ℤ} (heven_unique : ∀ (i j : ι), IsEvenPrimeDiscriminant (D i) → IsEvenPrimeDiscriminant (D j) → D i = D j) : ¬((∃ (i : ι), D i = -4) ∧ (∃ (i : ι), D i = 8) ∧ ∃ (i : ι), D i = -8)

A prime-discriminant family with at most one even prime discriminant cannot contain the three even prime discriminants -4, 8, and -8 simultaneously.

The hypothesis is stated extensionally: any two indices whose discriminants are even prime discriminants must carry the same discriminant value. This is the form supplied by the prime-discriminant factorization of a quadratic discriminant, where there is only one 2-adic factor.

theorem TauCeti.Multiquadratic.not_isSquare_prod_primeDiscriminantRadicands_of_forall_isEvenPrimeDiscriminant_eq {ι : Type u_1} (D : ι → ℤ) (hD : ∀ (i : ι), IsPrimeDiscriminant (D i)) (hinj : Function.Injective D) (heven_unique : ∀ (i j : ι), IsEvenPrimeDiscriminant (D i) → IsEvenPrimeDiscriminant (D j) → D i = D j) (S : Finset ι) : S.Nonempty → ¬IsSquare (∏ i ∈ S, ↑(primeDiscriminantRadicand (D i)))

Square-class independence for prime-discriminant families with at most one even factor. Let D : ι → ℤ be an injective family of prime discriminants, and assume any two even prime discriminants in the family are equal as integers. Then no nonempty subset product of the associated radicands primeDiscriminantRadicand (D i) is a rational square.

This is the genus-field specialization of not_isSquare_prod_primeDiscriminantRadicands: the prime discriminants dividing a quadratic discriminant have at most one even member, so the exceptional product (-1) * 2 * (-2) = 4 cannot occur.

theorem TauCeti.Multiquadratic.finrank_adjoin_roots_primeDiscriminantRadicands {ι : Type u_1} [Finite ι] {L : Type u_2} [Field L] [Algebra ℚ L] (D : ι → ℤ) (hD : ∀ (i : ι), IsPrimeDiscriminant (D i)) (hinj : Function.Injective D) (heven : ¬((∃ (i : ι), D i = -4) ∧ (∃ (i : ι), D i = 8) ∧ ∃ (i : ι), D i = -8)) (root : ι → L) (hroot : ∀ (i : ι), root i ^ 2 = (algebraMap ℚ L) ↑(primeDiscriminantRadicand (D i))) : Module.finrank ℚ ↥(IntermediateField.adjoin ℚ (Set.range root)) = 2 ^ Nat.card ι

Full degree for adjoining roots of prime-discriminant radicands. Over any field L ⊇ ℚ carrying square roots root i of the radicands of an injective family of prime discriminants not containing all three even prime discriminants, the compositum ℚ(root i : i) has degree 2^|ι|. In a later genus-field specialization, the chosen roots will be identified with the genus-field generators. This is the prime-discriminant instance of finrank_adjoin_range, fed the square-class independence not_isSquare_prod_primeDiscriminantRadicands.

theorem TauCeti.Multiquadratic.finrank_adjoin_roots_primeDiscriminantRadicands_of_forall_isEvenPrimeDiscriminant_eq {ι : Type u_1} [Finite ι] {L : Type u_2} [Field L] [Algebra ℚ L] (D : ι → ℤ) (hD : ∀ (i : ι), IsPrimeDiscriminant (D i)) (hinj : Function.Injective D) (heven_unique : ∀ (i j : ι), IsEvenPrimeDiscriminant (D i) → IsEvenPrimeDiscriminant (D j) → D i = D j) (root : ι → L) (hroot : ∀ (i : ι), root i ^ 2 = (algebraMap ℚ L) ↑(primeDiscriminantRadicand (D i))) : Module.finrank ℚ ↥(IntermediateField.adjoin ℚ (Set.range root)) = 2 ^ Nat.card ι

Full degree for adjoining roots of prime-discriminant radicands with at most one even factor. If D : ι → ℤ is an injective finite family of prime discriminants with at most one even member, then adjoining square roots of the associated radicands gives a multiquadratic field of degree 2 ^ Nat.card ι.

This is the degree theorem in the form needed for genus-field generator lists coming from prime discriminants of a quadratic discriminant.