Module

Basic.lean

Nyll.ValuedFieldTheory.LocalField.NonarchimedeanLocalField.Basic

19 declarations indexed from sourceView source ↗

Module documentation

Basic structure of nonarchimedean local fields

Compactness facts and the normalized integer-valued valuation attached to a nonarchimedean local field.

Imports1

Mathlib.NumberTheory.LocalField.Basic

Imported by10

def

v

L29 ↗

LocalFieldTheory.IsNonarchimedeanLocalField.v

Documentation

The normalized integer valuation attached to a nonarchimedean local field.

It is obtained by transporting the value group to WithZero (Multiplicative Int) and then taking the exponent of the nonzero value of a field unit.

Source context 5 commands

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

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

Lean source · statement

def v (K : Type u) [Field K] [ValuativeRel K] [TopologicalSpace K]
    [IsNonarchimedeanLocalField K] : Additive Kˣ → Int

theorem

v_apply

L41 ↗

LocalFieldTheory.IsNonarchimedeanLocalField.v_apply

Documentation

The normalized integer valuation is obtained by transporting the field valuation to multiplicative integers and taking its additive exponent.

Source context 5 commands

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

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

Lean source · full declaration

theorem v_apply (K : Type u) [Field K] [ValuativeRel K] [TopologicalSpace K]
    [IsNonarchimedeanLocalField K] (x : Additive Kˣ) :
    v K x =
      Multiplicative.toAdd
        (WithZero.unzero
          (x := (_root_.IsNonarchimedeanLocalField.valueGroupWithZeroIsoInt K)
            (ValuativeRel.valuation K ((Additive.toMul x : Kˣ) : K)))
          (by simp)) :=
  rfl

theorem

v_surjective

L52 ↗

LocalFieldTheory.IsNonarchimedeanLocalField.v_surjective

Documentation

Every integer occurs as the normalized valuation of a nonzero field element.

Source context 5 commands

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

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

Lean source · statement

theorem v_surjective (K : Type u) [Field K] [ValuativeRel K] [TopologicalSpace K]
    [IsNonarchimedeanLocalField K] :
    Function.Surjective (v K)

theorem

v_mul

L71 ↗

LocalFieldTheory.IsNonarchimedeanLocalField.v_mul

Documentation

The normalized valuation turns multiplication of field units into addition of integers.

Source context 5 commands

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

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

Lean source · statement

theorem v_mul (K : Type u) [Field K] [ValuativeRel K] [TopologicalSpace K]
    [IsNonarchimedeanLocalField K] (x y : Kˣ) :
    v K (Additive.ofMul (x * y)) =
      v K (Additive.ofMul x) + v K (Additive.ofMul y)

theorem

v_one

L79 ↗

LocalFieldTheory.IsNonarchimedeanLocalField.v_one

Documentation

The normalized valuation of the multiplicative identity is zero.

Source context 5 commands

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

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

Lean source · statement

theorem v_one (K : Type u) [Field K] [ValuativeRel K] [TopologicalSpace K]
    [IsNonarchimedeanLocalField K] :
    v K (Additive.ofMul (1 : Kˣ)) = 0

theorem

v_inv

L95 ↗

LocalFieldTheory.IsNonarchimedeanLocalField.v_inv

Documentation

The normalized valuation of an inverse is the negative of the original valuation.

Source context 5 commands

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

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

Lean source · statement

theorem v_inv (K : Type u) [Field K] [ValuativeRel K] [TopologicalSpace K]
    [IsNonarchimedeanLocalField K] (x : Kˣ) :
    v K (Additive.ofMul x⁻¹) = -v K (Additive.ofMul x)

theorem

v_div

L103 ↗

LocalFieldTheory.IsNonarchimedeanLocalField.v_div

Documentation

The normalized valuation of a quotient is the difference of the two valuations.

Source context 5 commands

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

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

Lean source · statement

theorem v_div (K : Type u) [Field K] [ValuativeRel K] [TopologicalSpace K]
    [IsNonarchimedeanLocalField K] (x y : Kˣ) :
    v K (Additive.ofMul (x / y)) =
      v K (Additive.ofMul x) - v K (Additive.ofMul y)

theorem

v_pow

L110 ↗

LocalFieldTheory.IsNonarchimedeanLocalField.v_pow

Documentation

Raising a field unit to a natural power multiplies its normalized valuation by that power.

Source context 5 commands

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

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

Lean source · statement

theorem v_pow (K : Type u) [Field K] [ValuativeRel K] [TopologicalSpace K]
    [IsNonarchimedeanLocalField K] (x : Kˣ) (n : Nat) :
    v K (Additive.ofMul (x ^ n)) = (n : Int) * v K (Additive.ofMul x)

theorem

v_zpow

L124 ↗

LocalFieldTheory.IsNonarchimedeanLocalField.v_zpow

Documentation

Raising a field unit to an integral power multiplies its normalized valuation by that integer. Raising a field unit to an integral power multiplies its normalized valuation by that integer.

Source context 5 commands

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

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

Lean source · statement

theorem v_zpow (K : Type u) [Field K] [ValuativeRel K] [TopologicalSpace K]
    [IsNonarchimedeanLocalField K] (x : Kˣ) (n : Int) :
    v K (Additive.ofMul (x ^ n)) = n * v K (Additive.ofMul x)

theorem

v_mul_zpow

L138 ↗

LocalFieldTheory.IsNonarchimedeanLocalField.v_mul_zpow

Documentation

The valuation of a unit times an integral power is the valuation of the unit plus the scaled valuation of the powered factor.

Source context 5 commands

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

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

Lean source · statement

theorem v_mul_zpow (K : Type u) [Field K] [ValuativeRel K] [TopologicalSpace K]
    [IsNonarchimedeanLocalField K] (x ϖ : Kˣ) (n : Int) :
    v K (Additive.ofMul (x * ϖ ^ n)) =
      v K (Additive.ofMul x) + n * v K (Additive.ofMul ϖ)

theorem

v_zpow_of_uniformizer

L145 ↗

LocalFieldTheory.IsNonarchimedeanLocalField.v_zpow_of_uniformizer

Documentation

An integral power of a normalized uniformizer has valuation equal to its exponent.

Source context 5 commands

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

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

Lean source · statement

theorem v_zpow_of_uniformizer (K : Type u) [Field K] [ValuativeRel K]
    [TopologicalSpace K] [IsNonarchimedeanLocalField K] (ϖ : Kˣ)
    (hϖ : v K (Additive.ofMul ϖ) = 1) (n : Int) :
    v K (Additive.ofMul (ϖ ^ n)) = n

theorem

v_mul_zpow_of_uniformizer

L152 ↗

LocalFieldTheory.IsNonarchimedeanLocalField.v_mul_zpow_of_uniformizer

Documentation

Multiplying by the n-th power of a normalized uniformizer shifts valuation by n.

Source context 5 commands

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

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

Lean source · statement

theorem v_mul_zpow_of_uniformizer (K : Type u) [Field K] [ValuativeRel K]
    [TopologicalSpace K] [IsNonarchimedeanLocalField K] (x ϖ : Kˣ)
    (hϖ : v K (Additive.ofMul ϖ) = 1) (n : Int) :
    v K (Additive.ofMul (x * ϖ ^ n)) = v K (Additive.ofMul x) + n

theorem

v_div_eq_zero_iff

L160 ↗

LocalFieldTheory.IsNonarchimedeanLocalField.v_div_eq_zero_iff

Documentation

A quotient has valuation zero exactly when its numerator and denominator have equal valuation. A quotient has valuation zero exactly when its numerator and denominator have equal valuation.

Source context 5 commands

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

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

Lean source · statement

theorem v_div_eq_zero_iff (K : Type u) [Field K] [ValuativeRel K]
    [TopologicalSpace K] [IsNonarchimedeanLocalField K] (x y : Kˣ) :
    v K (Additive.ofMul (x / y)) = 0 ↔
      v K (Additive.ofMul x) = v K (Additive.ofMul y)

theorem

v_eq_iff_v_div_eq_zero

L167 ↗

LocalFieldTheory.IsNonarchimedeanLocalField.v_eq_iff_v_div_eq_zero

Documentation

Two field units have equal valuation exactly when their quotient has valuation zero.

Source context 5 commands

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

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

Lean source · statement

theorem v_eq_iff_v_div_eq_zero (K : Type u) [Field K] [ValuativeRel K]
    [TopologicalSpace K] [IsNonarchimedeanLocalField K] (x y : Kˣ) :
    v K (Additive.ofMul x) = v K (Additive.ofMul y) ↔
      v K (Additive.ofMul (x / y)) = 0

theorem

v_uniformiser

L174 ↗

LocalFieldTheory.IsNonarchimedeanLocalField.v_uniformiser

Documentation

A nonarchimedean local field contains a unit representative of normalized valuation one.

Source context 5 commands

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

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

Lean source · statement

theorem v_uniformiser (K : Type u) [Field K] [ValuativeRel K] [TopologicalSpace K]
    [IsNonarchimedeanLocalField K] :
    ∃ ϖ : Kˣ, v K (Additive.ofMul ϖ) = 1

def

integerUnitsToFieldUnits

L181 ↗

LocalFieldTheory.IsNonarchimedeanLocalField.integerUnitsToFieldUnits

Documentation

The canonical inclusion of valuation-integer units into field units.

Source context 5 commands

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

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

Lean source · statement

def integerUnitsToFieldUnits (K : Type u) [Field K] [ValuativeRel K] : 𝒪[K]ˣ →* Kˣ

theorem

integerUnitsToFieldUnits_apply

L187 ↗

LocalFieldTheory.IsNonarchimedeanLocalField.integerUnitsToFieldUnits_apply

Documentation

The inclusion of valuation-ring units into field units preserves the underlying field element. The inclusion of valuation-ring units into field units preserves the underlying field element.

Source context 5 commands

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

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

Lean source · statement

theorem integerUnitsToFieldUnits_apply (K : Type u) [Field K] [ValuativeRel K]
    (x : 𝒪[K]ˣ) :
    ((integerUnitsToFieldUnits K x : Kˣ) : K) = (((x : 𝒪[K]ˣ) : 𝒪[K]) : K)

theorem

integerUnitsToFieldUnits_injective

L194 ↗

LocalFieldTheory.IsNonarchimedeanLocalField.integerUnitsToFieldUnits_injective

Documentation

The canonical inclusion of valuation-integer units into field units is injective.

Source context 5 commands

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

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

Lean source · statement

theorem integerUnitsToFieldUnits_injective
    (K : Type u) [Field K] [ValuativeRel K] :
    Function.Injective (integerUnitsToFieldUnits K)

theorem

v_integerUnitsToFieldUnits

L204 ↗

LocalFieldTheory.IsNonarchimedeanLocalField.v_integerUnitsToFieldUnits

Documentation

A valuation-integer unit has normalized valuation zero as a field unit.

Source context 5 commands

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

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

Lean source · statement

theorem v_integerUnitsToFieldUnits (K : Type u) [Field K] [ValuativeRel K]
    [TopologicalSpace K] [IsNonarchimedeanLocalField K] (x : 𝒪[K]ˣ) :
    v K (Additive.ofMul (integerUnitsToFieldUnits K x)) = 0

Module documentation

Basic structure of nonarchimedean local fields

Declarations