Jumps of the ramification filtrations

An upper jump is an index at which the upper ramification group is strictly larger than at every later index, including the possible jump at -1 from the full Galois group to inertia. The Herbrand order isomorphism carries the lower jumps exactly to the upper jumps. The lower-jump definition and its integer criterion are in RamificationGroup.

In prime degree, an upper break at a natural number t implies that the lower ramification group G_t is the full Galois group and that G_{t+1} is trivial. The natural inverse Herbrand function fixes every depth up to t.

These statements identify the breaks used by the norm filtration and Hasse–Arf theory.

References

• J.-P. Serre, Corps Locaux, Chapter IV, §3.

def TauCeti.LocalFieldsRamification.UpperJump (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) : Prop

An upper break: the upper ramification group at u is strictly larger than the group at every later index.

Equations

• One or more equations did not get rendered due to their size.

theorem TauCeti.LocalFieldsRamification.upperJump_iff (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) : UpperJump K L u ↔ ∀ (v : ↑RamificationIndexDomain), u < v → upperRamificationGroup K L v < upperRamificationGroup K L u

An upper break is a strict drop of the upper ramification group at every later index.

@[simp]

theorem TauCeti.LocalFieldsRamification.upperJump_herbrand_iff (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) : UpperJump K L (herbrand K L u) ↔ LowerJump K L u

The Herbrand function takes lower breaks precisely to upper breaks.

@[simp]

theorem TauCeti.LocalFieldsRamification.lowerJump_inverseHerbrand_iff (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) : LowerJump K L (inverseHerbrand K L u) ↔ UpperJump K L u

The inverse Herbrand function takes upper breaks precisely to lower breaks.

theorem TauCeti.LocalFieldsRamification.lowerRamificationGroup_natCast_eq_top_of_upperJump (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] (hℓ : Nat.Prime (Module.finrank K L)) {t : ℕ} (ht : UpperJump K L ⟨↑t, ⋯⟩) : lowerRamificationGroup K L ↑t = ⊤

In prime degree, an upper break at a natural number t has G_t = Gal(L/K): the group G^t = G_{ψ(t)} strictly contains every later upper group, so it is nontrivial, hence the whole Galois group, and t ≤ ψ(t).

theorem TauCeti.LocalFieldsRamification.psiNat_eq_self_of_le_break (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] (hℓ : Nat.Prime (Module.finrank K L)) {v t : ℕ} (hvt : v ≤ t) (ht : UpperJump K L ⟨↑t, ⋯⟩) : psiNat K L v = v

In prime degree, the natural inverse Herbrand function fixes every depth at or below a natural upper break.

theorem TauCeti.LocalFieldsRamification.lowerRamificationGroup_natCast_add_one_eq_bot_of_upperJump (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] (hℓ : Nat.Prime (Module.finrank K L)) {t : ℕ} (ht : UpperJump K L ⟨↑t, ⋯⟩) : lowerRamificationGroup K L (↑t + 1) = ⊥

In prime degree, an upper break at a natural number t has G_{t+1} = 1. Together with G_t = Gal(L/K) (lowerRamificationGroup_natCast_eq_top_of_upperJump), this says that the lower filtration drops from the whole Galois group to the trivial group exactly between t and t + 1.