The levels of the idele-class formation #
Let K be a number field with separable closure Kˢ and absolute Galois group G_K, and let
U be an open subgroup of G_K with fixed field E, a finite subextension of Kˢ/K that need not
be Galois over K.
This file identifies the level (C_{Kˢ})^U of the idele-class formation globalFormation K with
the idele class group C_E = I_E / Eˣ of E (ideleClassLevelEquiv):
C_E ≃ (C_{Kˢ})^U.
The map sends the class of an idele a of E to the class of a regarded as an idele of Kˢ.
- It is surjective by Hilbert 90 for
U: an idele class fixed byUis the class of an idele fixed byU(exists_ideleClassMk_eq_of_isClosed), which is an idele ofEby Galois descent for ideles (mem_range_ideleCoeffOfIntermediateField_iff). - It is injective because a principal idele of
Kˢthat is an idele ofEcomes from a unit ofKˢfixed byU, that is, from a unit ofE(mem_level_unitsFormation_iff).
The identification is Galois equivariant: an element of G_K restricting to an automorphism e
of E acts on the level as e acts on C_E (ideleClassLevelEquiv_units_map_adeleEquiv), which
for E Galois over K is the action of Gal(E/K) (ideleClassLevelEquiv_smul). It is the map
induced on idele classes by the identification ideleLevelEquiv of the corresponding level of the
idele formation with I_E (ideleClassHom_ideleLevelEquiv). For an arbitrary layer V ◁ U of
globalFormation K, with fixed fields L ⊇ F, it identifies the coefficient module of the layer
with C_L, on which U acts through its restrictions to L, and its ground level with C_F.
At the ground, U = G_K and E is the bottom subextension, the image of K in Kˢ; reading
C_E as C_K through extension of ideles gives globalGroundEquiv K : C_K ≃ (C_{Kˢ})^{G_K}, the
ground level of every layer V ◁ G_K, that is, of every finite Galois extension of K.
Main definitions #
TauCeti.ClassFieldTheory.ideleClassLevelEquiv hU: the level of the idele-class formation at an open subgroup with fixed fieldEis the idele class group ofE.TauCeti.ClassFieldTheory.globalGroundEquiv K: the ground level of the idele-class formation is the idele class group ofK.
Main results #
TauCeti.ClassFieldTheory.ideleClassLevelEquiv_mk: the class of an idele ofEgoes to the class of the same idele ofKˢ.TauCeti.ClassFieldTheory.ideleClassLevelEquiv_units_map_adeleEquiv,TauCeti.ClassFieldTheory.ideleClassLevelEquiv_smul:ideleClassLevelEquivis Galois equivariant.TauCeti.ClassFieldTheory.ideleClassHom_ideleLevelEquiv: it is compatible withideleLevelEquivand the quotient map from ideles to idele classes.TauCeti.ClassFieldTheory.globalGroundEquiv_mk: the class of an idele ofKgoes to the class of its extension toKˢ.TauCeti.ClassFieldTheory.coe_ideleClassLevelEquiv_ideleClassExtensionandTauCeti.ClassFieldTheory.LayerRestriction.groundInclusion_ideleClassLevelEquiv: extension of idele classes agrees with inclusion of levels.
References #
- J. Neukirch, Algebraic Number Theory, Chapter VI, §2.
The level of the idele-class formation is the idele class group of the fixed field: if
the fixed field of the open subgroup U is the finite subextension E, then sending the class of
an idele of E to its class as an idele of Kˢ identifies the idele class group
C_E = I_E / Eˣ with the level (C_{Kˢ})^U of globalFormation K. Applied to the open normal
subgroup fixing a finite Galois extension L/K, it identifies the top level of the layer of L
with C_L; applied to the two subgroups of an arbitrary layer V ◁ U, it identifies its
coefficient module and its ground level with the idele class groups of their fixed fields.
Instances For
ideleClassLevelEquiv hU sends the class of an idele of E to the class of the same idele
of Kˢ.
ideleClassLevelEquiv is Galois equivariant: if g ∈ G_K restricts on E to the
automorphism e of E, then g acts on the level as e acts on the idele classes of E.
ideleClassLevelEquiv is Galois equivariant: if E is normal over K, then g ∈ G_K
acts on the level as its restriction to Gal(E/K) acts on the idele classes of E.
ideleClassLevelEquiv is induced by ideleLevelEquiv: the quotient map from ideles to
idele classes sends the idele of Kˢ attached to an idele a of E to the class of a.
Extension of idele classes is inclusion of levels. For finite subextensions F ⊆ E
inside Kˢ, extending an idele class from F to E does not change its image in the ambient
idele-class formation.
The ground inclusion of the idele-class formation is extension of idele classes.
If a layer restriction raises the ground field from F to E, its ground inclusion is the
usual map C_F → C_E under the fixed-field level identifications.
The ground level #
The ground level of the idele-class formation is the idele class group of K: extension
of ideles from K to Kˢ identifies C_K with the level (C_{Kˢ})^{G_K} of globalFormation K.
It is ideleClassLevelEquiv at the bottom subextension, read on C_K through the identification
of K with its image in Kˢ.
Instances For
globalGroundEquiv K sends the class of an idele of K to the class of its extension to
Kˢ.