Galois action on ideles, idele classes and S-ideles #
Let L/K be an extension of number fields. The automorphism group Aut(L/K) acts on the adeles
of L by ring automorphisms (TauCeti.GlobalNumberFields.adeleGaloisAction), hence on the ideles
I_L, and this action fixes the principal ideles setwise, so it descends to the idele class group
C_L = I_L / Lˣ. Both actions are recorded in the scope AdeleGaloisAction, beside the action on
the adeles, so that they do not compete with other actions on these groups. A field isomorphism
e : L ≃+* M transports idele classes, C_L ≃* C_M (ideleClassEquiv), and for a
K-isomorphism this transport carries the action of Aut(L/K) to that of Aut(M/K) along
conjugation by e (ideleClassEquiv_smul).
These actions are continuous. Transport of idele classes along a field isomorphism is a
homeomorphism, since it is induced by the continuous transport of adeles, and the action of
σ ∈ Aut(L/K) on C_L is the transport along σ itself. With the discrete topology on
Aut(L/K), the actions on I_L and C_L are jointly continuous.
For a set S of finite places of K, the S-ideles I_{L,S} are the ideles of L that are
units at every finite place of L not above S. They form a subgroup stable under Aut(L/K)
(smul_mem_sIdeles), and the principal ideles in it are exactly those of the S-units of L
(unitEmbedding_mem_sIdeles_iff), the units of L at every finite place not above S. When the
classes of the primes above S generate the ideal class group of L, every idele class is the
class of an S-idele (exists_mem_sIdeles_mk_eq), so that
C_L = I_{L,S} / U_{L,S}.
This is the form in which the cohomology of the idele classes of a cyclic extension is computed
from that of the S-ideles and the S-units.
Main definitions #
TauCeti.GlobalNumberFields.ideleMulDistribMulAction: the action ofAut(L/K)onI_L.TauCeti.GlobalNumberFields.ideleClassMulDistribMulAction: the action ofAut(L/K)onC_L.TauCeti.GlobalNumberFields.ideleClassEquiv e: the transportC_L ≃* C_Malong a field isomorphisme : L ≃+* M.TauCeti.GlobalNumberFields.sIdeles L S: theS-ideles ofL.
Main results #
TauCeti.GlobalNumberFields.smul_unitEmbedding: the action on principal ideles is the action onLˣ.TauCeti.GlobalNumberFields.ideleClassEquiv_smul: transport of idele classes along aK-isomorphism is Galois equivariant.TauCeti.GlobalNumberFields.isHomeomorph_ideleClassEquiv: transport of idele classes along a field isomorphism is a homeomorphism.TauCeti.GlobalNumberFields.continuous_idele_smulandTauCeti.GlobalNumberFields.continuous_ideleClass_smul: the Galois actions on ideles and idele classes are continuous.TauCeti.GlobalNumberFields.smul_mem_sIdeles: theS-ideles are stable underAut(L/K).TauCeti.GlobalNumberFields.unitEmbedding_mem_sIdeles_iff: a principal idele is anS-idele exactly when it comes from anS-unit.TauCeti.GlobalNumberFields.exists_mem_sIdeles_mk_eq: every idele class is the class of anS-idele, when the primes aboveSgenerate the class group.
References #
- J. S. Milne, Class Field Theory, Chapter VII, §4.
- J. Neukirch, Algebraic Number Theory, Chapter VI, §§1–2.
The Galois action on ideles and idele classes #
The Galois action on ideles: σ ∈ Aut(L/K) acts on the units of the adele ring of L by
the ring automorphism TauCeti.GlobalNumberFields.adeleGaloisAction K L σ. It is a definition
rather than a global instance, available as an instance in the scope AdeleGaloisAction.
Instances For
The Galois action on an idele is the Galois action on the underlying adele.
The Galois action on an idele is Units.map of the Galois action on adeles, the form in which
it is written elsewhere.
The finite part of σ • x is the image of the finite part of x under the Galois action on
finite adeles.
The infinite part of σ • x is the image of the infinite part of x under the Galois action
on infinite adeles.
The idele with finite part σ a and infinite part 1 is σ applied to the idele with
finite part a and infinite part 1.
The Galois action on principal ideles is the Galois action on Lˣ.
The Galois action preserves the principal ideles.
The Galois action on idele classes, induced by the Galois action on ideles, which
preserves the principal ideles. It is a definition rather than a global instance, available as an
instance in the scope AdeleGaloisAction.
Instances For
The Galois action on the class of an idele is the class of the Galois action on the idele.
Transport of idele classes along field isomorphisms #
Transport of ideles along a field isomorphism e : L ≃+* M maps the principal ideles of L
onto those of M.
Transport of idele classes along a field isomorphism: an isomorphism e : L ≃+* M of
number fields induces C_L ≃* C_M, sending the class of an idele a of L to the class of its
transport adeleEquiv L M e a (ideleClassEquiv_mk).
Instances For
ideleClassEquiv e sends the class of an idele a to the class of its transport along
adeleEquiv L M e.
The inverse of the transport of idele classes along e is the transport along e.symm.
Transport of idele classes along the identity field isomorphism is the identity.
Transport of idele classes respects composition of field isomorphisms.
Transport of idele classes is Galois equivariant: along a K-isomorphism e : L ≃ₐ[K] M,
the action of σ ∈ Aut(L/K) on C_L corresponds to the action of its conjugate
e σ e⁻¹ ∈ Aut(M/K) (AlgEquiv.autCongr) on C_M.
Continuity #
Transport of idele classes along a field isomorphism is continuous. It is induced by the
transport of ideles, which is continuous for the units topology because the transport of adeles
adeleEquiv L M e is continuous.
Transport of idele classes along a field isomorphism is a homeomorphism: its inverse is
the transport along e.symm, which is continuous as well.
The Galois action of σ ∈ Aut(L/K) on idele classes is the transport of idele classes along
the field automorphism σ.
The Galois action on ideles is continuous: each σ ∈ Aut(L/K) acts on the ideles by
Units.map of the continuous ring automorphism adeleGaloisAction K L σ of the adeles, which is
continuous for the units topology.
The Galois action on idele classes is continuous, being the transport of idele classes along a field automorphism.
Each σ ∈ Aut(L/K) acts continuously on the ideles.
Each σ ∈ Aut(L/K) acts continuously on the idele classes.
With the discrete topology on field automorphisms, the Galois action on ideles is jointly continuous.
With the discrete topology on field automorphisms, the Galois action on idele classes is jointly continuous.
S-ideles #
The S-ideles. For a set S of finite places of K, the ideles of L whose component
at every finite place of L not above S is a unit of the ring of integers of the completion.
Every infinite component is unconstrained.
Instances For
An idele is an S-idele exactly when its component at every finite place not above S has
valuation one.
The S-ideles grow with S.
Every idele is an S-idele for a finite set S of finite places: its finite components
are units of the rings of integers at all but finitely many places. The set S may be taken to
contain any given finite set S₀.
An idele whose finite components are all 1 is an S-idele.
A principal idele is an S-idele exactly when it comes from an S-unit of L, a unit at
every finite place of L not above S.
The principal S-ideles are those of the S-units: Lˣ ∩ I_{L,S} = U_{L,S}. This is
NumberField.IdeleGroup.mem_principalSubgroup_iff_exists_mem_unit read on sIdeles L S.
Every idele class is the class of an S-idele, when the classes of the primes of L
above S generate the ideal class group of L: I_L = Lˣ · I_{L,S}. This is
NumberField.IdeleClassGroup.exists_valued_ideleFiniteCoord_eq_one_and_mk_eq read on
sIdeles L S.
The S-ideles are stable under the Galois action. Since S is a set of places of K,
the places of L not above S are permuted by Aut(L/K).
The Galois action of Aut(L/K) on the S-ideles, restricted from the action on ideles.
The Galois action on an S-idele is the Galois action on the underlying idele.
The S-units are stable under the Galois action: they are the units whose principal
ideles are S-ideles.
The Galois action of Aut(L/K) on the S-units of L, restricted from the action on
Lˣ.
The Galois action on an S-unit is the Galois action on the underlying unit.