NYLL
Module

HerbrandFunctionAtLowerIndexNatOfJump.lean

Nyll.ClassFieldTheory.Theorems.HasseArf.HerbrandFunctionAtLowerIndexNatOfJump
2 declarations indexed from sourceView source ↗

Module documentation

Natural Herbrand values at lower ramification jumps

The finite-sum Herbrand value is nonnegative at every integral lower index. For a finite Abelian extension of nonarchimedean local fields, Hasse--Arf therefore makes the value at each lower jump a natural number.

Imports4
Imported by1

Declarations

theorem

herbrandFunctionAtLowerIndex_nonneg

L25 ↗
ClassFieldTheory.herbrandFunctionAtLowerIndex_nonneg
Documentation

The rational Herbrand value at any integral lower index is nonnegative.

Source context 2 commands

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

namespace ClassFieldTheory
universe u v
Lean source · statement
theorem herbrandFunctionAtLowerIndex_nonneg
    (K : Type u) {L : Type v} [Field K] [Field L] [Algebra K L]
    (A : ValuationSubring L) (n : ℕ) :
    0 ≤ herbrandFunctionAtLowerIndex K A n
theorem

herbrandFunctionAtLowerIndex_eq_nat_of_isLowerRamificationJump

L38 ↗
ClassFieldTheory.herbrandFunctionAtLowerIndex_eq_nat_of_isLowerRamificationJump
Documentation

At an integral lower ramification jump of a finite Abelian local extension, the rational Herbrand value is a natural number.

Source context 2 commands

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

namespace ClassFieldTheory
universe u v
Lean source · statement
theorem herbrandFunctionAtLowerIndex_eq_nat_of_isLowerRamificationJump
    (K : Type u) (L : Type v) [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) :
    ∃ m : ℕ,
      herbrandFunctionAtLowerIndex K
        (ValuativeRel.valuation L).valuationSubring n = (m : ℚ)

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.