Ramified primes in a Galois extension unramified over a quadratic subfield #
Let M / ℚ be a Galois number-field extension and let F ⊆ M be a quadratic intermediate field
such that M / F is unramified at every finite prime. This file computes which rational primes
ramify in the intermediate fields of M. Two statements come out, and together they say that the
quadratic subfields of M ramified at a fixed prime p form a coset of those unramified at p.
- Ramification descends to
F. Every rational prime ramifying in an intermediate field ofMalready ramifies inF. - Two ramified square roots multiply to an unramified one. If
√a ∈ Mandpramifies inℚ(√a), thenpis unramified inℚ(√(ab)), whereℚ(√b) = F.
Both are read off the inertia subgroups of the primes P of 𝓞 M above p: an intermediate
field is unramified at p exactly when every one of them fixes it pointwise
(NumberField.notMem_ramifiedPrimes_iff_forall_inertia_le). Unramifiedness of M / F makes such
an inertia subgroup I meet Gal(M / F) trivially
(NumberField.disjoint_inertia_of_ramificationIdx_eq_one), and Gal(M / F) has index two, so any
two nonidentity elements of I coincide: I is {1} at an unramified prime and {1, σ} at a
ramified one. Since σ sends a square root of a rational number to plus or minus itself,
σ √a = -√a and σ √b = -√b give σ (√a √b) = √a √b, which is the second statement; and
σ ≠ 1 does not lie in Gal(M / F), which is the first.
For the second statement one prime above p still settles the others: the Galois group permutes
them transitively and conjugates their inertia subgroups (Ideal.mem_inertia_pointwise_smul_iff),
while g √c = ±√c for rational c makes fixing a quadratic subfield generated by a square root a
conjugation-invariant condition.
The arithmetic form of both statements is stated with fundamentalDiscriminant, using that the
discriminant of ℚ(√a) for squarefree a is fundamentalDiscriminant a
(TauCeti.Multiquadratic.discr_adjoin_singleton_eq_fundamentalDiscriminant). It constrains the
prime discriminants of a quadratic subfield of M by those of F, which is the arithmetic half of
the maximality proof for the candidate genus field. The field-theoretic half is
TauCeti.Multiquadratic.exists_squarefree_root_adjoin_range_eq_top_of_isUnramifiedIn_over_quadratic
in TauCeti/NumberTheory/Multiquadratic/Unramified/Basic.lean, which presents such an M as a
multiquadratic field.
This is the classical argument in the genus-field construction; see D. A. Cox, Primes of the Form x² + ny², §6.A, and F. Lemmermeyer, Reciprocity Laws: From Euler to Eisenstein, §2.2.
Main results #
In the namespace TauCeti.Multiquadratic:
ramifiedPrimes_subset_of_isUnramifiedIn: a prime ramifying in an intermediate field ramifies in the quadratic subfield.notMem_ramifiedPrimes_adjoin_mul: a prime ramifying inℚ(√a)is unramified inℚ(√(ab)).mem_ramifiedPrimes_adjoin_iff_dvd_fundamentalDiscriminant: the ramified primes of the quadratic subfield generated by a square root of a squarefree integer.dvd_fundamentalDiscriminant_base_of_dvd_subfieldandnot_dvd_fundamentalDiscriminant_mul_of_dvd_subfield: the arithmetic forms.
Provenance #
Independently reconstructed. The multiquadratic roadmap designates
kim-em/erdos-unit-distance (the formalization of
L. Alpöge's disproof of the uniform-constant Erdős unit-distance conjecture) as the migration
source for its Layer-0 square-class machinery — sqrtTower, mem_sup_adjoin_sq,
squareClass_of_sqrt_mem, sqrtTower_finrank, exists_transversal_family and
units_sq_index_le — and none of that is used here: this file is inertia theory over the Galois
group of M / ℚ, resting on Mathlib's Ideal.inertia and on
TauCeti/NumberTheory/NumberField/Inertia.lean.
Ramification descends to the quadratic subfield. Let M / ℚ be Galois, let F ⊆ M be an
intermediate field such that M / F is unramified at every finite prime, and let E ⊆ M be any
intermediate field. Then every rational prime ramifying in E ramifies in F.
Were such a prime unramified in F, the inertia subgroup of every prime P of 𝓞 M above it
would be contained in Gal(M / F); being also disjoint from Gal(M / F) it would be trivial,
hence contained in Gal(M / E), and the prime would be unramified in E.
Two ramified square roots multiply to an unramified one. Let M / ℚ be Galois, let
y ∈ M be a square root of a rational number generating a quadratic subfield ℚ(y), and suppose
M / ℚ(y) is unramified at every finite prime. Let x ∈ M be a square root of a rational number.
If a rational prime p ramifies in ℚ(x), then it is unramified in ℚ(r x y) for every
rational r.
Ramification in ℚ(x) produces a prime P₀ above p whose inertia subgroup I does not fix
ℚ(x) pointwise, say τ ∈ I with τ x ≠ x, hence τ x = -x. As I is disjoint from
Gal(M / ℚ(y)), which has index two, any two nonidentity elements of I coincide: a nonidentity
σ ∈ I satisfies σ τ = 1, so σ x = -x, while σ ∉ Gal(M / ℚ(y)) forces σ y = -y. Thus σ
fixes x y, and I fixes ℚ(r x y) pointwise. Any other prime above p is a translate
g • P₀, whose inertia subgroup is the conjugate g I g⁻¹, and fixing ℚ(r x y) is invariant
under conjugation.
The ramified primes of a quadratic subfield generated by a square root. For squarefree a
that is not a rational square and x ∈ M with x ^ 2 = a, a rational prime ramifies in ℚ(x)
exactly when it divides fundamentalDiscriminant a.
A ramified prime of a quadratic subfield ramifies in the quadratic base. In a Galois
M / ℚ unramified over ℚ(√d) at every finite prime, every prime dividing the discriminant of a
quadratic subfield ℚ(√a) divides the discriminant of ℚ(√d).
The product of two square roots is unramified where the first one ramifies. In a Galois
M / ℚ unramified over the quadratic field ℚ(√d) at every finite prime, if c is a squarefree
integer in the square class of a * d then no prime dividing the discriminant of ℚ(√a) divides
the discriminant of ℚ(√c).