The number of primes above two in a multiquadratic field

For K = ℚ(√d₁, …, √dₙ) with integer radicands not divisible by four, this file gives the prime count at two directly in terms of the radicands, including when two ramifies. The ramification index is 2 ^ a, where a = 2 when the radicands generate two ramified dyadic square classes, a = 0 when all radicands are one modulo four, and a = 1 otherwise. The residue degree is 2 ^ b, where b = 1 precisely when the squarefree part of a subset product is five modulo eight, and b = 0 otherwise.

Thus the number of primes above two is [K : ℚ] / 2 ^ (a + b). Under square-class independence, ncard_primesOver_two_eq_two_pow_sub gives 2 ^ (n - (a + b)), using the equivalent rational square-class test for b. The companion dyadic_exponents_add_le_card exposes the bound a + b ≤ n, so subtraction cannot conceal an impossible decomposition type. Independence is unnecessary for the formula in terms of the field degree.

References

• D. A. Cox, Primes of the Form x² + ny², §5.B.
• J. Neukirch, Algebraic Number Theory, Chapter I, §9 and Chapter II, §5.
• Mathlib, Ideal.ncard_primesOver_mul_ramificationIdxIn_mul_inertiaDegIn (the Galois fundamental identity).

theorem TauCeti.Multiquadratic.ncard_primesOver_two_mul_two_pow_eq_finrank {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) = ⊤) (hd : ∀ (i : ι), ¬4 ∣ d i) : have a := if (∃ (i : ι) (j : ι), d i % 4 = 3 ∧ 2 ∣ d j) ∨ ∃ (i : ι) (j : ι), d i % 8 = 2 ∧ d j % 8 = 6 then 2 else if ∀ (i : ι), d i % 4 = 1 then 0 else 1; have b := if ∃ (T : Finset ι) (s : ℤ) (t : ℤ), Squarefree s ∧ t ≠ 0 ∧ ∏ i ∈ T, d i = s * t ^ 2 ∧ s % 8 = 5 then 1 else 0; ((Ideal.span {2}).primesOver (NumberField.RingOfIntegers K)).ncard * 2 ^ (a + b) = Module.finrank ℚ K

The dyadic decomposition identity, without square-class independence. The number of primes above two multiplied by 2 ^ (a + b) equals [K : ℚ], where the displayed arithmetic tests determine the ramification index e = 2 ^ a and residue degree f = 2 ^ b. In particular, 2 ^ (a + b) divides the field degree, including when two ramifies.

theorem TauCeti.Multiquadratic.ncard_primesOver_two_eq_finrank_div {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) = ⊤) (hd : ∀ (i : ι), ¬4 ∣ d i) : have a := if (∃ (i : ι) (j : ι), d i % 4 = 3 ∧ 2 ∣ d j) ∨ ∃ (i : ι) (j : ι), d i % 8 = 2 ∧ d j % 8 = 6 then 2 else if ∀ (i : ι), d i % 4 = 1 then 0 else 1; have b := if ∃ (T : Finset ι) (s : ℤ) (t : ℤ), Squarefree s ∧ t ≠ 0 ∧ ∏ i ∈ T, d i = s * t ^ 2 ∧ s % 8 = 5 then 1 else 0; ((Ideal.span {2}).primesOver (NumberField.RingOfIntegers K)).ncard = Module.finrank ℚ K / 2 ^ (a + b)

The number of primes above two, without square-class independence. The exponents a and b read the ramification index and residue degree from the radicands: e = 2 ^ a and f = 2 ^ b. The number of primes is therefore [K : ℚ] / 2 ^ (a + b), whether or not two ramifies. Radicands need only be indivisible by four, rather than squarefree.

theorem TauCeti.Multiquadratic.dyadic_exponents_add_le_card {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) = ⊤) (hd : ∀ (i : ι), ¬4 ∣ d i) (hindep : ∀ (S : Finset ι), S.Nonempty → ¬IsSquare (∏ i ∈ S, ↑(d i))) : have a := if (∃ (i : ι) (j : ι), d i % 4 = 3 ∧ 2 ∣ d j) ∨ ∃ (i : ι) (j : ι), d i % 8 = 2 ∧ d j % 8 = 6 then 2 else if ∀ (i : ι), d i % 4 = 1 then 0 else 1; have b := if ∃ (T : Finset ι) (s : ℤ) (t : ℤ), Squarefree s ∧ t ≠ 0 ∧ ∏ i ∈ T, d i = s * t ^ 2 ∧ s % 8 = 5 then 1 else 0; a + b ≤ Nat.card ι

The dyadic exponents fit within the number of independent radicands. The displayed ramification and residue-degree exponents satisfy a + b ≤ Nat.card ι, ensuring that natural subtraction of their sum from the number of radicands does not truncate.

theorem TauCeti.Multiquadratic.ncard_primesOver_two_eq_two_pow_sub {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) = ⊤) (hd : ∀ (i : ι), ¬4 ∣ d i) (hindep : ∀ (S : Finset ι), S.Nonempty → ¬IsSquare (∏ i ∈ S, ↑(d i))) : ((Ideal.span {2}).primesOver (NumberField.RingOfIntegers K)).ncard = 2 ^ (Nat.card ι - ((if (∃ (i : ι) (j : ι), d i % 4 = 3 ∧ 2 ∣ d j) ∨ ∃ (i : ι) (j : ι), d i % 8 = 2 ∧ d j % 8 = 6 then 2 else if ∀ (i : ι), d i % 4 = 1 then 0 else 1) + if ∃ (T : Finset ι) (c : ℤ) (q : ℚ), c % 8 = 5 ∧ q ≠ 0 ∧ ∏ i ∈ T, ↑(d i) = ↑c * q ^ 2 then 1 else 0))

The number of primes above 2. Let K be generated over ℚ by square roots of n square-class independent integers d i (no nonempty subset product is a square) not divisible by 4. Then there are exactly 2 ^ (n - a - b) primes of 𝓞 K above 2, where the ramification index is e = 2 ^ a and the residue degree is f = 2 ^ b:

• a = 2 when some d i is 3 modulo 4 and some d j is even, or some d i is 2 and some d j is 6 modulo 8; otherwise a = 0 when every d i is 1 modulo 4, and a = 1 when not;
• b = 1 when some subset product ∏_{i ∈ T} dᵢ lies in the rational square class of an integer that is 5 modulo 8, and b = 0 otherwise.