The idele formation and the idele-class formation of a number field #
For a number field K with separable closure Kˢ and absolute Galois group G_K, this file
assembles the two global formations on G_K:
ideleFormation K, whose coefficient module is the idelesI_{Kˢ}ofKˢ(TauCeti.ClassFieldTheory.IdeleCoeff K);globalFormation K, whose coefficient module is the idele classesC_{Kˢ} = I_{Kˢ} / (Kˢ)ˣ(TauCeti.ClassFieldTheory.IdeleClassCoeff K).
Together with the formation TauCeti.ClassFieldTheory.unitsFormation K of the multiplicative
group (Kˢ)ˣ, they are the three terms of the exact sequence 0 → (Kˢ)ˣ → I_{Kˢ} → C_{Kˢ} → 0
of discrete G_K-modules given by principalIdele and ideleClassMk. The global class
formation lives on globalFormation K, while the local invariants are summed on the second
cohomology of the layers of ideleFormation K.
By Galois descent for ideles (mem_range_ideleCoeffOfIntermediateField_iff), the level of
ideleFormation K at every open subgroup U is the idele group I_E of its fixed field E, a
finite subextension of Kˢ/K that need not be Galois over K (ideleLevelEquiv). An element of
G_K restricting to an automorphism e of E acts on it by transport along e
(ideleLevelEquiv_units_map_adeleEquiv); when E is Galois over K, this is the action of
Gal(E/K) (ideleLevelEquiv_smul). So for a finite Galois extension L/K inside Kˢ, the
coefficient module of the layer of L is the Gal(L/K)-module I_L, and the second cohomology
of that layer is H²(Gal(L/K), I_L); for a layer V ◁ U with fixed fields E ⊇ F, its top and
ground levels are I_E and I_F.
Both coefficient modules are discrete with open stabilizers, so the continuous cohomology of G_K
with coefficients in either of them is the colimit of the cohomology of the finite quotients
G_K ⧸ U with coefficients in the U-invariants, by the general
TauCeti.ContCohomology.continuousFiniteQuotientColimit.
Main definitions #
TauCeti.ClassFieldTheory.ideleFormation K: the formation of the ideles ofKˢ.TauCeti.ClassFieldTheory.globalFormation K: the formation of the idele classes ofKˢ.TauCeti.ClassFieldTheory.ideleCoeffEquivIdeleFormation K,TauCeti.ClassFieldTheory.ideleClassCoeffEquivGlobalFormation K: their coefficient modules asIdeleCoeff KandIdeleClassCoeff K.TauCeti.ClassFieldTheory.ideleLevelEquiv hU: the level of the idele formation at an open subgroup with fixed fieldEis the idele groupI_E.
Main results #
TauCeti.ClassFieldTheory.mem_level_ideleFormation_iff: the level of the idele formation at an open subgroup with fixed fieldEconsists of the ideles ofE.TauCeti.ClassFieldTheory.ideleLevelEquiv_units_map_adeleEquiv,TauCeti.ClassFieldTheory.ideleLevelEquiv_smul:ideleLevelEquivis Galois equivariant.
Implementation notes #
As for unitsFormation, the bodies of the formations are not exposed, and their coefficient
modules are read through the equivariant dictionaries ideleCoeffEquivIdeleFormation and
ideleClassCoeffEquivGlobalFormation.
References #
- J. Neukirch, Algebraic Number Theory, Chapter VI, §2.
The idele formation #
The idele formation of a number field K: the discrete module I_{Kˢ} of ideles of the
separable closure, written additively as IdeleCoeff K, over the absolute Galois group G_K.
Instances For
The coefficient dictionary between IdeleCoeff K and the coefficient module of
ideleFormation K. It is equivariant by ideleCoeffEquivIdeleFormation_smul.
Instances For
The coefficient dictionary of the idele formation is equivariant: G_K acts on the
coefficient module of ideleFormation K as it acts on the ideles of Kˢ.
The idele-class formation #
The idele-class formation of a number field K: the discrete module C_{Kˢ} of idele
classes of the separable closure, written additively as IdeleClassCoeff K, over the absolute
Galois group G_K.
Instances For
The coefficient dictionary between IdeleClassCoeff K and the coefficient module of
globalFormation K. It is equivariant by ideleClassCoeffEquivGlobalFormation_smul.
Instances For
The coefficient dictionary of the idele-class formation is equivariant: G_K acts on the
coefficient module of globalFormation K as it acts on the idele classes of Kˢ.
The levels of the idele formation #
The level of the idele formation at an open subgroup with fixed field E consists of the
ideles of E.
The level of the idele formation is the idele group of the fixed field: if the fixed
field of the open subgroup U is the finite subextension E, then ideleCoeffOfIntermediateField
identifies the ideles I_E of E with the level (I_{Kˢ})^U of ideleFormation 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 I_L.
Instances For
ideleLevelEquiv hU sends an idele of E to the same idele of Kˢ.
ideleLevelEquiv 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 ideles of E.
ideleLevelEquiv 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 ideles of E.