Module

HasseArf.lean

Nyll.ClassFieldTheory.Theorems.HasseArf.HasseArf

1 declaration indexed from sourceView source ↗

Module documentation

Hasse--Arf theorem

Let L/K be a finite abelian extension of nonarchimedean local fields, with the valuation of L extending that of K. If n is a jump in the lower ramification filtration, the corresponding upper index is the Herbrand value φ(n). Hasse--Arf says that this upper index is an integer.

This is the standard equivalent integral-lower-jump formulation of the theorem. It avoids postulating an opaque predicate for upper jumps: the lower groups and the Herbrand value are defined explicitly in ClassFieldTheory.Definitions.HasseArf modules from Mathlib's valuation-subring data.

Imports6

Nyll.ClassFieldTheory.Definitions.HasseArf.HerbrandFunctionAtLowerIndex
Nyll.ClassFieldTheory.Definitions.HasseArf.IsLowerRamificationJump
Nyll.ClassFieldTheory.HasseArf
Mathlib.FieldTheory.Galois.Abelian
Mathlib.NumberTheory.LocalField.Basic
Mathlib.RingTheory.Valuation.Extension

Imported by2

theorem

hasseArf

L40 ↗

ClassFieldTheory.hasseArf

Documentation

Hasse--Arf. For a finite abelian extension of nonarchimedean local fields, the Herbrand image of every lower ramification jump is integral.

Here the lower filtration is attached to the canonical valuation subring of L. The Valuation.HasExtension assumption records compatibility of the canonical valuations on K and L; it is data about the extension, not a ramification or integrality conclusion.

Source context 2 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace ClassFieldTheory

Lean source · statement

theorem hasseArf
    (K L : Type*) [Field K] [Field L] [Algebra K L]
    [FiniteDimensional K L] [IsAbelianGalois K L]
    [ValuativeRel K] [TopologicalSpace K]
    [IsNonarchimedeanLocalField K]
    [ValuativeRel L] [TopologicalSpace L]
    [IsNonarchimedeanLocalField L]
    [Valuation.HasExtension (ValuativeRel.valuation K) (ValuativeRel.valuation L)]
    {n : ℕ}
    (hn : IsLowerRamificationJump K
      (ValuativeRel.valuation L).valuationSubring n) :
    ∃ z : ℤ,
      herbrandFunctionAtLowerIndex K
        (ValuativeRel.valuation L).valuationSubring n = (z : ℚ)

Module documentation

Hasse--Arf theorem

Declarations

hasseArf