Hasse--Arf for cyclic extensions of prime-power degree

Let L/K be a finite Galois extension of nonarchimedean local fields whose Galois group G is cyclic of order a power of a prime p. The Hasse--Arf theorem for L/K says that every upper ramification break of L/K is an integer. This file proves it by induction on the degree, comparing norms with the unit filtration.

Let H be the subgroup of order p of G, with fixed field F. The upper breaks of L/K are those of F/K, integral by induction, together with φ_{F/K}(t) for the break t of the prime-degree extension L/F. To see that φ_{F/K}(t) is an integer, suppose instead that ψℕ_{F/K}(n) < t < ψℕ_{F/K}(n + 1). For x ∈ U(F,t), the Herbrand-shifted inclusion puts N_{F/K}(x) in U(K, n + 1), and G^{n+1} = 1 makes N_{F/K} map U(F, ψℕ_{F/K}(n + 1)) onto U(K, n + 1). So x = w z with z ∈ U(F, t + 1) and N_{F/K}(w) = 1, and by Hilbert's Theorem 90 w = g y / y for a generator g of Gal(F/K). Since L/K is Galois, Gal(F/K) acts on the cokernel U(F,0) / N_{L/F}(U(L,0)), which has order p; being a p-group, it acts trivially. A uniformizer of F is a norm from the totally ramified extension L, so w is a norm from L. Hence every element of U(F,t) is a norm modulo U(F, t + 1), contradicting the fact that the graded norm of L/F at its break has cokernel of order p.

Main results

• TauCeti.LocalFieldsRamification.UpperJump.exists_psiNat_eq_of_isPGroup: the induction step: in a tower L/F/K with Gal(F/K) a cyclic ℓ-group, [L : F] = ℓ prime, and no lower ramification of F/K beyond the break t of L/F, the break t is a value of ψℕ_{F/K}.
• TauCeti.LocalFieldsRamification.UpperJump.exists_eq_intCast_of_isPGroup: Hasse--Arf for cyclic extensions of prime-power degree.

References

• J.-P. Serre, Corps Locaux, Chapter IV, §3, and Chapter V, §§3, 6 and 7.

theorem TauCeti.LocalFieldsRamification.UpperJump.exists_psiNat_eq_of_isPGroup {K : Type u_1} {F : Type u_2} {L : Type u_3} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] [Field F] [ValuativeRel F] [TopologicalSpace F] [IsNonarchimedeanLocalField F] [Field L] [ValuativeRel L] [TopologicalSpace L] [IsNonarchimedeanLocalField L] [Algebra K F] [ValuativeExtension K F] [Module.Finite K F] [IsGalois K F] [Algebra F L] [ValuativeExtension F L] [Module.Finite F L] [IsGalois F L] [Algebra K L] [ValuativeExtension K L] [Module.Finite K L] [IsGalois K L] [IsScalarTower K F L] [IsCyclic Gal(F/K)] {t : ℕ} (ht : UpperJump F L ⟨↑t, ⋯⟩) (hℓ : Nat.Prime (Module.finrank F L)) (hp : IsPGroup (Module.finrank F L) Gal(F/K)) (hbot : lowerRamificationGroup K F ↑(t + 1) = ⊥) : ∃ (n : ℕ), psiNat K F n = t

The induction step of Hasse--Arf. Let L/F/K be a tower of Galois extensions of nonarchimedean local fields in which L/F has prime degree ℓ with an upper break at the natural number t, and Gal(F/K) is a cyclic ℓ-group with trivial lower ramification group Gal(F/K)_{t+1}. Then t = ψℕ_{F/K}(n) for some natural number n; equivalently, the Herbrand function φ_{F/K} takes the break t to an integer.

theorem TauCeti.LocalFieldsRamification.UpperJump.exists_eq_intCast_of_isPGroup {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] [IsGalois K L] [IsCyclic Gal(L/K)] {p : ℕ} [Fact (Nat.Prime p)] (hp : IsPGroup p Gal(L/K)) {u : ↑RamificationIndexDomain} (hu : UpperJump K L u) : ∃ (z : ℤ), ↑u = ↑z

Hasse--Arf for cyclic extensions of prime-power degree. If the Galois group of a finite Galois extension L/K of nonarchimedean local fields is cyclic of p-power order, every upper ramification break of L/K is an integer.