Module

DVFEmbedding.lean

Nyll.ValuedFieldTheory.Valuation.Completion.DVFEmbedding

4 declarations indexed from sourceView source ↗

Module documentation

Completion maps for extensions of discrete valuations

Powers of a ground-field uniformizer are cofinal in the target valuation balls. The Archimedean property is used only for the actual value group of the target valuation, which is order-isomorphic to the multiplicative integers with zero. Thus an extension of discrete valuations induces a uniformly continuous field map and an actual map of completions.

Imports6

Nyll.ValuedFieldTheory.Valuation.DiscreteValuationField.ValuationTransport
Mathlib.GroupTheory.ArchimedeanDensely
Mathlib.RingTheory.Valuation.Discrete.RankOne
Mathlib.RingTheory.Valuation.Extension
Mathlib.Topology.Algebra.UniformRing
Mathlib.Topology.Algebra.Valued.WithVal

Imported by4

theorem

withValMap_uniformContinuous

L33 ↗

ValuationTheory.DiscreteValuationField.DVF.withValMap_uniformContinuous

Documentation

The actual field embedding is uniformly continuous for the two discrete valuation topologies. No agreement of independently normalized norms is needed.

Source context 3 commands

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

namespace ValuationTheory.DiscreteValuationField.DVF
open MonoidWithZeroHom
variable {K L : Type*} [Field K] [Field L] [Algebra K L]
  (base : DVF K) (target : DVF L) [base.valuation.HasExtension target.valuation]

Lean source · statement

theorem withValMap_uniformContinuous :
    UniformContinuous (WithVal.map base.valuation target.valuation (algebraMap K L))

def

completionMap

L78 ↗

ValuationTheory.DiscreteValuationField.DVF.completionMap

Documentation

The map of completions induced by an extension of discrete valuations.

Source context 3 commands

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

namespace ValuationTheory.DiscreteValuationField.DVF
open MonoidWithZeroHom
variable {K L : Type*} [Field K] [Field L] [Algebra K L]
  (base : DVF K) (target : DVF L) [base.valuation.HasExtension target.valuation]

Lean source · statement

def completionMap : base.valuation.Completion →+* target.valuation.Completion

theorem

completionMap_coe

L84 ↗

ValuationTheory.DiscreteValuationField.DVF.completionMap_coe

Documentation

The completion map agrees with the actual field embedding on WithVal.

Source context 3 commands

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

namespace ValuationTheory.DiscreteValuationField.DVF
open MonoidWithZeroHom
variable {K L : Type*} [Field K] [Field L] [Algebra K L]
  (base : DVF K) (target : DVF L) [base.valuation.HasExtension target.valuation]

Lean source · statement

theorem completionMap_coe (x : WithVal base.valuation) :
    completionMap base target (x : base.valuation.Completion) =
      (WithVal.map base.valuation target.valuation (algebraMap K L) x :
        target.valuation.Completion)

theorem

completionMap_coe_base

L92 ↗

ValuationTheory.DiscreteValuationField.DVF.completionMap_coe_base

Documentation

On an original ground-field element, the completion map is the algebra map.

Source context 3 commands

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

namespace ValuationTheory.DiscreteValuationField.DVF
open MonoidWithZeroHom
variable {K L : Type*} [Field K] [Field L] [Algebra K L]
  (base : DVF K) (target : DVF L) [base.valuation.HasExtension target.valuation]

Lean source · statement

theorem completionMap_coe_base (x : K) :
    completionMap base target (x : base.valuation.Completion) =
      (algebraMap K L x : target.valuation.Completion)

Module documentation

Completion maps for extensions of discrete valuations

Declarations

withValMap_uniformContinuous

completionMap

completionMap_coe

completionMap_coe_base