The Galois group of a finite extension of local fields is solvable

Let L/K be a finite extension of nonarchimedean local fields, with automorphism group G = L ≃ₐ[K] L and lower ramification filtration G_i. The three steps of the filtration 1 ⊴ G_1 ⊴ G_0 ⊴ G have the following quotients:

• G / G_0 embeds, through the action on the residue field, into the Galois group of the finite residue field extension, so it is cyclic;
• the tame quotient G_0 / G_1 embeds into 𝓀[L]ˣ through the tame character, so it is cyclic (TauCeti.isCyclic_ramificationGroupGraded_zero);
• the wild inertia group G_1 is a p-group for the residue characteristic p (TauCeti.isPGroup_ramificationGroup), hence nilpotent.

Consequently G is solvable. Solvability is what lets a statement about the cohomology of a finite local Galois group be proved by induction along a chain of normal subgroups with cyclic quotients, reducing it to the cyclic case.

Main results

• TauCeti.LocalFieldsRamification.isSolvable_algEquiv: G is solvable.

References

• J.-P. Serre, Corps Locaux, Chapter IV, §2.

instance TauCeti.LocalFieldsRamification.isSolvable_algEquiv (K : Type u_1) (L : Type u_2) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] [Field L] [ValuativeRel L] [TopologicalSpace L] [IsNonarchimedeanLocalField L] [Algebra K L] [ValuativeExtension K L] [Module.Finite K L] : Group.IsSolvable Gal(L/K)

The Galois group of a finite extension of nonarchimedean local fields is solvable: its ramification filtration 1 ⊴ G_1 ⊴ G_0 ⊴ G has a p-group at the bottom and cyclic quotients above it.