The prime-degree case of Hasse--Arf

For a finite Galois extension of prime degree, every upper ramification break is integral. More precisely, an upper break is either -1, accounting for the jump from the full Galois group to inertia in the unramified case, or is a natural number.

This is the base case for the prime-order induction in the Hasse--Arf theorem. The proof uses the integrality of lower breaks and the fact that a subgroup of a group of prime order is either trivial or the whole group. At a nonnegative lower break t, the lower filtration is therefore constant through t, so the inverse Herbrand function fixes t.

Main results

• TauCeti.LocalFieldsRamification.UpperJump.eq_neg_one_or_exists_eq_natCast_of_finrank_prime: a prime-degree upper break is -1 or a natural number.
• TauCeti.LocalFieldsRamification.UpperJump.exists_eq_intCast_of_finrank_prime: the prime-degree case of the Hasse--Arf integrality statement.
• TauCeti.LocalFieldsRamification.UpperJump.eq_of_finrank_prime: a prime-degree extension has at most one upper break.

References

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

theorem TauCeti.LocalFieldsRamification.UpperJump.eq_of_finrank_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] [IsGalois K L] {u v : ↑RamificationIndexDomain} (hu : UpperJump K L u) (hv : UpperJump K L v) (hdegree : Nat.Prime (Module.finrank K L)) : u = v

A finite Galois extension of prime degree has at most one upper ramification break.

theorem TauCeti.LocalFieldsRamification.UpperJump.eq_neg_one_or_exists_eq_natCast_of_finrank_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] [IsGalois K L] {u : ↑RamificationIndexDomain} (hu : UpperJump K L u) (hdegree : Nat.Prime (Module.finrank K L)) : ↑u = -1 ∨ ∃ (t : ℕ), ↑u = ↑t

In a prime-degree Galois extension, an upper ramification break is either the possible unramified break at -1 or a nonnegative integer.

The nonnegative alternative is stated with a natural number so that the norm-conductor API can consume it directly.

theorem TauCeti.LocalFieldsRamification.UpperJump.exists_eq_intCast_of_finrank_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] [IsGalois K L] {u : ↑RamificationIndexDomain} (hu : UpperJump K L u) (hdegree : Nat.Prime (Module.finrank K L)) : ∃ (z : ℤ), ↑u = ↑z

Hasse--Arf in prime degree. Every upper ramification break of a finite Galois extension of prime degree is an integer.