Comparing two prime-discriminant factorizations

Let a and d be integers and write A = fundamentalDiscriminant a, D = fundamentalDiscriminant d. Suppose A = ∏ P ∈ u, P and D = ∏ P ∈ s, P are factorizations into prime discriminants, at most one member of each being even (Int.IsFundamentalDiscr.exists_finset_primeDiscriminant produces such factorizations). This file gives a criterion for u ⊆ s, that is, for the quadratic field ℚ(√a) to sit inside the compositum of the prime-discriminant quadratic fields attached to s:

• every rational prime dividing A divides D, and
• if 2 ∣ A then 2 ∤ fundamentalDiscriminant c, where c is any integer with a * d = c * e ^ 2 — that is, ℚ(√(ad)) is unramified at 2.

These are exactly the two constraints that the maximality argument for the genus field extracts from ramification theory (TauCeti.Multiquadratic.dvd_fundamentalDiscriminant_base_of_dvd_subfield and TauCeti.Multiquadratic.not_dvd_fundamentalDiscriminant_mul_of_dvd_subfield), so the theorem below is the arithmetic half of that argument, isolated from the field theory.

The odd part of the criterion is immediate: an odd prime lies under exactly one prime discriminant, namely p* = (-1)^((p-1)/2) p, so a shared prime forces a shared factor. The even part is the announced trap: -4, 8 and -8 all lie over 2, and mere divisibility cannot tell them apart. What separates them is the second hypothesis. Writing A = E * m and D = F * n with E, F ∈ {-4, 8, -8} and m, n ≡ 1 (mod 4) (a product of odd prime discriminants is 1 mod 4), one has 4a = E * m and 4d = F * n; a mismatch E ≠ F then makes a * d either twice an odd number or -4 times a number that is 1 mod 4, and neither is c * e ^ 2 with c ≡ 1 (mod 4).

The classical statement is that the discriminant of a quadratic subfield of the genus field divides the discriminant of the base; see D. A. Cox, Primes of the Form x² + ny², §6.A, and F. Lemmermeyer, Reciprocity Laws: From Euler to Eisenstein, §2.2. Divisibility of fundamental discriminants is genuinely weaker than the subset relation proved here (-4 ∣ 8, yet the quadratic field of discriminant -4 is not the one of discriminant 8), which is why the conclusion is stated as u ⊆ s.

Main results

• TauCeti.Multiquadratic.IsPrimeDiscriminant.mod_four_eq_one: an odd prime discriminant is 1 modulo 4.
• TauCeti.Multiquadratic.exists_mod_four_eq_one_four_mul_eq: splitting the even factor off a prime-discriminant factorization of fundamentalDiscriminant a writes 4 * a = E * m with m ≡ 1 (mod 4).
• TauCeti.Multiquadratic.isEvenPrimeDiscriminant_eq_of_four_mul_eq: the even factors of two such factorizations agree as soon as the square class of the product is unramified at 2.
• TauCeti.Multiquadratic.subset_of_forall_prime_dvd_fundamentalDiscriminant: the criterion for one factorization to be a subset of the other.

theorem TauCeti.Multiquadratic.IsPrimeDiscriminant.mod_four_eq_one {P : ℤ} (hP : IsPrimeDiscriminant P) (hne : ¬IsEvenPrimeDiscriminant P) : P % 4 = 1

A prime discriminant other than -4, 8, -8 is congruent to 1 modulo 4: it is the odd prime discriminant p*.

theorem TauCeti.Multiquadratic.prod_primeDiscriminant_mod_four_eq_one {s : Finset ℤ} (hs : ∀ P ∈ s, IsPrimeDiscriminant P) (hne : ∀ P ∈ s, ¬IsEvenPrimeDiscriminant P) : (∏ P ∈ s, P) % 4 = 1

A product of odd prime discriminants is congruent to 1 modulo 4.

theorem TauCeti.Multiquadratic.exists_mod_four_eq_one_four_mul_eq {a E : ℤ} {u : Finset ℤ} (hu : ∀ P ∈ u, IsPrimeDiscriminant P) (hue : ∀ P ∈ u, ∀ Q ∈ u, IsEvenPrimeDiscriminant P → IsEvenPrimeDiscriminant Q → P = Q) (huprod : ∏ P ∈ u, P = fundamentalDiscriminant a) (hE : E ∈ u) (hEeven : IsEvenPrimeDiscriminant E) : ∃ (m : ℤ), m % 4 = 1 ∧ 4 * a = E * m

Splitting off the even prime discriminant. If the prime discriminants in u have product fundamentalDiscriminant a and at most one of them is even, then an even member E of u satisfies 4 * a = E * m for a complementary factor m ≡ 1 (mod 4), namely the product of the remaining (odd) prime discriminants.

theorem TauCeti.Multiquadratic.isEvenPrimeDiscriminant_eq_of_four_mul_eq {a d c e E F m n : ℤ} (hE : IsEvenPrimeDiscriminant E) (hF : IsEvenPrimeDiscriminant F) (hm : m % 4 = 1) (hn : n % 4 = 1) (ha : 4 * a = E * m) (hd : 4 * d = F * n) (hade : a * d = c * e ^ 2) (hc : c % 4 = 1) : E = F

The even prime discriminants of two fundamental discriminants agree when the square class of the product is unramified at 2. Concretely: if 4 * a = E * m and 4 * d = F * n with E, F even prime discriminants and m ≡ n ≡ 1 (mod 4), and if a * d = c * e ^ 2 with c ≡ 1 (mod 4), then E = F.

This is what distinguishes -4, 8 and -8, which no divisibility statement can: for instance 4 * 3 = (-4) * (-3) and 4 * 2 = 8 * 1, and the product 3 * 2 = 6 has squarefree part 6, which is 2 modulo 4, not 1.

theorem TauCeti.Multiquadratic.subset_of_forall_prime_dvd_fundamentalDiscriminant {a d c e : ℤ} {s u : Finset ℤ} (hs : ∀ P ∈ s, IsPrimeDiscriminant P) (hse : ∀ P ∈ s, ∀ Q ∈ s, IsEvenPrimeDiscriminant P → IsEvenPrimeDiscriminant Q → P = Q) (hsprod : ∏ P ∈ s, P = fundamentalDiscriminant d) (hu : ∀ P ∈ u, IsPrimeDiscriminant P) (hue : ∀ P ∈ u, ∀ Q ∈ u, IsEvenPrimeDiscriminant P → IsEvenPrimeDiscriminant Q → P = Q) (huprod : ∏ P ∈ u, P = fundamentalDiscriminant a) (hade : a * d = c * e ^ 2) (hdvd : ∀ (p : ℕ), Nat.Prime p → ↑p ∣ fundamentalDiscriminant a → ↑p ∣ fundamentalDiscriminant d) (hodd : 2 ∣ fundamentalDiscriminant a → ¬2 ∣ fundamentalDiscriminant c) : u ⊆ s

A prime-discriminant factorization sits inside another. Let u and s be finite sets of prime discriminants, at most one member of each being even, with products fundamentalDiscriminant a and fundamentalDiscriminant d. If every rational prime dividing fundamentalDiscriminant a divides fundamentalDiscriminant d, and if 2 ∣ fundamentalDiscriminant a forces fundamentalDiscriminant c to be odd for some c with a * d = c * e ^ 2, then u ⊆ s.

Both hypotheses are needed, and both are supplied by the ramification theory of a Galois extension unramified over ℚ(√d): the first says a prime ramifying in ℚ(√a) ramifies in ℚ(√d), the second that 2 does not ramify in ℚ(√(ad)).