Prime-discriminant splitting in multiquadratic fields

The genus-field layer indexes the quadratic factors by prime discriminants D, while the multiquadratic splitting theorem is stated for the corresponding squarefree radicands primeDiscriminantRadicand D. This file records the small bridge between those conventions.

The prime-discriminant convention follows the standard genus-theory convention in Cox's Primes of the Form x² + ny² and Lemmermeyer's Reciprocity Laws.

Main results

• NumberField.ncard_primesOver_primeDiscriminantRadicands_iff: the multiquadratic splitting law for a field generated by roots of prime-discriminant radicands, stated in terms of Legendre symbols of the prime discriminants themselves.
• NumberField.ncard_primesOver_primeDiscriminantRadicands_iff_congruences: the same splitting law with the prime-discriminant Legendre-symbol condition expanded into the corresponding congruence conditions.

theorem NumberField.ncard_primesOver_primeDiscriminantRadicands_iff {K : Type u_1} [Field K] [NumberField K] {ι : Type u_2} (D : ι → ℤ) (r : ι → K) (hr : ∀ (i : ι), r i ^ 2 = (algebraMap ℤ K) (TauCeti.Multiquadratic.primeDiscriminantRadicand (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

Prime-discriminant-radicand multiquadratic splitting law. Let K be generated over ℚ by square roots of the radicands attached to a family of integers D. For an odd prime p dividing none of the D i, p splits completely in K exactly when every D i is a quadratic residue modulo p.

theorem NumberField.ncard_primesOver_primeDiscriminantRadicands_iff_congruences {K : Type u_1} [Field K] [NumberField K] {ι : Type u_2} (D : ι → ℤ) (hD : ∀ (i : ι), TauCeti.Multiquadratic.IsPrimeDiscriminant (D i)) (r : ι → K) (hr : ∀ (i : ι), r i ^ 2 = (algebraMap ℤ K) (TauCeti.Multiquadratic.primeDiscriminantRadicand (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 : ι), (TauCeti.Multiquadratic.IsEvenPrimeDiscriminant (D i) ∧ if D i = -4 then p % 4 = 1 else if D i = 8 then p % 8 = 1 ∨ p % 8 = 7 else p % 8 = 1 ∨ p % 8 = 3) ∨ ∃ (q : ℕ) (hq : Nat.Prime q), Odd q ∧ D i = TauCeti.Multiquadratic.oddPrimeDiscriminant q ∧ legendreSym q ↑p = 1

Prime-discriminant-radicand multiquadratic splitting law, congruence form. Let K be generated over ℚ by square roots of the radicands attached to a family of prime discriminants D. For an odd prime p dividing none of the D i, p splits completely in K exactly when each even prime discriminant satisfies the corresponding supplementary congruence condition, and each odd prime discriminant satisfies the reciprocal Legendre-symbol condition.