Multiquadratic fields with pairwise-coprime squarefree integer radicands

The field-generic degree theorem TauCeti.Multiquadratic.finrank_adjoin_range gives a multiquadratic field degree 2ⁿ once its radicands are square-class independent: no nonempty subset product of them is a square. The genus theory the roadmap targets works with the rational field ℚ(√d₁, …, √dₙ) for squarefree integers dᵢ, where the radicands range over composite and negative values (ℚ(√-3, √-7), ℚ(√6, √35)), not just the distinct primes already handled in TauCeti.NumberTheory.Multiquadratic.Prime.Radicands.

This file supplies square-class independence in that setting: a family of pairwise coprime, squarefree, non-unit integers is square-class independent. The argument is the same one that works for distinct primes, run at the level of the integers: a nonempty subset product of pairwise coprime squarefree integers is again squarefree (Mathlib's Finset.squarefree_prod_of_pairwise_isCoprime) and is not a unit (it has a non-unit factor), so it is not a square; and an integer is a square in ℚ iff it is a square in ℤ (Rat.isSquare_intCast_iff). The distinct-primes statement not_isSquare_prod_primes is the special case where each radicand is prime.

Main results

• TauCeti.Multiquadratic.not_isSquare_prod_of_coprime_squarefree: for pairwise coprime squarefree non-unit integers d i, no nonempty subset product ∏_{i ∈ S} d i is a square in ℤ.
• TauCeti.Multiquadratic.not_isSquare_prod_of_coprime_squarefree_rat: the same square-class independence cast to ℚ, in the ∀ S shape the degree theorem consumes.
• TauCeti.Multiquadratic.finrank_adjoin_range_of_coprime_squarefree: [ℚ(√d₁, …, √dₙ) : ℚ] = 2^|ι| for pairwise coprime squarefree non-unit integer radicands, the squarefree-integer corollary of finrank_adjoin_range.
• TauCeti.Multiquadratic.finrank_adjoin_sqrt_six_thirtyfive: [ℚ(√6, √35) : ℚ] = 4, a worked example with composite radicands, beyond the reach of the distinct-primes corollary.

theorem TauCeti.Multiquadratic.not_isSquare_prod_of_coprime_squarefree {ι : Type u_1} (d : ι → ℤ) {S : Finset ι} (hcop : (↑S).Pairwise (Function.onFun IsCoprime d)) (hsf : ∀ i ∈ S, Squarefree (d i)) (hnu : ∀ i ∈ S, ¬IsUnit (d i)) (hS : S.Nonempty) : ¬IsSquare (∏ i ∈ S, d i)

Square-class independence of pairwise coprime squarefree integers. If the radicands d i are pairwise coprime, each squarefree, and each a non-unit, then no nonempty subset product ∏_{i ∈ S} d i is a square in ℤ. This generalises not_isSquare_prod_primes (the distinct-primes case) to the squarefree integers the genus theory uses, and supplies the square-class independence the multiquadratic degree theorem finrank_adjoin_range consumes.

theorem TauCeti.Multiquadratic.not_isSquare_prod_of_coprime_squarefree_rat {ι : Type u_1} (d : ι → ℤ) (hcop : Pairwise (Function.onFun IsCoprime d)) (hsf : ∀ (i : ι), Squarefree (d i)) (hnu : ∀ (i : ι), ¬IsUnit (d i)) (S : Finset ι) : S.Nonempty → ¬IsSquare (∏ i ∈ S, ↑(d i))

Square-class independence cast to ℚ. If d : ι → ℤ is pairwise coprime with each entry squarefree and a non-unit, then no nonempty subset product ∏_{i ∈ S} (d i : ℚ) is a square in ℚ. This is the ∀ S shape of hindep the degree and Galois-group theorems consume directly.

theorem TauCeti.Multiquadratic.finrank_adjoin_range_of_coprime_squarefree {ι : Type u_1} [Finite ι] {L : Type u_2} [Field L] [Algebra ℚ L] (d : ι → ℤ) (root : ι → L) (hroot : ∀ (i : ι), root i ^ 2 = (algebraMap ℚ L) ↑(d i)) (hcop : Pairwise (Function.onFun IsCoprime d)) (hsf : ∀ (i : ι), Squarefree (d i)) (hnu : ∀ (i : ι), ¬IsUnit (d i)) : Module.finrank ℚ ↥(IntermediateField.adjoin ℚ (Set.range root)) = 2 ^ Nat.card ι

Degree of a multiquadratic field with squarefree integer radicands. If d : ι → ℤ is pairwise coprime with each entry squarefree and a non-unit, and root i is a square root of d i in a field L over ℚ (so ℚ(√d₁, …, √dₙ) makes sense even for the negative radicands the genus theory needs), then [ℚ(rootᵢ : i) : ℚ] = 2^|ι|. This is the squarefree-integer corollary of the field-generic degree theorem finrank_adjoin_range.

theorem TauCeti.Multiquadratic.finrank_adjoin_sqrt_six_thirtyfive : Module.finrank ℚ ↥ℚ⟮√6, √35⟯ = 4

Worked example: [ℚ(√6, √35) : ℚ] = 4. The radicands 6 = 2·3 and 35 = 5·7 are composite, so this lies beyond the distinct-primes corollary finrank_adjoin_sqrt_primes; it is covered by finrank_adjoin_range_of_coprime_squarefree because 6 and 35 are coprime, squarefree, and not units.