Prime-degree towers in abelian Galois extensions

A finite abelian Galois extension admits a finite tower of intermediate fields from the base to the whole extension, with every successive extension of prime degree. Every field in the tower is Galois over the base, so the corresponding fixing subgroups form a normal series with prime-order quotients. Such towers supply the induction used in the Hasse--Arf theorem.

The tower uses Mathlib's RelSeries of covering relations on intermediate fields. The algebra of each adjacent pair is the algebra induced by its inclusion.

References

• J.-P. Serre, Corps Locaux, Chapter V, §7.

theorem IntermediateField.prime_finrank_of_covBy {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] [Module.Finite K L] [IsAbelianGalois K L] (E F : IntermediateField K L) (h : E ⋖ F) [aEF : Algebra ↥E ↥F] [IsScalarTower K ↥E ↥F] [IsScalarTower (↥E) (↥F) L] : Nat.Prime (Module.finrank ↥E ↥F)

A covering pair of intermediate fields in a finite abelian Galois extension has prime relative degree. The algebra and tower instances retain the caller's chosen inclusion map.

theorem TauCeti.exists_prime_finrank_intermediateField_series (K : Type u_1) (L : Type u_2) [Field K] [Field L] [Algebra K L] [Module.Finite K L] [IsAbelianGalois K L] : ∃ (s : RelSeries {(E, F) : IntermediateField K L × IntermediateField K L | E ⋖ F}), s.head = ⊥ ∧ s.last = ⊤ ∧ ∀ (i : Fin s.length), have this := (IntermediateField.inclusion ⋯).toAlgebra; Nat.Prime (Module.finrank ↥(s.toFun i.castSucc) ↥(s.toFun i.succ)) ∧ IsAbelianGalois ↥(s.toFun i.castSucc) ↥(s.toFun i.succ)

A finite abelian Galois extension admits a bottom-to-top series of intermediate fields with prime relative degree at every step. The successive algebras are induced by inclusion. Every node is abelian Galois over the base, and every step is abelian Galois. The trivial extension gives a series of length zero.