Admissible moduli and ramification #
Let L/K be a finite abelian extension of number fields and πͺ a modulus of K admissible for
L/K. This file shows that the exponents of the conductor of L/K are its local conductor
exponents, so that πͺ bounds them, and, in particular, that every prime of K ramified in L
divides πͺ, and that every real place of K ramified in L belongs to πͺ. Conversely, an
extension unramified at every finite prime admits every modulus carrying its ramified real places;
this identifies the extensions admitting the trivial and the narrow modulus.
Let v be a finite place of K and w a place of L above it. The class of the idele
concentrated at v with component u β K_vΛ£ is a norm from C_L exactly when its global Artin
symbol is trivial. By localβglobal compatibility (globalArtinMap_local) that symbol is the local
Artin symbol of u, and for an abelian extension the local Artin symbols that vanish are exactly
the norms from L_w (localArtinAt_eq_one_iff_mem_normGroup). So that class is a norm exactly
when u is a norm from L_w (ofAdicCompletion_mem_range_ideleClassNormMap_iff). Since the
exponent of v in the conductor is read off from these classes
(exponent_abelianConductor_le_iff), it is the conductor exponent of L_w/K_v
(exponent_abelianConductor). As πͺ is a multiple of the conductor, the conductor exponent of
L_w/K_v is at most the exponent of v in πͺ
(IsAdmissibleModulus.conductorExponent_le_exponent).
The same argument applies to the fixed field of a subgroup H β€ Gal(L/K). Its idele class at
v is a norm exactly when the local Artin symbol of u, an element of the decomposition group
D_w β
Gal(L_w/K_v), lies in H. By local reciprocity this happens exactly when u is a norm
from the fixed field of H β© D_w in L_w (mem_normGroup_fixedField_iff,
ofAdicCompletion_mem_range_ideleClassNormMap_fixedField_iff). Hence the exponent of v in the
conductor of the fixed field of H is the local conductor exponent of the fixed field of
H β© D_w (exponent_abelianConductor_fixedField). For H = ker Ο this is the Artin conductor
exponent f(Ο|_{D_w}) (conductorExponent_fixedField_ker,
exponent_abelianConductor_fixedField_ker).
If v is not in the support of πͺ, then its exponent in πͺ is 0, so every unit of K_v is a
norm from L_w. By the unramified criterion of local class field theory
(conductorExponent_eq_zero_iff), L_w/K_v is unramified, and since the local ramification
index is the global one, so is w over v
(IsAdmissibleModulus.isUnramifiedAt_of_notMem_support). Contrapositively, a prime of K below
a ramified prime of L lies in the support of every admissible modulus
(IsAdmissibleModulus.mem_support_of_ramified). Equivalently, the support of an admissible
modulus contains the primes dividing the relative discriminant
(IsAdmissibleModulus.ramifiedSupport_subset_support); this applies in particular to the conductor
abelianConductor K L, which is admissible.
At an infinite place v of K outside the real places of πͺ, the idele class that is -1 at
v lies in the ray subgroup of πͺ, hence is a norm, so its global Artin symbol vanishes. By
globalArtinMap_infiniteLocal that symbol is the local Artin symbol of -1 at v, so -1 is a
norm from L_w for a place w of L above v (infiniteLocalArtinAt_eq_one_iff_mem_normGroup).
If w were ramified, L_w/K_v would be β/β, whose norms are positive. Hence w is unramified
(IsAdmissibleModulus.isUnramified_of_forall_ne).
Conversely (isAdmissibleModulus_of_isUnramifiedAt), suppose that L/K is Galois and unramified
at every finite prime, and that the infinite places of L above the infinite places of K
outside the real places of πͺ are unramified. The finite components of a congruence idele x
for πͺ are units, so their local Artin symbols vanish at the unramified finite places
(localArtinAt_eq_one_of_normalizedValuation_eq_one). Its components at the real places of πͺ
are positive, and the places above the other infinite places are unramified, so its archimedean
local Artin symbols vanish too. By the localβglobal character formula, the global Artin symbol
of the class of x vanishes (globalArtinMap_eq_zero_of_forall_eq_one), that is, the class is a
norm. In particular, for L/K abelian, the trivial modulus is admissible exactly
when L/K is unramified at every finite prime and at every infinite place
(isAdmissibleModulus_one_iff), and the modulus narrowModulus K carrying every real place is
admissible exactly when L/K is unramified at every finite prime
(isAdmissibleModulus_narrowModulus_iff). These describe the abelian extensions contained in the
Hilbert class field and in the narrow Hilbert class field.
The abelian hypothesis cannot be dropped. By norm limitation, the norm group of β(β2)/β is the
whole idele class group, so the trivial modulus is admissible for it, although 2 and 3 ramify.
Main results #
TauCeti.ClassFieldTheory.ofAdicCompletion_mem_range_ideleClassNormMap_iff: the class of an idele concentrated atvis a norm fromLexactly when its component is a norm fromL_w.TauCeti.ClassFieldTheory.exponent_abelianConductor: the exponent ofvin the conductor ofL/Kis the conductor exponent ofL_w/K_v.TauCeti.ClassFieldTheory.exponent_abelianConductor_fixedField: the exponent ofvin the conductor of the fixed field ofH β€ Gal(L/K)is the local conductor exponent of the fixed field of the corresponding subgroup ofGal(L_w/K_v).TauCeti.ClassFieldTheory.exponent_abelianConductor_fixedField_ker: the exponent ofvin the conductor of a characterΟofGal(L/K)is the Artin conductor exponent of the restriction ofΟtoGal(L_w/K_v).TauCeti.ClassFieldTheory.IsAdmissibleModulus.conductorExponent_le_exponent: the conductor exponent ofL_w/K_vis at most the exponent ofvin an admissible modulus.TauCeti.ClassFieldTheory.IsAdmissibleModulus.isUnramifiedAt_of_notMem_support: a prime ofLover a place outside the support of an admissible modulus is unramified.TauCeti.ClassFieldTheory.IsAdmissibleModulus.mem_support_of_ramified: a prime ofKbelow a ramified prime ofLlies in the support of every admissible modulus.TauCeti.ClassFieldTheory.IsAdmissibleModulus.isUnramifiedAway: the same, for every prime ofLabove a place outside the support, in the form taken by the ideal-theoretic Artin map.TauCeti.ClassFieldTheory.IsAdmissibleModulus.isUnramifiedAt_of_integralIdealsPrimeTo: the same, for every prime ofLabove a prime ideal ofKprime toπͺ.TauCeti.ClassFieldTheory.IsAdmissibleModulus.ramifiedSupport_subset_support: the ramified support ofL/Kis contained in the support of every admissible modulus.TauCeti.ClassFieldTheory.IsAdmissibleModulus.isUnramified_of_forall_ne: an infinite place ofLover an infinite place outside the real places of an admissible modulus is unramified.TauCeti.ClassFieldTheory.isAdmissibleModulus_of_isUnramifiedAt: an extension unramified at every finite prime admits every modulus carrying its ramified real places.TauCeti.ClassFieldTheory.isAdmissibleModulus_one_iff: the trivial modulus is admissible exactly for extensions unramified at every finite and every infinite place.TauCeti.ClassFieldTheory.isAdmissibleModulus_narrowModulus_iff: the narrow modulus is admissible exactly for extensions unramified at every finite prime.
References #
- J. S. Milne, Class Field Theory, v4.03, Chapter V (the conductor of an abelian extension).
- J. Neukirch, Algebraic Number Theory, Chapter VI, Β§6, and Chapter VII, Β§11.
- J.-P. Serre, Corps Locaux, Chapter VI, Β§3.
Idele classes concentrated at one place that are norms. For an abelian extension L/K, a
finite place v of K and a place w of L above it, the class of the idele concentrated at
v with component u is a norm from L exactly when u is a norm from L_w.
The exponents of the conductor are the local conductor exponents. For an
abelian extension L/K, a finite place v of K and a place w of L above it, the exponent
of v in the conductor of L/K is the conductor exponent of L_w/K_v.
Idele classes concentrated at one place that are norms from a subextension. Let L/K be
abelian, H a subgroup of Gal(L/K), v a finite place of K and w a place of L above it.
The class of the idele concentrated at v with component u is a norm from the fixed field of
H exactly when u is a norm from the fixed field in L_w of the subgroup of Gal(L_w/K_v)
corresponding to H under the decomposition group of w.
The conductor of a subextension at a finite place. Let L/K be abelian, H a subgroup
of Gal(L/K), v a finite place of K and w a place of L above it. The exponent of v in
the conductor of the fixed field of H is the conductor exponent of the fixed field in L_w of
the subgroup of Gal(L_w/K_v) corresponding to H under the decomposition group of w.
The conductor of a character at a finite place is a local Artin conductor. Let L/K be
abelian, Ο a homomorphism on Gal(L/K), v a finite place of K and w a place of L above
it. The exponent of v in the conductor of the fixed field of ker Ο is the Artin conductor
exponent of Ο restricted to Gal(L_w/K_v), the decomposition group of w.
An admissible modulus bounds the local conductors. For an abelian extension L/K, a
modulus πͺ admissible for L/K, a finite place v of K and a place w of L above it, the
conductor exponent of L_w/K_v is at most the exponent of v in πͺ.
Primes outside an admissible modulus are unramified. For an abelian extension L/K and a
modulus πͺ admissible for L/K, every prime of L above a finite place v of K outside the
support of πͺ is unramified over K.
Ramified primes divide every admissible modulus. For an abelian extension L/K and a
modulus πͺ admissible for L/K, a finite place v of K below a prime of L ramified over K
lies in the support of πͺ.
An admissible modulus bounds the ramification. For an abelian extension L/K and a
modulus πͺ admissible for L/K, every prime of L above a finite place of K outside the
support of πͺ is unramified over K. This is the unramifiedness hypothesis of the
ideal-theoretic Artin map NumberFieldArithmetic.artinHomAway for the excluded set πͺ.support.
Primes prime to an admissible modulus are unramified. For an abelian extension L/K and a
modulus πͺ admissible for L/K, every prime of L above a prime ideal of K prime to πͺ is
unramified over K.
The ramified support lies in the support of every admissible modulus. For an abelian
extension L/K, every prime of K dividing the relative discriminant of L/K divides every
modulus admissible for L/K, in particular the conductor abelianConductor K L.
Infinite places outside an admissible modulus are unramified. For an abelian extension
L/K and a modulus πͺ admissible for L/K, every infinite place of L above an infinite place
v of K that is not one of the real places of πͺ is unramified over K: if v is real, the
places of L above it are real.
Unramified extensions #
Unramified extensions admit every modulus carrying their ramified real places. Let L/K
be a finite Galois extension of number fields that is unramified at every finite prime, and let
πͺ be a modulus such that every infinite place of L above an infinite place of K outside the
real places of πͺ is unramified. Then πͺ is admissible for L/K.
The trivial modulus is admissible exactly for unramified extensions. For an abelian
extension L/K of number fields, the trivial modulus is admissible for L/K exactly when L/K
is unramified at every finite prime and at every infinite place.
The narrow modulus is admissible exactly for extensions unramified at the finite primes.
For an abelian extension L/K of number fields, the modulus narrowModulus K, trivial at the
finite places and carrying every real place, is admissible for L/K exactly when L/K is
unramified at every finite prime.