Module

DiscreteRingEquiv.lean

Nyll.ValuedFieldTheory.Valuation.Completion.DiscreteRingEquiv

3 declarations indexed from sourceView source ↗

Module documentation

Completion of an isomorphism preserving discrete valuations

A field isomorphism which carries one valuation to an equivalent valuation induces an isomorphism of the actual valued completions. The construction preserves the original embedding of the field.

Imports5

Nyll.ValuedFieldTheory.Valuation.DiscreteValuationField.ValuationTransport
Nyll.ValuedFieldTheory.Valuation.Completion.WithValScalars
Mathlib.GroupTheory.ArchimedeanDensely
Mathlib.RingTheory.Valuation.Discrete.RankOne
Mathlib.Topology.Algebra.UniformRing

Imported by4

theorem

withValRingEquiv_uniformContinuous

L30 ↗

ValuationTheory.DiscreteValuationField.DVF.withValRingEquiv_uniformContinuous

Documentation

Preservation of the valuation ordering makes a field isomorphism uniformly continuous on the associated valued fields.

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]
  (source : DVF K) (target : DVF L)

Lean source · statement

theorem withValRingEquiv_uniformContinuous (e : K ≃+* L)
    (he : source.valuation.IsEquiv (target.valuation.comap e.toRingHom)) :
    UniformContinuous (WithVal.congr source.valuation target.valuation e)

def

completionRingEquiv

L74 ↗

ValuationTheory.DiscreteValuationField.DVF.completionRingEquiv

Documentation

The equivalence of completed fields induced by a valuation preserving field isomorphism.

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]
  (source : DVF K) (target : DVF L)

Lean source · statement

def completionRingEquiv (e : K ≃+* L)
    (he : source.valuation.IsEquiv (target.valuation.comap e.toRingHom)) :
    source.valuation.Completion ≃+* target.valuation.Completion

theorem

completionRingEquiv_algebraMap

L88 ↗

ValuationTheory.DiscreteValuationField.DVF.completionRingEquiv_algebraMap

Documentation

The completed isomorphism restricts to the supplied isomorphism on the original fields.

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]
  (source : DVF K) (target : DVF L)

Lean source · statement

theorem completionRingEquiv_algebraMap (e : K ≃+* L)
    (he : source.valuation.IsEquiv (target.valuation.comap e.toRingHom)) (x : K) :
    completionRingEquiv source target e he (algebraMap K source.valuation.Completion x) =
      algebraMap L target.valuation.Completion (e x)

Module documentation

Completion of an isomorphism preserving discrete valuations

Declarations

withValRingEquiv_uniformContinuous

completionRingEquiv

completionRingEquiv_algebraMap