Restricting the abelianized absolute Galois group of an extension to a finite normal layer

Let F/K be a field extension, not necessarily algebraic, and L/K a finite normal extension. Every K-embedding j : L →ₐ[K] Fᵃˡᵍ into an algebraic closure of F has a G_F-stable image, because L/K is normal, so an automorphism τ ∈ G_F = Gal(Fᵃˡᵍ/F) induces the automorphism σ of L/K with j ∘ σ = τ ∘ j (AlgHom.restrictNormalHom). The map τ ↦ σ depends on j, but two embeddings differ by an automorphism of L/K and the two maps by conjugation by it (AlgHom.restrictNormalHom_comp), which Gal(L/K)^ab does not see. The kernel is open, since τ fixes j(L) once it fixes the images of a K-basis of L; so the map factors through the topological abelianization G_F^ab, and gives a homomorphism

decompositionRestrict K F L : G_F^ab →* Gal(L/K)^ab,   [τ] ↦ [σ]   whenever j ∘ σ = τ ∘ j,

for every j (decompositionRestrict_mk). When K is a number field and F = K_v a completion, a K-embedding j of L into K_vᵃˡᵍ is a place of L above v, and the image of G_{K_v} in Gal(L/K) is the decomposition group of that place. The absolute local Artin map of K_v takes values in G_{K_v}^ab, so decompositionRestrict is the map that reads a local Artin symbol in Gal(L/K)^ab, as the local–global compatibility of a global reciprocity map requires; the same construction serves the finite and the infinite places.

The global theory works with the separable closure Kˢ, through the maps TauCeti.absoluteGaloisGroupMap τ : G_F → G_K attached to embeddings τ : Kˢ →ₐ[K] Fˢ. Read along any such τ and any embedding iota of L into Kˢ, decompositionRestrict is restriction to L (decompositionRestrict_mk_eq_restrictNormalHom_absoluteGaloisGroupMap).

Main definitions

• TauCeti.decompositionRestrict K F L: the homomorphism G_F^ab →* Gal(L/K)^ab.

Main results

• AlgHom.isOpen_ker_restrictNormalHom_comp_restrictScalarsHom: restriction of Gal(Ω/F) to Gal(L/K) along an embedding of L into an algebraic extension Ω of F has open kernel.
• TauCeti.decompositionRestrict_mk: the class of τ goes to the class of the automorphism σ of L with j ∘ σ = τ ∘ j, for every K-embedding j : L →ₐ[K] Fᵃˡᵍ.
• TauCeti.decompositionRestrict_mk_eq_restrictNormalHom: the value on the class of τ, as the class of the restriction of τ along a chosen j.
• TauCeti.decompositionRestrict_mk_eq_restrictNormalHom_absoluteGaloisGroupMap: the comparison with restriction along the separable closures.
• TauCeti.decompositionRestrict_comp: compatibility with restriction to a normal subextension.

References

• J. Neukirch, Algebraic Number Theory, Chapter II, §9 (decomposition groups and completions) and Chapter VI, §5 (local–global compatibility of the reciprocity map).
• J. S. Milne, Class Field Theory, Chapter V, §5, and Chapter VII, §5.

Openness of the kernel of restriction

theorem AlgHom.isOpen_ker_restrictNormalHom_comp_restrictScalarsHom {K : Type u_1} {F : Type u_2} {L : Type u_3} {Ω : Type u_4} [Field K] [Field F] [Field L] [Field Ω] [Algebra K F] [Algebra K L] [Algebra F Ω] [Algebra K Ω] [IsScalarTower K F Ω] [Algebra.IsAlgebraic F Ω] [FiniteDimensional K L] [Normal K L] (j : L →ₐ[K] Ω) : IsOpen ↑(j.restrictNormalHom.comp (AlgEquiv.restrictScalarsHom K)).ker

Let Ω/F be algebraic, F/K an extension and L/K finite normal. Restriction of Gal(Ω/F) to Gal(L/K) along a K-embedding j : L →ₐ[K] Ω has open kernel: an automorphism of Ω/F fixing the images under j of a K-basis of L fixes j(L), and those images generate a finite extension of F.

The restriction map

noncomputable def TauCeti.decompositionRestrict (K : Type u_1) (F : Type u_2) (L : Type u_3) [Field K] [Field F] [Algebra K F] [Field L] [Algebra K L] [Normal K L] [FiniteDimensional K L] : Field.absoluteGaloisGroupAbelianization F →* Abelianization Gal(L/K)

Restriction of G_F^ab to a finite normal layer L/K, for an extension F/K: the class of τ ∈ G_F goes to the class of the automorphism σ of L/K with j ∘ σ = τ ∘ j, for any K-embedding j : L →ₐ[K] Fᵃˡᵍ (decompositionRestrict_mk). The value does not depend on j. For a completion F = K_v of a number field the image of G_F in Gal(L/K) is the decomposition group of the place of L above v given by j.

theorem TauCeti.decompositionRestrict_mk {K : Type u_1} {F : Type u_2} {L : Type u_3} [Field K] [Field F] [Algebra K F] [Field L] [Algebra K L] [Normal K L] [FiniteDimensional K L] (j : L →ₐ[K] AlgebraicClosure F) (τ : Field.absoluteGaloisGroup F) (σ : Gal(L/K)) (hσ : ∀ (y : L), j (σ y) = τ.toRingEquiv (j y)) : (decompositionRestrict K F L) ↑τ = Abelianization.of σ

The characterizing equation of decompositionRestrict. For every K-embedding j : L →ₐ[K] Fᵃˡᵍ, the class of τ ∈ G_F goes to the class of the automorphism σ of L/K with j ∘ σ = τ ∘ j.

theorem TauCeti.decompositionRestrict_mk_eq_restrictNormalHom {K : Type u_1} {F : Type u_2} {L : Type u_3} [Field K] [Field F] [Algebra K F] [Field L] [Algebra K L] [Normal K L] [FiniteDimensional K L] (j : L →ₐ[K] AlgebraicClosure F) (τ : Field.absoluteGaloisGroup F) : (decompositionRestrict K F L) ↑τ = Abelianization.of (j.restrictNormalHom ((AlgEquiv.restrictScalarsHom K) τ))

decompositionRestrict on the class of τ, computed along any K-embedding j : L →ₐ[K] Fᵃˡᵍ as the class of the restriction of τ to j(L).

theorem TauCeti.decompositionRestrict_comp {K : Type u_1} {F : Type u_2} {L : Type u_3} [Field K] [Field F] [Algebra K F] [Field L] [Algebra K L] [Normal K L] [FiniteDimensional K L] {M : Type u_4} [Field M] [Algebra K M] [FiniteDimensional K M] [Normal K M] (f : M →ₐ[K] L) : (Abelianization.map f.restrictNormalHom).comp (decompositionRestrict K F L) = decompositionRestrict K F M

Compatibility with restriction to a normal subextension. For a K-embedding f : M →ₐ[K] L of a finite normal extension M/K, restricting G_F^ab to Gal(L/K)^ab and then to Gal(M/K)^ab along f is restricting G_F^ab to Gal(M/K)^ab.

Comparison with restriction along the separable closures

theorem TauCeti.decompositionRestrict_mk_eq_restrictNormalHom_absoluteGaloisGroupMap {K : Type u_1} {F : Type u_2} {L : Type u_3} [Field K] [Field F] [Algebra K F] [Field L] [Algebra K L] [Normal K L] [FiniteDimensional K L] (iota : L →ₐ[K] SeparableClosure K) (τ : SeparableClosure K →ₐ[K] SeparableClosure F) (σ : Field.absoluteGaloisGroup F) : (decompositionRestrict K F L) ↑σ = Abelianization.of (iota.restrictNormalHom ((absoluteGaloisGroupMap τ) ((absoluteGaloisGroupRestrictEquiv F) σ)))

decompositionRestrict along the separable closures. Let iota : L →ₐ[K] Kˢ embed L in the separable closure of K and τ : Kˢ →ₐ[K] Fˢ be an embedding of separable closures. Then the class of σ ∈ G_F goes to the class of the restriction to L, along iota, of the image of σ under absoluteGaloisGroupMap τ : G_F → G_K.