Complete splitting in number fields #
For a finite Galois number field K / β, a rational prime p splits completely β meaning
there are exactly [K : β] primes of π K above p β if and only if p is unramified with
residue degree one, i.e. both the ramification index e and the inertia degree f (which are
common to all primes above p, the extension being Galois) equal 1.
One direction needs no Galois hypothesis at all: a full complement of primes already forces
e = f = 1 at each of them, directly from the fundamental identity, and hence identifies each
residue field with the prime field.
The relative criteria apply to a finite Galois extension L / K and a base ring over which
Gal(L/K) acts as a Galois group on π L. They include the rings of integers π K and,
when K = β, the rational integers. This is the count form of the fundamental identity
(#primes) Β· e Β· f = [L : K]: the number of primes is maximal exactly when e = f = 1.
Equivalently, the decomposition group of a prime above the base ideal is trivial. These
criteria connect complete splitting with the residue conditions used in prime-splitting laws.
Main results #
NumberField.ncard_primesOver_eq_finrank_iff_of_isGalois: the relative criterion over an arbitrary Dedekind base.NumberField.ncard_primesOver_eq_finrank_iff: the rational-prime specialization.Ideal.isUnramifiedAt_of_ncard_primesOver_eq_finrank: complete splitting implies unramifiedness in any extension of number fields.Ideal.bijective_algebraMap_quotient_of_ncard_primesOver_eq_finrank: complete splitting makes each residue field the prime field.Ideal.absNorm_eq_of_ncard_primesOver_eq_finrank: a prime above a completely split rational prime has that prime as its absolute norm.NumberField.ncard_primesOver_eq_finrank_iff_stabilizer_eq_bot: the relative orbitβstabilizer form of the splitting criterion.
Provenance #
Two of Mathlib's fundamental identities are used, according to whether a Galois hypothesis is
available. The splitting criterion itself rests on the Galois identity
(Ideal.ncard_primesOver_mul_ramificationIdxIn_mul_inertiaDegIn). The consequences drawn without
a Galois hypothesis β that complete splitting forces e = f = 1, and hence that the residue field
at Q is the prime field β rest instead on the general identity for finite flat extensions of
domains (Ideal.sum_ramification_inertia_eq_finrank), applied through
the general theorem in TauCeti.RamificationInertia.Splitting.
The decomposition-group criterion uses the description of the primes above an ideal as one
orbit (Algebra.IsInvariant.orbit_eq_primesOver) and orbitβstabilizer
(MulAction.index_stabilizer), through TauCeti.NumberTheory.RamificationInertia.Galois.
In a Galois extension of number fields, the number of primes over a prime ideal of a
Dedekind base equals the relative degree iff the common ramification index and inertia degree
are both 1.
In a Galois number field, a rational prime p splits completely (there are [K : β] primes
of π K above p) iff its ramification index and inertia degree are both 1.
In a Galois extension of number fields, a base ideal P has [L : K] primes above it
iff the decomposition group of a prime Q above it is trivial. The base ring may be π K
or, when K = β, the rational integers.
A full complement of primes forces unramifiedness. If π L has [L : K] primes above a
prime ideal π of π K, then every prime Q of π L above π is unramified over π K.
No Galois hypothesis is needed.
Complete splitting makes the residue field at Q the prime field. If p splits
completely then algebraMap (β€ β§Έ (p)) (π K β§Έ Q) is bijective. No Galois hypothesis is needed.
The absolute norm of a prime above a completely split rational prime is that prime. If
p splits completely in K then the inertia degree at each prime π above p is 1, so the
residue field at π is β€/p and N(π) = p. No Galois hypothesis is needed.