NYLL
Module

HerbrandFunctionCanonical.lean

Nyll.ClassFieldTheory.Theorems.HasseArf.HerbrandFunctionCanonical
1 declaration indexed from sourceView source ↗

Module documentation

Strict growth of the public Herbrand function

The piecewise function defined from the public integral lower groups agrees with the existing Herbrand function of the local lower filtration. Its strict growth is consequently available without exposing that filtration in the public theorem statement.

Imports3
Imported by2

Declarations

theorem

herbrandFunction_canonical_strictMono

L31 ↗
ClassFieldTheory.herbrandFunction_canonical_strictMono
Documentation

For a finite Abelian extension of nonarchimedean local fields, the Herbrand function built from the canonical lower groups is strictly increasing on the real line.

Source context 5 commands

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

noncomputable section
namespace ClassFieldTheory
open LocalFieldTheory
open RamificationTheory.LocalField
open RamificationTheory.HilbertRamification.Higher
Lean source · statement
theorem herbrandFunction_canonical_strictMono
    (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)] :
    StrictMono (ClassFieldTheory.herbrandFunction K
      (ValuativeRel.valuation L).valuationSubring)

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