Module

MultiplicativeDecomposition.lean

Nyll.ValuedFieldTheory.LocalField.NonarchimedeanLocalField.MultiplicativeDecomposition

11 declarations indexed from sourceView source ↗

Module documentation

Topological decomposition of a local multiplicative group

This file packages the normalized valuation and the unit factor in the standard decomposition of Kˣ as continuous homomorphisms. After fixing a noncanonical uniformizer internally, the resulting parameter-free map lets downstream separation arguments avoid carrying a uniformizer parameter.

Imports4

Nyll.ValuedFieldTheory.LocalField.NonarchimedeanLocalField.NormContinuity
Nyll.ValuedFieldTheory.LocalField.NonarchimedeanLocalField.ProfiniteUnits
Nyll.ValuedFieldTheory.LocalField.NonarchimedeanLocalField.ValuationExactSequence
Mathlib.Topology.LocallyConstant.Basic

Imported by2

theorem

valuationUnitsMulHom_eq_iff_valuation_eq

L32 ↗

LocalFieldTheory.IsNonarchimedeanLocalField.valuationUnitsMulHom_eq_iff_valuation_eq

Documentation

Equality under the normalized valuation is equality under the field valuation.

Source context 4 commands

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

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

Lean source · statement

theorem valuationUnitsMulHom_eq_iff_valuation_eq
    (K : Type u) [Field K] [ValuativeRel K] [TopologicalSpace K]
    [IsNonarchimedeanLocalField K] (x y : Kˣ) :
    valuationUnitsMulHom K x = valuationUnitsMulHom K y ↔
      ValuativeRel.valuation K (x : K) = ValuativeRel.valuation K (y : K)

theorem

valuationUnitsMulHom_continuous

L47 ↗

LocalFieldTheory.IsNonarchimedeanLocalField.valuationUnitsMulHom_continuous

Documentation

The normalized valuation on Kˣ, viewed multiplicatively, is continuous.

Source context 4 commands

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

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

Lean source · statement

theorem valuationUnitsMulHom_continuous
    (K : Type u) [Field K] [ValuativeRel K] [TopologicalSpace K]
    [IsNonarchimedeanLocalField K] : Continuous (valuationUnitsMulHom K)

def

valuationUnitsContinuousMonoidHom

L67 ↗

LocalFieldTheory.IsNonarchimedeanLocalField.valuationUnitsContinuousMonoidHom

Documentation

The normalized valuation as a continuous multiplicative homomorphism.

Source context 4 commands

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

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

Lean source · full declaration

def valuationUnitsContinuousMonoidHom
    (K : Type u) [Field K] [ValuativeRel K] [TopologicalSpace K]
    [IsNonarchimedeanLocalField K] : Kˣ →ₜ* Multiplicative Int where
  toMonoidHom := valuationUnitsMulHom K
  continuous_toFun := valuationUnitsMulHom_continuous K

theorem

uniformizerUnitFactor_one

L75 ↗

LocalFieldTheory.IsNonarchimedeanLocalField.uniformizerUnitFactor_one

Documentation

The unit factor of one is one.

Source context 4 commands

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

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

Lean source · statement

theorem uniformizerUnitFactor_one
    (K : Type u) [Field K] [ValuativeRel K] [TopologicalSpace K]
    [IsNonarchimedeanLocalField K]
    (ϖ : Kˣ) (hϖ : valuationMap K (Additive.ofMul ϖ) = 1) :
    uniformizerUnitFactor K ϖ hϖ 1 = 1

theorem

uniformizerUnitFactor_mul

L86 ↗

LocalFieldTheory.IsNonarchimedeanLocalField.uniformizerUnitFactor_mul

Documentation

The unit factor respects multiplication.

Source context 4 commands

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

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

Lean source · statement

theorem uniformizerUnitFactor_mul
    (K : Type u) [Field K] [ValuativeRel K] [TopologicalSpace K]
    [IsNonarchimedeanLocalField K]
    (ϖ : Kˣ) (hϖ : valuationMap K (Additive.ofMul ϖ) = 1)
    (x y : Kˣ) :
    uniformizerUnitFactor K ϖ hϖ (x * y) =
      uniformizerUnitFactor K ϖ hϖ x * uniformizerUnitFactor K ϖ hϖ y

def

uniformizerUnitFactorMonoidHom

L101 ↗

LocalFieldTheory.IsNonarchimedeanLocalField.uniformizerUnitFactorMonoidHom

Documentation

The unit factor in the uniformizer decomposition as a homomorphism.

Source context 4 commands

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

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

Lean source · full declaration

def uniformizerUnitFactorMonoidHom
    (K : Type u) [Field K] [ValuativeRel K] [TopologicalSpace K]
    [IsNonarchimedeanLocalField K]
    (ϖ : Kˣ) (hϖ : valuationMap K (Additive.ofMul ϖ) = 1) :
    Kˣ →* 𝒪[K]ˣ where
  toFun := uniformizerUnitFactor K ϖ hϖ
  map_one' := uniformizerUnitFactor_one K ϖ hϖ
  map_mul' := uniformizerUnitFactor_mul K ϖ hϖ

theorem

uniformizerUnitFactor_continuous

L111 ↗

LocalFieldTheory.IsNonarchimedeanLocalField.uniformizerUnitFactor_continuous

Documentation

The unit factor in the uniformizer decomposition is continuous.

Source context 4 commands

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

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

Lean source · statement

theorem uniformizerUnitFactor_continuous
    (K : Type u) [Field K] [ValuativeRel K] [TopologicalSpace K]
    [IsNonarchimedeanLocalField K]
    (ϖ : Kˣ) (hϖ : valuationMap K (Additive.ofMul ϖ) = 1) :
    Continuous (uniformizerUnitFactor K ϖ hϖ)

def

uniformizerUnitFactorContinuousMonoidHom

L144 ↗

LocalFieldTheory.IsNonarchimedeanLocalField.uniformizerUnitFactorContinuousMonoidHom

Documentation

The unit factor in the uniformizer decomposition as a continuous homomorphism.

Source context 4 commands

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

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

Lean source · full declaration

def uniformizerUnitFactorContinuousMonoidHom
    (K : Type u) [Field K] [ValuativeRel K] [TopologicalSpace K]
    [IsNonarchimedeanLocalField K]
    (ϖ : Kˣ) (hϖ : valuationMap K (Additive.ofMul ϖ) = 1) :
    Kˣ →ₜ* 𝒪[K]ˣ where
  toMonoidHom := uniformizerUnitFactorMonoidHom K ϖ hϖ
  continuous_toFun := uniformizerUnitFactor_continuous K ϖ hϖ

def

chosenLocalUniformizer

L153 ↗

LocalFieldTheory.IsNonarchimedeanLocalField.chosenLocalUniformizer

Documentation

The fixed noncanonical uniformizer used by the parameter-free unit map.

Source context 4 commands

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

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

Lean source · statement

def chosenLocalUniformizer
    (K : Type u) [Field K] [ValuativeRel K] [TopologicalSpace K]
    [IsNonarchimedeanLocalField K] : Kˣ

theorem

chosenLocalUniformizer_spec

L160 ↗

LocalFieldTheory.IsNonarchimedeanLocalField.chosenLocalUniformizer_spec

Documentation

The chosen local uniformizer has normalized valuation one.

Source context 4 commands

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

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

Lean source · statement

theorem chosenLocalUniformizer_spec
    (K : Type u) [Field K] [ValuativeRel K] [TopologicalSpace K]
    [IsNonarchimedeanLocalField K] :
    valuationMap K (Additive.ofMul (chosenLocalUniformizer K)) = 1

def

localUnitFactorContinuousMonoidHom

L167 ↗

LocalFieldTheory.IsNonarchimedeanLocalField.localUnitFactorContinuousMonoidHom

Documentation

A parameter-free continuous projection from Kˣ to its unit factor.

Source context 4 commands

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

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

Lean source · statement

def localUnitFactorContinuousMonoidHom
    (K : Type u) [Field K] [ValuativeRel K] [TopologicalSpace K]
    [IsNonarchimedeanLocalField K] : Kˣ →ₜ* 𝒪[K]ˣ

Module documentation

Topological decomposition of a local multiplicative group

Declarations