The Hasse--Arf theorem #
The Hasse--Arf theorem says that every upper ramification break of a finite abelian Galois extension of nonarchimedean local fields is an integer.
The proof separates the elementary nonpositive breaks from the positive wild breaks. An upper break of an abelian extension is detected in a cyclic subextension. A positive break of that cyclic extension remains a break after quotienting out the prime-to-residue-characteristic part of its Galois group. The resulting cyclic extension has prime-power degree, where integrality follows from the norm-conductor form of Hasse--Arf.
Main result #
TauCeti.LocalFieldsRamification.hasseArf: every upper ramification break of a finite abelian extension is integral.
References #
- J.-P. Serre, Corps Locaux, Chapter V, §7.
theorem
TauCeti.LocalFieldsRamification.hasseArf
(K : Type u)
(L : Type v)
[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]
{w : ↑RamificationIndexDomain}
(hw : UpperJump K L w)
:
Hasse--Arf. Every upper ramification break of a finite abelian Galois extension of nonarchimedean local fields is an integer.