The prime-splitting law for a multiquadratic field

For a multiquadratic number field K = ℚ(√d₁, …, √dₙ) and an odd prime p dividing none of the radicands, p splits completely in K if and only if every dᵢ is a quadratic residue mod p.

This is the general (compositum) case; the base case n = 1 is ncard_primesOver_quadratic_iff.

Main results

• NumberField.map_eq_self_of_legendreSym_eq_one: the decomposition group of a prime above p fixes the square root of every quadratic residue mod p.
• NumberField.ncard_primesOver_multiquadratic_iff: the multiquadratic prime-splitting law — p splits completely in K = ℚ(√d₁, …, √dₙ) iff every dᵢ is a quadratic residue mod p.

theorem NumberField.map_eq_self_of_legendreSym_eq_one {K : Type u_1} [Field K] [NumberField K] (d : ℤ) (r : K) (hr : r ^ 2 = (algebraMap ℤ K) d) {p : ℕ} [Fact (Nat.Prime p)] (hodd : p ≠ 2) (hqr : legendreSym p d = 1) (Q : Ideal (RingOfIntegers K)) [Q.IsPrime] [Q.LiesOver (Ideal.span {↑p})] {σ : Gal(K/ℚ)} (hσ : σ ∈ MulAction.stabilizer Gal(K/ℚ) Q) : σ r = r

The decomposition group fixes the square root of a residue. If d is a quadratic residue mod the odd prime p (with p ∤ d), then every σ in the decomposition group of a prime Q above p fixes the square root r of d. Equivalently, an automorphism moving r moves every prime above p.

theorem NumberField.ncard_primesOver_multiquadratic_iff {K : Type u_1} [Field K] [NumberField K] {ι : Type u_2} [Finite ι] (d : ι → ℤ) (r : ι → K) (hr : ∀ (i : ι), r i ^ 2 = (algebraMap ℤ K) (d i)) (htop : IntermediateField.adjoin ℚ (Set.range r) = ⊤) {p : ℕ} [Fact (Nat.Prime p)] (hodd : p ≠ 2) (hcop : ∀ (i : ι), ¬↑p ∣ d i) : ((Ideal.span {↑p}).primesOver (RingOfIntegers K)).ncard = Module.finrank ℚ K ↔ ∀ (i : ι), legendreSym p (d i) = 1

The multiquadratic splitting law. For K = ℚ(√d₁, …, √dₙ) generated over ℚ by square roots r i of integers d i, and an odd prime p dividing none of the d i, p splits completely in K iff every d i is a quadratic residue mod p.