The decomposition group acts on the completion #
Let L/K be an extension of number fields, v a finite place of K, and w a finite place of
L above v. An automorphism σ ∈ Aut(L/K) carries w to the place σ • w, and extends by
continuity to an isomorphism of completions L_w ≃ₐ[K_v] L_{σ • w}. This file constructs that
isomorphism, completionCongr, and restricts it to the decomposition group, the stabilizer of
w, to obtain the homomorphism
decompositionHom v w : MulAction.stabilizer (L ≃ₐ[K] L) w.asIdeal →* (L_w ≃ₐ[K_v] L_w).
When L/K is Galois this homomorphism is an isomorphism, decompositionEquiv: the
decomposition group of w is the Galois group of the local extension L_w/K_v. Injectivity
is density of L in L_w; surjectivity is a count. The decomposition group has e(w ∣ v) · f(w ∣ v) elements, that product is the local degree [L_w : K_v], and a finite extension of
fields has at most [L_w : K_v] automorphisms, so the embedding is already onto. The same count
shows that L_w/K_v is itself Galois.
The target place of completionCongr is an arbitrary w' together with the equation
w'.asIdeal = σ • w.asIdeal, so that no transport along an equality of places is needed.
Both completions carry the canonical K_v-algebra structure of completionAlgHom, which is
available in the AdicCompletionExtension scope.
Main definitions #
IsDedekindDomain.HeightOneSpectrum.completionCongr: the isomorphismL_w ≃ₐ[K_v] L_{w'}induced byσwhenw' = σ • w.IsDedekindDomain.HeightOneSpectrum.decompositionHom: the action of the decomposition group ofwonL_w.IsDedekindDomain.HeightOneSpectrum.decompositionEquiv: that action, as an isomorphism onto the local Galois group, whenL/Kis Galois.
Main results #
IsDedekindDomain.HeightOneSpectrum.valuation_apply_eq_of_asIdeal_eq_smul:σcarries thew-adic valuation to theσ • w-adic valuation.IsDedekindDomain.HeightOneSpectrum.completionCongr_algebraMapandIsDedekindDomain.HeightOneSpectrum.eq_completionCongr_of_continuous:completionCongrextendsσ, uniquely among continuous ring homomorphisms.IsDedekindDomain.HeightOneSpectrum.valued_completionCongr:completionCongrpreserves the completion valuations.IsDedekindDomain.HeightOneSpectrum.decompositionHom_algebraMap: the defining propertydecompositionHom v w τ x = τ xforx ∈ L;decompositionHom_algebraMap_ringOfIntegersis its form on𝓞 L, andvalued_decompositionHomsays the action preserves the valuation.IsDedekindDomain.HeightOneSpectrum.decompositionHom_injective: the decomposition group embeds intoAut(L_w/K_v).IsDedekindDomain.HeightOneSpectrum.decompositionHom_conj: compatibility with the action ofAut(L/K)on the places abovev; conjugating byσcorresponds to transporting alongcompletionCongr σ.IsDedekindDomain.HeightOneSpectrum.decompositionHom_surjectiveandIsDedekindDomain.HeightOneSpectrum.decompositionEquiv: forL/KGalois the decomposition group ofwis the Galois group ofL_w/K_v.IsDedekindDomain.HeightOneSpectrum.isGalois_adicCompletion: forL/KGalois the local extensionL_w/K_vis Galois; andIsDedekindDomain.HeightOneSpectrum.card_algEquiv_adicCompletion: a locally Galois completion hase(w ∣ v) · f(w ∣ v)automorphisms.IsDedekindDomain.HeightOneSpectrum.isCyclic_algEquiv_adicCompletion_of_isUnramifiedAt: at an unramified place the local Galois group is cyclic of orderf(w ∣ v).
References #
- [J. Neukirch, Algebraic Number Theory][Neukirch1992], Chapter II, §9.
An automorphism σ of L/K carries the w-adic valuation to the w'-adic valuation
when w' = σ • w.
The isomorphism of completions L_w ≃ₐ[K_v] L_{w'} induced by an automorphism σ of L/K
carrying w to w': the continuous extension of σ.
Equations
- v.completionCongr σ h = AlgEquiv.ofRingEquiv ⋯
Instances For
completionCongr v σ h extends σ.
completionCongr is continuous.
completionCongr is the only continuous ring homomorphism L_w →+* L_{w'} extending σ.
completionCongr preserves the valuations of the completions.
completionCongr of the identity is the identity.
completionCongr is multiplicative: transporting along σ and then along τ is
transporting along τ * σ.
The inverse of completionCongr v σ h is completionCongr of σ⁻¹.
The action of the decomposition group of w on the completion L_w: each element of the
stabilizer of w extends by continuity to a K_v-algebra automorphism of L_w.
Equations
- v.decompositionHom w = { toFun := fun (τ : ↥(MulAction.stabilizer Gal(L/K) w.asIdeal)) => v.completionCongr ↑τ ⋯, map_one' := ⋯, map_mul' := ⋯ }
Instances For
An element of the decomposition group acts on L_w by completionCongr.
The defining property of decompositionHom: on L it is the action of the automorphism.
On the ring of integers of L, decompositionHom is the action of the automorphism.
The action of the decomposition group on L_w preserves the valuation of L_w.
Each element of the decomposition group acts continuously on L_w.
The decomposition group of w acts faithfully on L_w.
Compatibility of decompositionHom with the action on places. If σ carries w to
w' and τ stabilizes w, then the action of σ τ σ⁻¹ on L_{w'} is the action of τ on
L_w transported along completionCongr σ.
The decomposition group is the local Galois group #
The decomposition group of w has order the local degree. For L/K Galois the
decomposition group of w has e(w ∣ v) · f(w ∣ v) elements, and that product is the degree
of L_w over K_v.
The decomposition group of w exhausts Aut(L_w/K_v). For L/K Galois every
K_v-algebra automorphism of L_w is the continuous extension of an automorphism of L/K
stabilizing w.
The decomposition group of w is the Galois group of L_w/K_v.
Equations
- v.decompositionEquiv w = MulEquiv.ofBijective (v.decompositionHom w) ⋯
Instances For
A completion of a Galois extension is Galois. For L/K Galois the local extension
L_w/K_v at a finite place w of L is a Galois extension.
The local Galois group at w has order e(w ∣ v) · f(w ∣ v).
The local Galois group at an unramified place #
The local Galois group at an unramified place has order f(w ∣ v).
The local Galois group at an unramified place is cyclic.