Module

ExponentialValuation.lean

Nyll.ValuedFieldTheory.Valuation.AbsoluteValue.ExponentialValuation

6 declarations indexed from sourceView source ↗

Module documentation

Canonical exponential valuation attached to an absolute value

The localization arguments of the ramification-localization construction are naturally multiplicative, whereas the unramified predicates of the unramified-extension construction use additive exponential valuations. This file supplies the canonical conversion v(x) = -log |x|.

Imports1

Nyll.ValuedFieldTheory.LocalField.Unramified.HenselianAlgebraicExtension

Imported by6

def

absoluteValueExponentialValuation

L27 ↗

AlgebraicNumberTheory.Valuations.absoluteValueExponentialValuation

Documentation

The additive exponential valuation - log |x|, with value ∞ at zero.

Source context 4 commands

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

noncomputable section
namespace AlgebraicNumberTheory
namespace Valuations
variable {K : Type*} [Field K]

Lean source · statement

def absoluteValueExponentialValuation
    (abv : AbsoluteValue K ℝ) (hnonarch : LubinTate.Valuations.NonarchimedeanAbsoluteValue abv) :
    LubinTate.Valuations.ExponentialValuation K

theorem

absoluteValueExponentialValuation_apply_ne_zero

L80 ↗

AlgebraicNumberTheory.Valuations.absoluteValueExponentialValuation_apply_ne_zero

Source context 4 commands

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

noncomputable section
namespace AlgebraicNumberTheory
namespace Valuations
variable {K : Type*} [Field K]

Lean source · statement

theorem absoluteValueExponentialValuation_apply_ne_zero
    (abv : AbsoluteValue K ℝ) (hnonarch : LubinTate.Valuations.NonarchimedeanAbsoluteValue abv)
    {x : K} (hx : x ≠ 0) :
    absoluteValueExponentialValuation abv hnonarch x =
      ((-Real.log (abv x) : ℝ) : WithTop ℝ)

theorem

absoluteValueExponentialValuation_associated

L89 ↗

AlgebraicNumberTheory.Valuations.absoluteValueExponentialValuation_associated

Documentation

The original absolute value is associated to its canonical exponential valuation, with base e.

Source context 4 commands

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

noncomputable section
namespace AlgebraicNumberTheory
namespace Valuations
variable {K : Type*} [Field K]

Lean source · statement

theorem absoluteValueExponentialValuation_associated
    (abv : AbsoluteValue K ℝ) (hnonarch : LubinTate.Valuations.NonarchimedeanAbsoluteValue abv) :
    LubinTate.Valuations.AssociatedAbsoluteValue
      (absoluteValueExponentialValuation abv hnonarch)
      (Real.exp 1) abv

theorem

exponentialValuation_ext

L103 ↗

AlgebraicNumberTheory.Valuations.exponentialValuation_ext

Documentation

Extensionality for exponential valuations.

Source context 4 commands

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

noncomputable section
namespace AlgebraicNumberTheory
namespace Valuations
variable {K : Type*} [Field K]

Lean source · statement

theorem exponentialValuation_ext
    (v w : LubinTate.Valuations.ExponentialValuation K) (h : ∀ x, v x = w x) : v = w

theorem

absoluteValueExponentialValuation_associated_eq

L115 ↗

AlgebraicNumberTheory.Valuations.absoluteValueExponentialValuation_associated_eq

Documentation

Converting the canonical associated absolute value back by -log recovers the original exponential valuation literally.

Source context 4 commands

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

noncomputable section
namespace AlgebraicNumberTheory
namespace Valuations
variable {K : Type*} [Field K]

Lean source · statement

theorem absoluteValueExponentialValuation_associated_eq
    (v : LubinTate.Valuations.ExponentialValuation K) :
    absoluteValueExponentialValuation
        (exponentialAssociatedAbsoluteValue v)
        (associatedAbsoluteValue_nonarchimedean v (Real.exp 1)
          (exponentialAssociatedAbsoluteValue v)
          (exponentialAssociatedAbsoluteValue_associated v)) = v

theorem

absoluteValueExponentialValuation_extends

L135 ↗

AlgebraicNumberTheory.Valuations.absoluteValueExponentialValuation_extends

Documentation

Exact extension of nonarchimedean absolute values gives exact extension of their canonical exponential valuations.

Source context 4 commands

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

noncomputable section
namespace AlgebraicNumberTheory
namespace Valuations
variable {K : Type*} [Field K]

Lean source · statement

theorem absoluteValueExponentialValuation_extends
    {L : Type*} [Field L] [Algebra K L]
    (av : AbsoluteValue K ℝ) (aw : AbsoluteValue L ℝ)
    (hav : LubinTate.Valuations.NonarchimedeanAbsoluteValue av)
    (haw : LubinTate.Valuations.NonarchimedeanAbsoluteValue aw)
    (hExt : ∀ x : K, aw (algebraMap K L x) = av x) :
    ∀ x : K,
      absoluteValueExponentialValuation aw haw (algebraMap K L x) =
        absoluteValueExponentialValuation av hav x

Module documentation

Canonical exponential valuation attached to an absolute value

Declarations

absoluteValueExponentialValuation

absoluteValueExponentialValuation_apply_ne_zero

absoluteValueExponentialValuation_associated

exponentialValuation_ext

absoluteValueExponentialValuation_associated_eq

absoluteValueExponentialValuation_extends