A place of full local degree in a prime-degree Galois extension

Let E/F be a Galois extension of number fields of prime degree. Some finite place w of E has nontrivial decomposition group: otherwise E/F would split completely at every finite place, and the first fundamental inequality would force E = F. Since Gal(E/F) has prime order, that nontrivial decomposition group is the whole Galois group. The identification of a decomposition group with the Galois group of the corresponding completion then shows that, for F an extension of a number field K and E embedded in Kˢ, every element of Gal(E/F) is the action on E of the image of an element of the absolute Galois group of some completion K_v.

Read on the absolute Galois group G_K, this applies to the finite normal layers V ◁ U of prime degree: with F and E the fixed fields of U and V, it produces an embedding of separable closures τ : Kˢ → K_vˢ for which the decomposition map φ_τ⁻¹(U) → U ⧸ V is onto. When U is the whole of G_K this is the quotient G_{K_v} → G_K ⧸ V. This is the local-degree input used to construct prescribed idele-layer invariants in prime-degree layers.

Main results

• TauCeti.ClassFieldTheory.exists_stabilizer_eq_top_of_finrank_prime: a prime-degree Galois extension of number fields has a finite place whose decomposition group is the whole Galois group.
• AlgHom.exists_absoluteGaloisGroupMap_apply_eq_of_finrank_prime: for a prime-degree Galois extension E/F of extensions of K and an embedding ι : E → Kˢ, some local absolute Galois group G_{K_v} realizes every element of Gal(E/F) on ι(E).
• IntermediateField.exists_surjective_restrictNormalHom_absoluteGaloisGroupMap_of_finrank_prime: a prime-degree finite Galois subextension of Kˢ/K has a finite place whose local absolute Galois group restricts onto its Galois group.
• OpenNormalSubgroup.exists_surjective_quotient_absoluteGaloisGroupMap_of_degree_prime: the corresponding statement for the quotient attached to a prime-degree open normal layer.
• TauCeti.ClassFieldTheory.NormalLayer.exists_surjective_absoluteGaloisGroupMap_of_degree_prime: for every finite normal layer V ◁ U of G_K of prime degree, some decomposition map φ_τ⁻¹(U) → U ⧸ V is onto.

References

• J. S. Milne, Class Field Theory, v4.03, Chapter VII, Propositions 4.6 and 4.7.
• J. Neukirch, Algebraic Number Theory, Chapter II, §9.

theorem TauCeti.ClassFieldTheory.exists_stabilizer_eq_top_of_finrank_prime {K : Type} [Field K] [NumberField K] {L : Type} [Field L] [NumberField L] [Algebra K L] [IsGalois K L] (hL : Nat.Prime (Module.finrank K L)) : ∃ (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) (w : { w : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers L) // w.asIdeal.LiesOver v.asIdeal }), MulAction.stabilizer Gal(L/K) (↑w).asIdeal = ⊤

A prime-degree Galois extension has a prime with full decomposition group. If L/K is a Galois extension of number fields of prime degree, then some finite place w of L has decomposition group all of Gal(L/K). Otherwise every decomposition group would be trivial, as Gal(L/K) has prime order, and finrank_eq_one_of_stabilizer_eq_bot would force L = K.

theorem AlgHom.exists_absoluteGaloisGroupMap_apply_eq_of_finrank_prime {K : Type} [Field K] [NumberField K] {F E : Type} [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) (hE : Nat.Prime (Module.finrank F E)) : ∃ (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) (τ : SeparableClosure K →ₐ[K] SeparableClosure (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)), ∀ (σ : Gal(E/F)), ∃ (g : TauCeti.AbsoluteGaloisGroup (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)), ∀ (x : E), ((TauCeti.absoluteGaloisGroupMap τ) g) (ι x) = ι (σ x)

A prime-degree Galois extension is realized by a local absolute Galois group. Let F be a number field over K, E/F a Galois extension of number fields of prime degree, and ι : E →ₐ[K] Kˢ an embedding into the separable closure of K. Then for some finite place v of K and some embedding τ : Kˢ → K_vˢ, every σ ∈ Gal(E/F) acts on ι(E) as the image under absoluteGaloisGroupMap τ of some element of G_{K_v}.

theorem IntermediateField.exists_surjective_restrictNormalHom_absoluteGaloisGroupMap_of_finrank_prime {K : Type} [Field K] [NumberField K] (L : IntermediateField K (SeparableClosure K)) [FiniteDimensional K ↥L] [IsGalois K ↥L] (hL : Nat.Prime (Module.finrank K ↥L)) : ∃ (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) (τ : SeparableClosure K →ₐ[K] SeparableClosure (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)), Function.Surjective fun (g : TauCeti.AbsoluteGaloisGroup (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)) => (AlgEquiv.restrictNormalHom ↥L) ((TauCeti.absoluteGaloisGroupMap τ) g)

A prime-degree Galois extension has a place of full local degree. If L/K is a finite Galois subextension of the separable closure and [L : K] is prime, then at some finite place v the map from G_{K_v} to Gal(L/K), obtained by an embedding Kˢ → K_vˢ and restriction to L, is surjective.

theorem OpenNormalSubgroup.exists_surjective_quotient_absoluteGaloisGroupMap_of_degree_prime {K : Type} [Field K] [NumberField K] (V : OpenNormalSubgroup (TauCeti.AbsoluteGaloisGroup K)) (hV : Nat.Prime (TauCeti.ClassFieldTheory.NormalLayer.ofOpenNormal V).degree) : ∃ (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) (τ : SeparableClosure K →ₐ[K] SeparableClosure (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)), Function.Surjective fun (g : TauCeti.AbsoluteGaloisGroup (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)) => ↑((TauCeti.absoluteGaloisGroupMap τ) g)

A prime-degree layer has a surjective decomposition map at some finite place. Let V be an open normal subgroup of G_K whose layer has prime degree. There are a finite place v and an embedding τ : Kˢ → K_vˢ for which the induced map G_{K_v} → G_K / V is onto.

theorem TauCeti.ClassFieldTheory.NormalLayer.exists_surjective_absoluteGaloisGroupMap_of_degree_prime {K : Type} [Field K] [NumberField K] (L : NormalLayer (AbsoluteGaloisGroup K)) (hL : Nat.Prime L.degree) : ∃ (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) (τ : SeparableClosure K →ₐ[K] SeparableClosure (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)), Function.Surjective fun (g : ↥(Subgroup.comap ↑(absoluteGaloisGroupMap τ) ↑L.ground)) => ↑(((absoluteGaloisGroupMap τ).subgroupComap ↑L.ground) g)

A prime-degree layer has a surjective decomposition map at some finite place. Let V ◁ U be a finite normal layer of G_K of prime degree. There are a finite place v of K and an embedding τ : Kˢ → K_vˢ for which the decomposition map φ_τ⁻¹(U) → U ⧸ V, induced by absoluteGaloisGroupMap τ : G_{K_v} → G_K, is onto.