Module

Valuation.lean

Nyll.SchemeTheory.AbhyankarLemma.TameRamification.ValueGroup.NonarchimedeanLocalField.Valuation

5 declarations indexed from sourceView source ↗

Module documentation

Neu1999 local-field valuations

This file packages the normalized integer valuation from IsNonarchimedeanLocalField as the MultiplicativeIntegerValuation used by the tame Abhyankar value-group layer, and rewrites the Neu1999 norm formula for the field-norm API.

Imports3

Imported by3

def

multiplicativeIntegerValuation

L33 ↗

TameAbhyankar.NAField.multiplicativeIntegerValuation

Documentation

The Neu1999 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.

noncomputable section
universe u
namespace TameAbhyankar
open LocalFieldTheory LocalFieldTheory.DiscreteValuationField
open scoped ValuativeRel
namespace NAField

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

L43 ↗

TameAbhyankar.NAField.multiplicativeIntegerValuation_val

Source context 6 commands

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

noncomputable section
universe u
namespace TameAbhyankar
open LocalFieldTheory LocalFieldTheory.DiscreteValuationField
open scoped ValuativeRel
namespace NAField

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

L51 ↗

TameAbhyankar.NAField.multiplicativeIntegerValuation_surjective

Documentation

The Neu1999 normalized integer valuation is onto ℤ.

Source context 6 commands

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

noncomputable section
universe u
namespace TameAbhyankar
open LocalFieldTheory LocalFieldTheory.DiscreteValuationField
open scoped ValuativeRel
namespace NAField

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

L62 ↗

TameAbhyankar.NAField.multiplicativeIntegerValuation_exists_uniformizer

Documentation

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

Source context 6 commands

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

noncomputable section
universe u
namespace TameAbhyankar
open LocalFieldTheory LocalFieldTheory.DiscreteValuationField
open scoped ValuativeRel
namespace NAField

Lean source · statement

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

theorem

fieldNormUnits_valuation_formula

L71 ↗

TameAbhyankar.NAField.fieldNormUnits_valuation_formula

Documentation

The Neu1999 norm-valuation formula, rewritten for the LocalFieldTheory.normUnits API used by the value-group layer.

Source context 6 commands

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

noncomputable section
universe u
namespace TameAbhyankar
open LocalFieldTheory LocalFieldTheory.DiscreteValuationField
open scoped ValuativeRel
namespace NAField

Lean source · statement

theorem fieldNormUnits_valuation_formula
    (K L : Type u)
    [Field K] [ValuativeRel K] [TopologicalSpace K]
    [IsNonarchimedeanLocalField K]
    [Field L] [ValuativeRel L] [TopologicalSpace L]
    [IsNonarchimedeanLocalField L]
    [Algebra K L] [FiniteDimensional K L] [Algebra.IsSeparable K L]
    [Valuation.HasExtension (ValuativeRel.valuation K)
      (ValuativeRel.valuation L)]
    (x : Lˣ) :
    (multiplicativeIntegerValuation K).val (normUnits K L x) =
      (Module.finrank 𝓀[K] 𝓀[L] : ℤ) *
        (multiplicativeIntegerValuation L).val x

Module documentation

Neu1999 local-field valuations

Declarations

multiplicativeIntegerValuation

multiplicativeIntegerValuation_val

multiplicativeIntegerValuation_surjective

multiplicativeIntegerValuation_exists_uniformizer

fieldNormUnits_valuation_formula