Module

Valuation.lean

Nyll.ValuedFieldTheory.LocalField.NonarchimedeanLocalField.Valuation

5 declarations indexed from sourceView source ↗

Module documentation

Integer-valued valuations

Relates membership in the valuation ring to the ambient valuation and exposes the associated surjective multiplicative valuation with a uniformizer.

Imports2

Imported by3

theorem

valuation_integer_membership

L28 ↗

LocalFieldTheory.IsNonarchimedeanLocalField.valuation_integer_membership

Documentation

An element belongs to the valuation ring exactly when its valuation is at most one.

Source context 6 commands

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

namespace LocalFieldTheory
noncomputable section
universe u
namespace IsNonarchimedeanLocalField
open DiscreteValuationField
open scoped ValuativeRel

Lean source · statement

theorem valuation_integer_membership
    (K : Type u) [Field K] [ValuativeRel K] (x : K) :
    x ∈ 𝒪[K] ↔ ValuativeRel.valuation K x ≤ 1

def

multiplicativeIntegerValuation

L35 ↗

LocalFieldTheory.IsNonarchimedeanLocalField.multiplicativeIntegerValuation

Documentation

The normalized integer valuation, packaged as the MultiplicativeIntegerValuation used by the value-group layer.

Source context 6 commands

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

namespace LocalFieldTheory
noncomputable section
universe u
namespace IsNonarchimedeanLocalField
open DiscreteValuationField
open scoped ValuativeRel

Lean source · full declaration

def multiplicativeIntegerValuation
    (K : Type u) [Field K] [ValuativeRel K] [TopologicalSpace K]
    [IsNonarchimedeanLocalField K] :
    MultiplicativeIntegerValuation Kˣ where
  val x := LocalFieldTheory.IsNonarchimedeanLocalField.v K (Additive.ofMul x)
  map_one := by
    exact LocalFieldTheory.IsNonarchimedeanLocalField.v_one K
  map_mul x y := by
    exact LocalFieldTheory.IsNonarchimedeanLocalField.v_mul K x y

theorem

multiplicativeIntegerValuation_val

L47 ↗

LocalFieldTheory.IsNonarchimedeanLocalField.multiplicativeIntegerValuation_val

Documentation

The multiplicative integer valuation records the additive integer exponent of the original valuation.

Source context 6 commands

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

namespace LocalFieldTheory
noncomputable section
universe u
namespace IsNonarchimedeanLocalField
open DiscreteValuationField
open scoped ValuativeRel

Lean source · statement

theorem multiplicativeIntegerValuation_val
    (K : Type u) [Field K] [ValuativeRel K] [TopologicalSpace K]
    [IsNonarchimedeanLocalField K] (x : Kˣ) :
    (multiplicativeIntegerValuation K).val x =
      LocalFieldTheory.IsNonarchimedeanLocalField.v K (Additive.ofMul x)

theorem

multiplicativeIntegerValuation_surjective

L55 ↗

LocalFieldTheory.IsNonarchimedeanLocalField.multiplicativeIntegerValuation_surjective

Documentation

The normalized integer valuation is onto ℤ.

Source context 6 commands

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

namespace LocalFieldTheory
noncomputable section
universe u
namespace IsNonarchimedeanLocalField
open DiscreteValuationField
open scoped ValuativeRel

Lean source · statement

theorem multiplicativeIntegerValuation_surjective
    (K : Type u) [Field K] [ValuativeRel K] [TopologicalSpace K]
    [IsNonarchimedeanLocalField K] :
    Function.Surjective (multiplicativeIntegerValuation K).val

theorem

multiplicativeIntegerValuation_exists_uniformizer

L66 ↗

LocalFieldTheory.IsNonarchimedeanLocalField.multiplicativeIntegerValuation_exists_uniformizer

Documentation

A nonarchimedean local field has a multiplicative element of normalized value one for the value-group API.

Source context 6 commands

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

namespace LocalFieldTheory
noncomputable section
universe u
namespace IsNonarchimedeanLocalField
open DiscreteValuationField
open scoped ValuativeRel

Lean source · statement

theorem multiplicativeIntegerValuation_exists_uniformizer
    (K : Type u) [Field K] [ValuativeRel K] [TopologicalSpace K]
    [IsNonarchimedeanLocalField K] :
    ∃ ϖ : Kˣ, (multiplicativeIntegerValuation K).IsUniformizer ϖ

Module documentation

Integer-valued valuations

Declarations

valuation_integer_membership

multiplicativeIntegerValuation

multiplicativeIntegerValuation_val

multiplicativeIntegerValuation_surjective

multiplicativeIntegerValuation_exists_uniformizer