Decomposition groups inside the image of a local absolute Galois group

Let K ⊆ F ⊆ E be number fields with E/F Galois, let ι : E →ₐ[K] Kˢ embed E in the separable closure Kˢ of K, and let w be a finite place of E above a place of F above the finite place v of K. An embedding of separable closures τ : Kˢ →ₐ[K] K_vˢ gives the map TauCeti.absoluteGaloisGroupMap τ : G_{K_v} → G_K. This file shows that for a suitable τ every element σ of the decomposition group of w in Gal(E/F) is read off along ι from the image of some g ∈ G_{K_v}: absoluteGaloisGroupMap τ g (ι x) = ι (σ x) for every x ∈ E (AlgHom.exists_absoluteGaloisGroupMap_apply_eq_of_mem_stabilizer). Such an image fixes ι(F) pointwise, so it lies in the subgroup of G_K cut out by F.

Let u be the place of F below w. The embedding τ is chosen so that its restriction to E factors through the completion E_w: embed F_u in K_vˢ over K_v, which makes K_vˢ a separable closure of F_u, embed E_w in it over F_u, and extend E → E_w → K_vˢ to Kˢ. An element σ of the decomposition group extends by continuity to an automorphism of E_w/F_u (IsDedekindDomain.HeightOneSpectrum.decompositionHom), which in turn is the restriction of an automorphism of K_vˢ over F_u, since K_vˢ/F_u is normal; that automorphism is in particular an element g of G_{K_v}, and absoluteGaloisGroupMap τ g acts as σ on ι(E).

For F = K this says that the decomposition group of w in Gal(E/K) lies in the image of G_{K_v} (AlgHom.exists_stabilizer_le_range_restrictNormalHom_comp_absoluteGaloisGroupMap). So a place whose decomposition group is the whole Galois group yields an embedding τ along which G_{K_v} maps onto it. This is how the existence of a place of full local degree, a statement about prime ideals, becomes a statement about the decomposition maps G_{K_v} → G_K used by Galois cohomology.

Main results

• AlgHom.exists_absoluteGaloisGroupMap_apply_eq_of_mem_stabilizer: for some embedding τ : Kˢ →ₐ[K] K_vˢ, every element of the decomposition group of w in Gal(E/F) agrees on ι(E) with the image of an element of G_{K_v}.
• AlgHom.exists_stabilizer_le_range_restrictNormalHom_comp_absoluteGaloisGroupMap: the case F = K, for some embedding τ : Kˢ →ₐ[K] K_vˢ, every element of the decomposition group of w is the restriction to E of the image of an element of G_{K_v}.

References

• J. Neukirch, Algebraic Number Theory, Chapter II, §9 (decomposition groups and completions).

theorem AlgHom.exists_absoluteGaloisGroupMap_apply_eq_of_mem_stabilizer {K : Type u_1} {F : Type u_2} {E : Type u_3} [Field K] [NumberField K] [Field F] [NumberField F] [Field E] [NumberField E] [Algebra K F] [Algebra K E] [Algebra F E] [IsScalarTower K F E] [IsGalois F E] (ι : E →ₐ[K] SeparableClosure K) {v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)} {u : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers F)} [hu : u.asIdeal.LiesOver v.asIdeal] (w : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers E)) [w.asIdeal.LiesOver u.asIdeal] : ∃ (τ : SeparableClosure K →ₐ[K] SeparableClosure (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)), ∀ σ ∈ MulAction.stabilizer Gal(E/F) w.asIdeal, ∃ (g : TauCeti.AbsoluteGaloisGroup (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)), ∀ (x : E), ((TauCeti.absoluteGaloisGroupMap τ) g) (ι x) = ι (σ x)

The decomposition group acts through the local absolute Galois group. Let K ⊆ F ⊆ E be number fields with E/F Galois, ι : E →ₐ[K] Kˢ an embedding into the separable closure of K, and w a finite place of E above a finite place u of F above the finite place v of K. For some embedding of separable closures τ : Kˢ →ₐ[K] K_vˢ, every element σ of the decomposition group of w in Gal(E/F) satisfies absoluteGaloisGroupMap τ g (ι x) = ι (σ x) for some g ∈ G_{K_v} and every x ∈ E.

theorem AlgHom.exists_stabilizer_le_range_restrictNormalHom_comp_absoluteGaloisGroupMap {K : Type u_1} {E : Type u_3} [Field K] [NumberField K] [Field E] [NumberField E] [Algebra K E] [IsGalois K E] (ι : E →ₐ[K] SeparableClosure K) {v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)} (w : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers E)) [w.asIdeal.LiesOver v.asIdeal] : ∃ (τ : SeparableClosure K →ₐ[K] SeparableClosure (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)), MulAction.stabilizer Gal(E/K) w.asIdeal ≤ (ι.restrictNormalHom.comp ↑(TauCeti.absoluteGaloisGroupMap τ)).range

The decomposition group lies in the image of the local absolute Galois group. Let E/K be a Galois extension of number fields, ι : E →ₐ[K] Kˢ an embedding into the separable closure of K, and w a finite place of E above the finite place v of K. For some embedding of separable closures τ : Kˢ →ₐ[K] K_vˢ, every element of the decomposition group of w is the restriction along ι of absoluteGaloisGroupMap τ g for some g ∈ G_{K_v}.