Detecting abelian ramification breaks in cyclic subextensions

Every upper break of a finite abelian extension of local fields is an upper break of a cyclic subextension. In fact, the subextension can be chosen so that every upper ramification group strictly after the break is trivial. Thus integrality of all abelian upper breaks reduces to integrality for cyclic extensions.

For an elementary abelian Galois group, the detecting cyclic subextension has prime degree. The prime-degree case of Hasse--Arf therefore proves integrality of every upper break of the original extension, regardless of its degree.

The break detection uses the integer indexing of lower breaks, cyclic quotients separating subgroups of a finite abelian group, and Herbrand's upper-numbering quotient theorem.

Main results

• TauCeti.LocalFieldsRamification.upperJump_iff_exists_isCyclic_intermediateField: an upper break is detected in a cyclic intermediate field, with no later nontrivial ramification.
• TauCeti.LocalFieldsRamification.UpperJump.exists_eq_intCast_of_exponent_prime: Hasse--Arf for elementary abelian extensions.

References

• J.-P. Serre, Local Fields, Chapter IV, §3, and Chapter V, §7.

theorem TauCeti.LocalFieldsRamification.upperJump_iff_exists_isCyclic_intermediateField (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] [IsAbelianGalois K L] (u : ↑RamificationIndexDomain) : UpperJump K L u ↔ ∃ (F : IntermediateField K L), IsCyclic Gal(↥F/K) ∧ UpperJump K (↥F) u ∧ ∀ (v : ↑RamificationIndexDomain), u < v → upperRamificationGroup K (↥F) v = ⊥

An upper break of a finite abelian extension is detected in a cyclic subextension. The subextension can be chosen with trivial upper ramification groups at every later index, so the specified break is its last break. Its local-field structures are the canonical ones induced from the base field.

theorem TauCeti.LocalFieldsRamification.UpperJump.exists_eq_intCast_of_exponent_prime {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] [IsAbelianGalois K L] {u : ↑RamificationIndexDomain} (hu : UpperJump K L u) (hp : Nat.Prime (Monoid.exponent Gal(L/K))) : ∃ (z : ℤ), ↑u = ↑z

Hasse--Arf for elementary abelian extensions. If the exponent of the abelian Galois group is prime, every upper ramification break is integral. This includes groups of arbitrary prime-power order, not just prime-degree extensions.