The decomposition group of an infinite place acts on the completion

Let L/K be an extension of number fields, v an infinite place of K, and w an infinite place of L above v. An automorphism σ ∈ Aut(L/K) carries w to the place σ • w, and it is an isometry from L with the absolute value w to L with the absolute value σ • w (apply_eq_of_eq_smul). It therefore extends by continuity to an isomorphism of completions L_w ≃ₐ[K_v] L_{σ • w}, completionCongr. Restricted to the stabilizer of w, its decomposition group, this gives

decompositionHom v w : MulAction.stabilizer (L ≃ₐ[K] L) w →* (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 L_w/K_v. Injectivity is density of L in L_w; surjectivity is a count. The decomposition group has one element when w is unramified over K and two when it is ramified, which is the local degree [L_w : K_v], and a finite extension of fields has at most [L_w : K_v] automorphisms.

The target place of completionCongr is an arbitrary w' together with the equation w' = σ • w, so that no transport along an equality of places is needed. Both completions carry the K_v-algebra structure NumberField.LiesOver.completionMap, available in the NumberField.LiesOver scope.

These are the archimedean counterparts of IsDedekindDomain.HeightOneSpectrum.completionCongr, IsDedekindDomain.HeightOneSpectrum.decompositionHom and IsDedekindDomain.HeightOneSpectrum.decompositionEquiv at the finite places. Like them, they are what identifies the units of K_v ⊗[K] L ≃ ∏_{w ∣ v} L_w with a representation coinduced from the decomposition group.

Main definitions

• NumberField.InfinitePlace.completionCongr: the isomorphism L_w ≃ₐ[K_v] L_{w'} induced by σ when w' = σ • w.
• NumberField.InfinitePlace.decompositionHom: the action of the decomposition group of w on L_w.
• NumberField.InfinitePlace.decompositionEquiv: that action, as an isomorphism onto the local Galois group, when L/K is Galois.

Main results

• NumberField.InfinitePlace.completionCongr_algebraMap and NumberField.InfinitePlace.eq_completionCongr_of_continuous: completionCongr extends σ, uniquely among continuous maps.
• NumberField.InfinitePlace.decompositionHom_injective: the decomposition group embeds into Aut(L_w/K_v), and restrictNormalHom_restrictScalarsHom_decompositionHom says that restricting its action back to L recovers the automorphism.
• NumberField.InfinitePlace.stabilizer_eq_bot_of_adjoin_eq_top: the decomposition group is trivial when L is generated over K by elements whose images in L_w come from K_v; for L/K Galois the local degree is then one (NumberField.InfinitePlace.finrank_completion_eq_one_of_adjoin_eq_top).
• NumberField.InfinitePlace.card_stabilizer_eq_finrank_completion: for L/K Galois the decomposition group has [L_w : K_v] elements.
• NumberField.InfinitePlace.finrank_completion_eq_ite: for L/K Galois, [L_w : K_v] is 1 or 2 according as v is unramified in L or not.
• NumberField.InfinitePlace.decompositionHom_surjective: for L/K Galois every K_v-automorphism of L_w comes from the decomposition group.
• NumberField.InfinitePlace.isGalois_completion: L_w/K_v is Galois.

References

• [J. Neukirch, Algebraic Number Theory][Neukirch1992], Chapter II, §8 and §9.

theorem NumberField.InfinitePlace.apply_eq_of_eq_smul {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] (σ : Gal(L/K)) {w w' : InfinitePlace L} (h : w' = σ • w) (x : L) : w' (σ x) = w x

An automorphism σ of L/K carries the absolute value w to the absolute value w' when w' = σ • w.

instance NumberField.InfinitePlace.liesOver_smul {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] (v : InfinitePlace K) (σ : Gal(L/K)) (w : InfinitePlace L) [w.LiesOver v] : (σ • w).LiesOver v

The Galois action on the places of L preserves the places above a place v of K.

noncomputable def NumberField.InfinitePlace.completionCongr {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] (v : InfinitePlace K) (σ : Gal(L/K)) {w w' : InfinitePlace L} [w.LiesOver v] [w'.LiesOver v] (h : w' = σ • w) : w.Completion ≃ₐ[v.Completion] w'.Completion

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 σ.

@[simp]

theorem NumberField.InfinitePlace.completionCongr_algebraMap {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] {v : InfinitePlace K} {w w' : InfinitePlace L} [w.LiesOver v] [w'.LiesOver v] (σ : Gal(L/K)) (h : w' = σ • w) (x : L) : (v.completionCongr σ h) (Completion.ofCompletion ↑(WithAbs.toAbs (↑w) x)) = Completion.ofCompletion ↑(WithAbs.toAbs (↑w') (σ x))

completionCongr v σ h extends σ.

theorem NumberField.InfinitePlace.continuous_completionCongr {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] (v : InfinitePlace K) {w w' : InfinitePlace L} [w.LiesOver v] [w'.LiesOver v] (σ : Gal(L/K)) (h : w' = σ • w) : Continuous ⇑(v.completionCongr σ h)

completionCongr is continuous.

theorem NumberField.InfinitePlace.eq_completionCongr_of_continuous {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] {v : InfinitePlace K} {w w' : InfinitePlace L} [w.LiesOver v] [w'.LiesOver v] (σ : Gal(L/K)) (h : w' = σ • w) {f : w.Completion → w'.Completion} (hf : Continuous f) (hfL : ∀ (x : L), f ((algebraMap L w.Completion) x) = (algebraMap L w'.Completion) (σ x)) : f = ⇑(v.completionCongr σ h)

completionCongr is the only continuous map L_w → L_{w'} extending σ.

@[simp]

theorem NumberField.InfinitePlace.completionCongr_one {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] {v : InfinitePlace K} {w : InfinitePlace L} [w.LiesOver v] : v.completionCongr 1 ⋯ = AlgEquiv.refl

completionCongr of the identity is the identity.

@[simp]

theorem NumberField.InfinitePlace.completionCongr_trans {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] {v : InfinitePlace K} {w w' : InfinitePlace L} [w.LiesOver v] [w'.LiesOver v] {w'' : InfinitePlace L} [w''.LiesOver v] (σ τ : Gal(L/K)) (hσ : w' = σ • w) (hτ : w'' = τ • w') : (v.completionCongr σ hσ).trans (v.completionCongr τ hτ) = v.completionCongr (τ * σ) ⋯

completionCongr is multiplicative: transporting along σ and then along τ is transporting along τ * σ.

@[simp]

theorem NumberField.InfinitePlace.completionCongr_symm {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] {v : InfinitePlace K} {w w' : InfinitePlace L} [w.LiesOver v] [w'.LiesOver v] (σ : Gal(L/K)) (h : w' = σ • w) : (v.completionCongr σ h).symm = v.completionCongr σ⁻¹ ⋯

The inverse of completionCongr v σ h is completionCongr of σ⁻¹.

noncomputable def NumberField.InfinitePlace.decompositionHom {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] (v : InfinitePlace K) (w : InfinitePlace L) [w.LiesOver v] : ↥(MulAction.stabilizer Gal(L/K) w) →* Gal(w.Completion/v.Completion)

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.

theorem NumberField.InfinitePlace.decompositionHom_apply {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] {v : InfinitePlace K} {w : InfinitePlace L} [w.LiesOver v] (τ : ↥(MulAction.stabilizer Gal(L/K) w)) : (v.decompositionHom w) τ = v.completionCongr ↑τ ⋯

An element of the decomposition group acts on L_w by completionCongr.

@[simp]

theorem NumberField.InfinitePlace.decompositionHom_algebraMap {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] {v : InfinitePlace K} {w : InfinitePlace L} [w.LiesOver v] (τ : ↥(MulAction.stabilizer Gal(L/K) w)) (x : L) : ((v.decompositionHom w) τ) (Completion.ofCompletion ↑(WithAbs.toAbs (↑w) x)) = Completion.ofCompletion ↑(WithAbs.toAbs (↑w) (↑τ x))

The defining property of decompositionHom: on L it is the action of the automorphism.

@[simp]

theorem NumberField.InfinitePlace.restrictNormalHom_restrictScalarsHom_decompositionHom {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] {v : InfinitePlace K} {w : InfinitePlace L} [w.LiesOver v] [Normal K L] (τ : ↥(MulAction.stabilizer Gal(L/K) w)) : ((AlgEquiv.restrictNormalHom L).comp (AlgEquiv.restrictScalarsHom K)) ((v.decompositionHom w) τ) = ↑τ

Restricting the action of an element of the decomposition group on L_w back to L recovers the element: composing decompositionHom with restriction Aut(L_w/K_v) → Aut(L/K) recovers the inclusion of the decomposition subgroup into Aut(L/K).

theorem NumberField.InfinitePlace.decompositionHom_injective {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] (v : InfinitePlace K) (w : InfinitePlace L) [w.LiesOver v] : Function.Injective ⇑(v.decompositionHom w)

The decomposition group of w acts faithfully on L_w.

theorem NumberField.InfinitePlace.apply_eq_self_of_algebraMap_mem_range {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] {v : InfinitePlace K} {w : InfinitePlace L} [w.LiesOver v] (τ : ↥(MulAction.stabilizer Gal(L/K) w)) {x : L} (hx : (algebraMap L w.Completion) x ∈ (algebraMap v.Completion w.Completion).range) : ↑τ x = x

An element of the decomposition group of w fixes every x ∈ L whose image in L_w comes from K_v: its action on L_w is K_v-linear and extends its action on L.

theorem NumberField.InfinitePlace.stabilizer_eq_bot_of_adjoin_eq_top {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] {v : InfinitePlace K} {w : InfinitePlace L} [w.LiesOver v] {s : Set L} (hs : IntermediateField.adjoin K s = ⊤) (h : ∀ x ∈ s, (algebraMap L w.Completion) x ∈ (algebraMap v.Completion w.Completion).range) : MulAction.stabilizer Gal(L/K) w = ⊥

The decomposition group is trivial when L is generated by elements of K_v. If L is generated over K by elements whose images in L_w come from K_v, then the decomposition group of w is trivial.

theorem NumberField.InfinitePlace.isGalois_completion {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] (v : InfinitePlace K) (w : InfinitePlace L) [w.LiesOver v] : IsGalois v.Completion w.Completion

A completion at an infinite place is Galois. The local extension L_w/K_v at an infinite place w of L is a Galois extension.

The decomposition group is the local Galois group

theorem NumberField.InfinitePlace.card_stabilizer_eq_finrank_completion {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] (v : InfinitePlace K) (w : InfinitePlace L) [w.LiesOver v] [IsGalois K L] : Nat.card ↥(MulAction.stabilizer Gal(L/K) w) = Module.finrank v.Completion w.Completion

The decomposition group of w has order the local degree. For L/K Galois the decomposition group of w has one element when w is unramified over K and two when it is ramified, and that is the degree of L_w over K_v.

theorem NumberField.InfinitePlace.finrank_completion_eq_one_of_adjoin_eq_top {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] (v : InfinitePlace K) (w : InfinitePlace L) [w.LiesOver v] [IsGalois K L] {s : Set L} (hs : IntermediateField.adjoin K s = ⊤) (h : ∀ x ∈ s, (algebraMap L w.Completion) x ∈ (algebraMap v.Completion w.Completion).range) : Module.finrank v.Completion w.Completion = 1

Local degree one. If the Galois extension L/K is generated by elements whose images in L_w come from K_v, then L_w = K_v: the local degree [L_w : K_v] is one.

theorem NumberField.InfinitePlace.finrank_completion_eq_ite {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] (v : InfinitePlace K) (w : InfinitePlace L) [w.LiesOver v] [IsGalois K L] [Decidable (IsUnramifiedIn L v)] : Module.finrank v.Completion w.Completion = if IsUnramifiedIn L v then 1 else 2

The local degree at an infinite place. For L/K Galois, [L_w : K_v] is 1 when v is unramified in L and 2 otherwise.

theorem NumberField.InfinitePlace.decompositionHom_surjective {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] (v : InfinitePlace K) (w : InfinitePlace L) [w.LiesOver v] [IsGalois K L] : Function.Surjective ⇑(v.decompositionHom w)

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.

noncomputable def NumberField.InfinitePlace.decompositionEquiv {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] (v : InfinitePlace K) (w : InfinitePlace L) [w.LiesOver v] [IsGalois K L] : ↥(MulAction.stabilizer Gal(L/K) w) ≃* Gal(w.Completion/v.Completion)

The decomposition group of w is the Galois group of L_w/K_v.

@[simp]

theorem NumberField.InfinitePlace.coe_decompositionEquiv {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] (v : InfinitePlace K) (w : InfinitePlace L) [w.LiesOver v] [IsGalois K L] : ⇑(v.decompositionEquiv w) = ⇑(v.decompositionHom w)