NYLL
Module

NormedModel.lean

Nyll.ValuedFieldTheory.Valuation.DiscreteValuationField.NormedModel
6 declarations indexed from sourceView source ↗

Module documentation

The normed model of a discrete valuation

Use the existing WithVal field with the rank-one embedding of base 2. The resulting norm has exactly the original valuation ring, transported by WithVal.equiv. The normed structures below are local to this file.

Imports4
Imported by4

Declarations

instance

(anonymous instance)

L28 ↗
Source context 4 commands

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

noncomputable section
namespace ValuationTheory.DiscreteValuationField.DVF
universe u v
variable {K : Type u} [Field K] (base : DVF.{u, v} K)
Lean source · statement
instance :
    (Valued.v : _root_.Valuation (WithVal base.valuation) base.ValueGroup).IsRankOneDiscrete
instance

(anonymous instance)

L32 ↗
Source context 5 commands

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

noncomputable section
namespace ValuationTheory.DiscreteValuationField.DVF
universe u v
variable {K : Type u} [Field K] (base : DVF.{u, v} K)
local instance :
    (Valued.v : _root_.Valuation (WithVal base.valuation) base.ValueGroup).IsRankOneDiscrete :=
  Valuation.isRankOneDiscrete_comap_ringEquiv base.valuation (WithVal.equiv base.valuation)
Lean source · statement
instance :
    (Valued.v : _root_.Valuation (WithVal base.valuation) base.ValueGroup).RankOne
instance

(anonymous instance)

L38 ↗
Source context 6 commands

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

noncomputable section
namespace ValuationTheory.DiscreteValuationField.DVF
universe u v
variable {K : Type u} [Field K] (base : DVF.{u, v} K)
local instance :
    (Valued.v : _root_.Valuation (WithVal base.valuation) base.ValueGroup).IsRankOneDiscrete :=
  Valuation.isRankOneDiscrete_comap_ringEquiv base.valuation (WithVal.equiv base.valuation)
local instance :
    (Valued.v : _root_.Valuation (WithVal base.valuation) base.ValueGroup).RankOne :=
  _root_.Valuation.IsRankOneDiscrete.rankOne
    (Valued.v : _root_.Valuation (WithVal base.valuation) base.ValueGroup)
    (e := 2) (by norm_num)
Lean source · statement
instance : NontriviallyNormedField (WithVal base.valuation)
theorem

normedWithVal_mem_valuationSubring_iff

L41 ↗
ValuationTheory.DiscreteValuationField.DVF.normedWithVal_mem_valuationSubring_iff
Source context 7 commands

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

noncomputable section
namespace ValuationTheory.DiscreteValuationField.DVF
universe u v
variable {K : Type u} [Field K] (base : DVF.{u, v} K)
local instance :
    (Valued.v : _root_.Valuation (WithVal base.valuation) base.ValueGroup).IsRankOneDiscrete :=
  Valuation.isRankOneDiscrete_comap_ringEquiv base.valuation (WithVal.equiv base.valuation)
local instance :
    (Valued.v : _root_.Valuation (WithVal base.valuation) base.ValueGroup).RankOne :=
  _root_.Valuation.IsRankOneDiscrete.rankOne
    (Valued.v : _root_.Valuation (WithVal base.valuation) base.ValueGroup)
    (e := 2) (by norm_num)
local instance : NontriviallyNormedField (WithVal base.valuation) :=
  Valued.toNontriviallyNormedField (WithVal base.valuation) base.ValueGroup
Lean source · statement
theorem normedWithVal_mem_valuationSubring_iff (x : WithVal base.valuation) :
    x ∈ (NormedField.valuation (K := WithVal base.valuation)).valuationSubring ↔
      WithVal.equiv base.valuation x ∈ base.valuation.valuationSubring
def

normedWithValValuationSubringEquiv

L53 ↗
ValuationTheory.DiscreteValuationField.DVF.normedWithValValuationSubringEquiv
Documentation

The normed WithVal model has the original valuation ring.

Its normed field structure is Valued.toNontriviallyNormedField, using Valuation.IsRankOneDiscrete.rankOne with base 2.

Source context 7 commands

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

noncomputable section
namespace ValuationTheory.DiscreteValuationField.DVF
universe u v
variable {K : Type u} [Field K] (base : DVF.{u, v} K)
local instance :
    (Valued.v : _root_.Valuation (WithVal base.valuation) base.ValueGroup).IsRankOneDiscrete :=
  Valuation.isRankOneDiscrete_comap_ringEquiv base.valuation (WithVal.equiv base.valuation)
local instance :
    (Valued.v : _root_.Valuation (WithVal base.valuation) base.ValueGroup).RankOne :=
  _root_.Valuation.IsRankOneDiscrete.rankOne
    (Valued.v : _root_.Valuation (WithVal base.valuation) base.ValueGroup)
    (e := 2) (by norm_num)
local instance : NontriviallyNormedField (WithVal base.valuation) :=
  Valued.toNontriviallyNormedField (WithVal base.valuation) base.ValueGroup
Lean source · full declaration
def normedWithValValuationSubringEquiv :
    (NormedField.valuation (K := WithVal base.valuation)).valuationSubring ≃+*
      base.valuationSubring where
  toFun x := ⟨WithVal.equiv base.valuation (x : WithVal base.valuation),
    (normedWithVal_mem_valuationSubring_iff base (x : WithVal base.valuation)).mp x.2⟩
  invFun y := ⟨(WithVal.equiv base.valuation).symm (y : K), by
    apply (normedWithVal_mem_valuationSubring_iff base
      ((WithVal.equiv base.valuation).symm (y : K))).mpr
    rw [RingEquiv.apply_symm_apply]
    exact y.2⟩
  left_inv x := Subtype.ext ((WithVal.equiv base.valuation).symm_apply_apply
    (x : WithVal base.valuation))
  right_inv y := Subtype.ext ((WithVal.equiv base.valuation).apply_symm_apply (y : K))
  map_mul' x y := Subtype.ext ((WithVal.equiv base.valuation).map_mul
    (x : WithVal base.valuation) (y : WithVal base.valuation))
  map_add' x y := Subtype.ext ((WithVal.equiv base.valuation).map_add
    (x : WithVal base.valuation) (y : WithVal base.valuation))
theorem

normedWithValValuationSubringEquiv_apply

L72 ↗
ValuationTheory.DiscreteValuationField.DVF.normedWithValValuationSubringEquiv_apply
Documentation

The valuation-ring equivalence is the restriction of WithVal.equiv.

Source context 7 commands

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

noncomputable section
namespace ValuationTheory.DiscreteValuationField.DVF
universe u v
variable {K : Type u} [Field K] (base : DVF.{u, v} K)
local instance :
    (Valued.v : _root_.Valuation (WithVal base.valuation) base.ValueGroup).IsRankOneDiscrete :=
  Valuation.isRankOneDiscrete_comap_ringEquiv base.valuation (WithVal.equiv base.valuation)
local instance :
    (Valued.v : _root_.Valuation (WithVal base.valuation) base.ValueGroup).RankOne :=
  _root_.Valuation.IsRankOneDiscrete.rankOne
    (Valued.v : _root_.Valuation (WithVal base.valuation) base.ValueGroup)
    (e := 2) (by norm_num)
local instance : NontriviallyNormedField (WithVal base.valuation) :=
  Valued.toNontriviallyNormedField (WithVal base.valuation) base.ValueGroup
Lean source · statement
theorem normedWithValValuationSubringEquiv_apply
    (x : (NormedField.valuation (K := WithVal base.valuation)).valuationSubring) :
    (normedWithValValuationSubringEquiv base x : K) =
      WithVal.equiv base.valuation (x : WithVal base.valuation)

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.