Module

LocalHenselianValuation.lean

Nyll.ClassFieldTheory.LocalClassFieldTheory.Finite.LocalReciprocity.LocalHenselianValuation

1 declaration indexed from sourceView source ↗

Module documentation

Finite local reciprocity: the normalized local valuation is Henselian

For a nonarchimedean local field, the normalized discrete valuation on the base unit group satisfies the Henselian valuation condition. The value group is the copy of the ordinary integers in the profinite integers. For every finite abstract field, including a non-normal one, the image after the abstract norm is the ordinary residue-degree multiple of that value group.

Imports3

Imported by6

def

localHenselianValuation

L36 ↗

LocalClassFieldTheory.localHenselianValuation

Documentation

Finite local reciprocity. The normalized valuation of a nonarchimedean local field, on the actual fixed coefficient group in its separable closure, is a Henselian valuation relative to the residue Frobenius degree datum.

Source context 5 commands

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

namespace LocalClassFieldTheory
open ClassFormation LocalFieldTheory
noncomputable section
open scoped NNReal ValuativeRel
open _root_.ValuationTheory.DiscreteValuationField.Valuation (
  valuationSubring_isIntegralClosure_of_isIntegral
) in

Lean source · statement

def localHenselianValuation
    (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K]
    [IsNonarchimedeanLocalField K] :
    ValuationData (localResidueDatum K)
      (galoisAmbientUnitsRep K (SeparableClosure K))

Module documentation

Finite local reciprocity: the normalized local valuation is Henselian

Declarations

localHenselianValuation