The Frobenius elements generate the Galois group of a solvable extension

Let L/K be a Galois extension of number fields and S a finite set of finite places of K. If Gal(L/K) is solvable, the arithmetic Frobenius elements at the places of L above the finite places of K outside S generate Gal(L/K) (closure_isArithFrobAt_eq_top). If moreover almost every finite place of K has a place of L above it with trivial decomposition group, then L = K (finrank_eq_one_of_stabilizer_eq_bot): a nontrivial solvable extension has infinitely many places that do not split completely.

Both statements are proved without the Chebotarev density theorem. If either failed, the fixed field of a normal subgroup of prime index containing the relevant decomposition groups would be a cyclic extension E/K of prime degree from which every idele class is a norm (exists_finrank_prime_ideleClassNormMap_surjective_of_closure_isArithFrobAt_ne_top and exists_finrank_prime_ideleClassNormMap_surjective_of_stabilizer_eq_bot, in the namespace TauCeti.GlobalNumberFields). The first fundamental inequality [C_K : N_{E/K}(C_E)] ≥ [E : K] excludes such a field (finrank_eq_one_of_surjective_ideleClassNormMap).

The Kummer-theoretic proof of the second fundamental inequality uses the generation statement for an extension M/L inside a tower K ⊆ L ⊆ M, with the excluded places given as places of the ground field K: the Frobenius elements of M/L at the places of M above the finite places of K outside S generate Gal(M/L) (closure_isArithFrobAt_eq_top_tower). A Frobenius basis of Gal(M/L) is then extracted from them (NumberField.exists_finset_closure_artinElementAway_eq_range_restrictScalarsHom).

Main results

• TauCeti.ClassFieldTheory.closure_isArithFrobAt_eq_top: the Frobenius elements at the places outside a finite set generate the Galois group of a solvable extension of number fields.
• TauCeti.ClassFieldTheory.closure_isArithFrobAt_eq_top_tower: the same statement for M/L in a tower K ⊆ L ⊆ M, with the excluded set given by places of K.
• TauCeti.ClassFieldTheory.finrank_eq_one_of_stabilizer_eq_bot: a solvable extension in which almost every place has a place above it with trivial decomposition group is trivial.

References

• J. S. Milne, Class Field Theory, v4.03, Chapter VII, Proposition 4.6 and Proposition 4.7.

theorem TauCeti.ClassFieldTheory.closure_isArithFrobAt_eq_top {K L : Type} [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] [IsGalois K L] (S : Finset (IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K))) [Group.IsSolvable (Gal(L/K) ⧸ Subgroup.normalClosure {σ : Gal(L/K) | ∃ v ∉ S, ∃ (w : { w : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers L) // w.asIdeal.LiesOver v.asIdeal }), IsArithFrobAt (NumberField.RingOfIntegers K) σ (↑w).asIdeal})] : Subgroup.closure {σ : Gal(L/K) | ∃ v ∉ S, ∃ (w : { w : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers L) // w.asIdeal.LiesOver v.asIdeal }), IsArithFrobAt (NumberField.RingOfIntegers K) σ (↑w).asIdeal} = ⊤

The Frobenius elements generate the Galois group (Milne VII, Proposition 4.7). Let L/K be a Galois extension of number fields and S a finite set of finite places of K. If the quotient of Gal(L/K) by the normal closure of the arithmetic Frobenius elements at the places of L above the finite places of K outside S is solvable, for instance if L/K is solvable, then these Frobenius elements generate Gal(L/K).

theorem TauCeti.ClassFieldTheory.finrank_eq_one_of_stabilizer_eq_bot {K L : Type} [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] [IsGalois K L] [Group.IsSolvable Gal(L/K)] (S : Finset (IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K))) (hS : ∀ v ∉ S, ∃ (w : { w : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers L) // w.asIdeal.LiesOver v.asIdeal }), MulAction.stabilizer Gal(L/K) (↑w).asIdeal = ⊥) : Module.finrank K L = 1

A solvable extension that splits almost everywhere is trivial (Milne VII, Proposition 4.6). Let L/K be a Galois extension of number fields with solvable Galois group. If every finite place v of K outside a finite set S has a place w of L above it with trivial decomposition group, then [L : K] = 1, that is, L = K.

theorem TauCeti.ClassFieldTheory.closure_isArithFrobAt_eq_top_tower {K L : Type} [Field K] [Field L] [NumberField L] [Algebra K L] {M : Type} [Field M] [NumberField M] [Algebra K M] [Algebra L M] [IsScalarTower K L M] [IsGalois L M] [Group.IsSolvable Gal(M/L)] (S : Finset (IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K))) : Subgroup.closure {τ : Gal(M/L) | ∃ v ∉ S, ∃ (Q : { Q : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers M) // Q.asIdeal.LiesOver v.asIdeal }), IsArithFrobAt (NumberField.RingOfIntegers L) τ (↑Q).asIdeal} = ⊤

The Frobenius elements generate the Galois group of the top of a tower. Let K ⊆ L ⊆ M be a tower of fields with L and M number fields and M/L Galois and solvable, and let S be a finite set of finite places of K. Then Gal(M/L) is generated by its arithmetic Frobenius elements at the places of M above the finite places of K outside S.

This is closure_isArithFrobAt_eq_top for M/L, applied to the places of L above S.