Multiquadratic fields with prime radicands

The field-generic degree theorem TauCeti.Multiquadratic.finrank_adjoin_range says that a multiquadratic field has degree 2ⁿ once the radicands are square-class independent: no nonempty subset product of them is a square. This file supplies that hypothesis for the most common concrete source of square-class independent radicands — a family of distinct primes — and so derives the prime-indexed degree corollary [ℚ(√p₁, …, √pₙ) : ℚ] = 2ⁿ (a genus-theory input) and the smallest non-vacuity example [ℚ(√2, √3) : ℚ] = 4.

The square-class independence of distinct primes is elementary: a nonempty subset product of distinct primes is squarefree (the primes are pairwise coprime) and is not a unit (it has a prime factor), so it is not a square.

Main results

• TauCeti.Multiquadratic.not_isSquare_prod_primes: for distinct primes p i, no nonempty subset product ∏_{i ∈ S} (p i : ℚ) is a square — square-class independence in the form the degree theorem consumes.
• TauCeti.Multiquadratic.not_isSquare_prod_primes_of_injective: the same square-class independence, packaged from an injective family of primes — the shape the multiquadratic degree and Galois-group theorems consume directly.
• TauCeti.Multiquadratic.irreducible_X_sq_sub_C_natCast_of_prime: X² - p is irreducible over ℚ for a prime p, the minimal polynomial of each single prime radicand.
• TauCeti.Multiquadratic.finrank_adjoin_sqrt_primes: [ℚ(√p₁, …, √pₙ) : ℚ] = 2^|ι| for a finite family of distinct primes.
• TauCeti.Multiquadratic.finrank_adjoin_sqrt_two_three: [ℚ(√2, √3) : ℚ] = 4.

theorem TauCeti.Multiquadratic.not_isSquare_prod_primes {ι : Type u_1} (p : ι → ℕ) {S : Finset ι} (hp : ∀ i ∈ S, Nat.Prime (p i)) (hdist : (↑S).Pairwise fun (i j : ι) => p i ≠ p j) (hS : S.Nonempty) : ¬IsSquare (∏ i ∈ S, ↑(p i))

Square-class independence of distinct primes. If the selected p i are prime and pairwise distinct, then no nonempty subset product ∏_{i ∈ S} (p i : ℚ) is a square in ℚ. This is the hypothesis the multiquadratic degree theorem finrank_adjoin_range consumes.

theorem TauCeti.Multiquadratic.irreducible_X_sq_sub_C_natCast_of_prime {p : ℕ} (hp : Nat.Prime p) : Irreducible (Polynomial.X ^ 2 - Polynomial.C ↑p)

X² - p is irreducible over ℚ for a prime p: a rational root would make p a square in ℕ (Rat.isSquare_natCast_iff), which a prime is not. This is Kummer irreducibility (X_pow_sub_C_irreducible_of_prime) for a single prime radicand.

theorem TauCeti.Multiquadratic.sq_sqrt_natCast (n : ℕ) : √↑n ^ 2 = (algebraMap ℚ ℝ) ↑n

The real square root of a natural number squares back to its rational value, in the form (√n)² = algebraMap ℚ ℝ n. This supplies the hroot hypothesis that the multiquadratic degree and Galois-group theorems consume for the family of square roots of a prime family. It is the 0 ≤ n special case of sq_sqrt_intCast.

theorem TauCeti.Multiquadratic.not_isSquare_prod_primes_of_injective {ι : Type u_1} (p : ι → ℕ) (hp : ∀ (i : ι), Nat.Prime (p i)) (hinj : Function.Injective p) (S : Finset ι) : S.Nonempty → ¬IsSquare (∏ i ∈ S, ↑(p i))

Square-class independence of an injective family of primes. If p : ι → ℕ is injective and each p i is prime, then no nonempty subset product ∏_{i ∈ S} (p i : ℚ) is a square. This is the hindep hypothesis the multiquadratic degree and Galois-group theorems consume directly.

theorem TauCeti.Multiquadratic.finrank_adjoin_sqrt_primes {ι : Type u_1} [Finite ι] (p : ι → ℕ) (hp : ∀ (i : ι), Nat.Prime (p i)) (hinj : Function.Injective p) : Module.finrank ℚ ↥(IntermediateField.adjoin ℚ (Set.range fun (i : ι) => √↑(p i))) = 2 ^ Nat.card ι

Degree of a prime-radicand multiquadratic field. For a finite family of distinct primes p : ι → ℕ, the field generated over ℚ by their real square roots has degree 2^|ι|. This is the prime-indexed corollary of the field-generic degree theorem finrank_adjoin_range.

theorem TauCeti.Multiquadratic.finrank_adjoin_sqrt_two_three : Module.finrank ℚ ↥ℚ⟮√2, √3⟯ = 4

Worked example: [ℚ(√2, √3) : ℚ] = 4. The smallest nontrivial multiquadratic degree, obtained from finrank_adjoin_sqrt_primes with the primes 2 and 3.