The Artin symbol of an unramified prime #
For a finite Galois extension of number fields, this file attaches to an unramified
prime ideal of the base the conjugacy class of its arithmetic Frobenius elements.
The definition uses Mathlib's IsArithFrobAt and arithFrobAt; no Frobenius
predicate or representative is introduced here.
The construction follows JΓΌrgen Neukirch, Algebraic Number Theory, Chapter I, Β§9, Exercise 2.
The same reference gives functoriality in a normal tower: restriction maps the Artin symbol of
L/K to the Artin symbol of M/K. Unramifiedness in the intermediate extension is derived from
unramifiedness in the top extension, rather than assumed separately.
Raising the base field is the companion law, and it takes a power: for K β M β L, the symbol
of a prime of π M above π, read inside Gal(L/K), is the f(π/π)-th power of the symbol of
π. Stated on conjugacy classes it names no prime of π L and no Frobenius representative, both
of which the element-level form in TauCeti.NumberTheory.NumberField.Frobenius.Tower fixes.
Finally, the symbol detects complete splitting: it is the identity class exactly when the
residue degree is one, equivalently when π L has [L : K] primes above π.
The arithmetic Artin symbol at a prime ideal unramified in L.
The value is the conjugacy class of Mathlib's coherently chosen arithmetic Frobenius at
one prime above π; the unramifiedness proof is an argument, so the symbol is only
defined at unramified primes.
Instances For
Every arithmetic Frobenius at a prime over π represents artinSymbol π hur.
Thus the definition is independent of the prime chosen above π and of the chosen
Frobenius at that prime, as required for a conjugacy-class-valued symbol.
The Artin symbol is functorial under restriction to a normal subextension. For a normal
tower L/M/K, applying restriction to the conjugacy class artinSymbol π for L/K gives the
Artin symbol for M/K. The latter's unramifiedness witness is derived canonically from the
hypothesis for L/K.
Every representative of artinSymbol π hur is an arithmetic Frobenius at some prime above
π.
Transport along an isomorphism of extensions #
An isomorphism e : L ββ[K] L' of extensions of K induces π L ββ[π K] π L', and everything
artinSymbol is built from travels along it: the primes above π, their unramifiedness, and the
Frobenius condition. The symbol itself is therefore equivariant for the induced isomorphism
AlgEquiv.autCongr e of Galois groups.
The Artin symbol is equivariant under an isomorphism of extensions. For e : L ββ[K] L',
the symbol computed in L' is the image of the one computed in L under the induced isomorphism
AlgEquiv.autCongr e of Galois groups.
The trivial Artin symbol #
Two equivalent readings of the identity Artin class at an unramified prime: residue degree one, and complete splitting.
The Artin symbol is trivial exactly at residue degree one. For a prime Q of π L above
an unramified π, the Artin symbol of π is the identity class if and only if f(Q/π) = 1.
The residue degree is common to all primes above π, so the choice of Q is immaterial.
The Artin symbol is trivial exactly at the completely split primes. For π unramified in
L, the Artin symbol of π is the identity class if and only if π splits completely, that is,
π L has [L : K] primes above π.
A caller who knows the prime count therefore knows the symbol, and conversely.
Raising the base field #
The companion to artinSymbol_map_restrictNormalHom. That law shrinks the top field of a normal
tower and takes no power; this one raises the base field and takes the power f(π/π).
Raising the base field raises the Artin symbol to the residue degree. For number fields
K β M β L with L / K Galois, π a prime of π K unramified in L / K, and π a prime of
π M over it: the Artin symbol of π for L / M, read inside Gal(L/K) along
AlgEquiv.restrictScalarsHom, is the f(π/π)-th power of the Artin symbol of π for L / K.
Only the L / K hypothesis is asked for. Unramifiedness of π in L / M follows from it: a
prime of π L above π lies above π, so it is unramified over π K, and
Algebra.IsUnramifiedAt.of_restrictScalars drops the base to π M.
This is the conjugacy-class form of NumberField.restrictScalars_arithFrobAt_eq_pow_inertiaDeg.
The gain over that element-level statement is that the choice it makes disappears. It is an
identity at a particular prime Q of π L; there is only one choice there, since at a fixed
unramified prime the Frobenius is uniquely determined, but the identity does fail for a conjugate
of Ο, which need not stabilize Q. Passing to conjugacy classes quotients by that choice and
so never has to name the Frobenius it determines β which is the form a Frobenius-class argument
can use, having no prime in hand.