The ramified primes of a multiquadratic field

Let d₁, …, dₙ be squarefree integers and let M = ℚ(√d₁, …, √dₙ). A rational prime p ramifies in M exactly when it ramifies in one of the possibly trivial square-root-generated factors ℚ(√dᵢ), that is, when it divides one of the fundamental discriminants fundamentalDiscriminant dᵢ. Concretely:

• an odd prime ramifies in M exactly when it divides some dᵢ;
• the prime 2 ramifies in M exactly when some dᵢ is not 1 modulo 4.

Thus the odd primes excluded by the multiquadratic splitting law (NumberField.ncard_primesOver_multiquadratic_iff, which assumes p ∤ dᵢ for every i) are exactly the odd ramified primes, and at 2 the ramification is governed by the discriminants dᵢ or 4dᵢ of the fields generated by the individual square roots rather than by the radicands themselves.

The reduction to the individual square-root factors is NumberField.ramifiedPrimes_iSup: in a Galois number field, a compositum ramifies exactly where one of its factors does. The quadratic case, including the trivial factor contributed by the radicand 1, is TauCeti.Multiquadratic.mem_ramifiedPrimes_adjoin_iff_dvd_fundamentalDiscriminant, so the radicands need not be nonsquares.

Main results

• TauCeti.Multiquadratic.mem_ramifiedPrimes_adjoin_range_iff: the ramified primes of the subfield ℚ(√d₁, …, √dₙ) of a number field.
• TauCeti.Multiquadratic.mem_ramifiedPrimes_iff_exists_dvd_fundamentalDiscriminant: the same for a number field generated by the square roots.
• TauCeti.Multiquadratic.isUnramifiedIn_iff_forall_not_dvd_of_ne_two: an odd prime is unramified exactly when it divides none of the radicands.
• TauCeti.Multiquadratic.isUnramifiedIn_two_iff_forall_mod_four_eq_one: the prime 2 is unramified exactly when every radicand is 1 modulo 4.

References

• D. A. Cox, Primes of the Form x² + ny², §5.B and §6.A.
• F. Lemmermeyer, Reciprocity Laws: From Euler to Eisenstein, §2.2.

theorem TauCeti.Multiquadratic.mem_ramifiedPrimes_adjoin_range_iff {ι : Type u_1} {L : Type u_2} [Field L] [NumberField L] {d : ι → ℤ} {r : ι → L} (hd : ∀ (i : ι), Squarefree (d i)) (hr : ∀ (i : ι), r i ^ 2 = (algebraMap ℤ L) (d i)) {p : ℕ} (hp : Nat.Prime p) : p ∈ NumberField.ramifiedPrimes ↥(IntermediateField.adjoin ℚ (Set.range r)) ↔ ∃ (i : ι), ↑p ∣ fundamentalDiscriminant (d i)

The ramified primes of a multiquadratic field. Let r i be square roots of squarefree integers d i in a number field. A rational prime ramifies in ℚ(r i : i) exactly when it divides the fundamental discriminant of one of the d i, that is, exactly when it ramifies in one of the possibly trivial square-root-generated factors ℚ(r i).

theorem TauCeti.Multiquadratic.mem_ramifiedPrimes_iff_exists_dvd_fundamentalDiscriminant {ι : Type u_1} {L : Type u_2} [Field L] [NumberField L] {d : ι → ℤ} {r : ι → L} (hd : ∀ (i : ι), Squarefree (d i)) (hr : ∀ (i : ι), r i ^ 2 = (algebraMap ℤ L) (d i)) (htop : IntermediateField.adjoin ℚ (Set.range r) = ⊤) {p : ℕ} (hp : Nat.Prime p) : p ∈ NumberField.ramifiedPrimes L ↔ ∃ (i : ι), ↑p ∣ fundamentalDiscriminant (d i)

The ramified primes of a field generated by square roots. The form of mem_ramifiedPrimes_adjoin_range_iff for a number field L generated by square roots of squarefree integers.

theorem TauCeti.Multiquadratic.isUnramifiedIn_iff_forall_not_dvd_of_ne_two {ι : Type u_1} {L : Type u_2} [Field L] [NumberField L] {d : ι → ℤ} {r : ι → L} (hd : ∀ (i : ι), Squarefree (d i)) (hr : ∀ (i : ι), r i ^ 2 = (algebraMap ℤ L) (d i)) (htop : IntermediateField.adjoin ℚ (Set.range r) = ⊤) {p : ℕ} (hp : Nat.Prime p) (hp2 : p ≠ 2) : Algebra.IsUnramifiedIn (NumberField.RingOfIntegers L) (Ideal.span {↑p}) ↔ ∀ (i : ι), ¬↑p ∣ d i

The odd ramified primes are the divisors of the radicands. In a number field L generated by square roots of squarefree integers d i, an odd prime p is unramified exactly when it divides none of the d i.

theorem TauCeti.Multiquadratic.isUnramifiedIn_two_iff_forall_mod_four_eq_one {ι : Type u_1} {L : Type u_2} [Field L] [NumberField L] {d : ι → ℤ} {r : ι → L} (hd : ∀ (i : ι), Squarefree (d i)) (hr : ∀ (i : ι), r i ^ 2 = (algebraMap ℤ L) (d i)) (htop : IntermediateField.adjoin ℚ (Set.range r) = ⊤) : Algebra.IsUnramifiedIn (NumberField.RingOfIntegers L) (Ideal.span {2}) ↔ ∀ (i : ι), d i % 4 = 1

The prime 2 is unramified exactly when every radicand is 1 modulo 4. In a number field generated by square roots of squarefree integers d i, the prime 2 is unramified exactly when d i ≡ 1 (mod 4) for every i.