Module

SpectralExtension.lean

Nyll.ValuedFieldTheory.Valuation.AbsoluteValue.SpectralExtension

12 declarations indexed from sourceView source ↗

Module documentation

Spectral extensions of nonarchimedean absolute values

The spectral norm gives the unique extension of a complete nonarchimedean absolute value to an algebraic field extension.

Imports3

Nyll.ValuedFieldTheory.Valuation.AbsoluteValue.Extension
Nyll.ValuedFieldTheory.Valuation.AbsoluteValue.Nonarchimedean
Mathlib.Analysis.Normed.Unbundled.SpectralNorm

Imported by5

def

spectral_withAbsNontriviallyNormedField

L22 ↗

AbsoluteValue.spectral_withAbsNontriviallyNormedField

Source context 2 commands

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

noncomputable section
namespace AbsoluteValue

Lean source · statement

def spectral_withAbsNontriviallyNormedField
    {K : Type*} [Field K] (v : AbsoluteValue K ℝ) (hv : v.IsNontrivial) :
    NontriviallyNormedField (WithAbs v)

instance

withAbsAlgebra_isAlgebraic

L36 ↗

AbsoluteValue.withAbsAlgebra_isAlgebraic

Documentation

Algebraicity is transported across the canonical WithAbs base-field equivalence.

Source context 2 commands

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

noncomputable section
namespace AbsoluteValue

Lean source · statement

instance withAbsAlgebra_isAlgebraic
    {K L : Type*} [Field K] [Field L] [Algebra K L]
    [Algebra.IsAlgebraic K L] (v : AbsoluteValue K ℝ) :
    Algebra.IsAlgebraic (WithAbs v) L

theorem

withAbs_isUltrametricDist

L44 ↗

AbsoluteValue.withAbs_isUltrametricDist

Documentation

The strong triangle inequality on the induced normed-field structure.

Source context 2 commands

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

noncomputable section
namespace AbsoluteValue

Lean source · statement

theorem withAbs_isUltrametricDist
    {K : Type*} [Field K] (v : AbsoluteValue K ℝ)
    (hnonarch : IsNonarchimedean (v : K → ℝ)) :
    IsUltrametricDist (WithAbs v)

theorem

spectral_spectralNorm_extends_base

L55 ↗

AbsoluteValue.spectral_spectralNorm_extends_base

Documentation

existence branch: the spectral extension restricts to the given absolute value on the base field.

Source context 2 commands

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

noncomputable section
namespace AbsoluteValue

Lean source · statement

theorem spectral_spectralNorm_extends_base
    {K L : Type*} [Field K] [Field L] [Algebra K L]
    [Algebra.IsAlgebraic K L]
    (v : AbsoluteValue K ℝ) (x : K) :
    _root_.spectralNorm (WithAbs v) L (algebraMap K L x) = v x

theorem

spectral_spectralNorm_strong_triangle

L68 ↗

AbsoluteValue.spectral_spectralNorm_strong_triangle

Documentation

existence branch: the spectral extension satisfies the strong triangle inequality in the nonarchimedean case.

Source context 2 commands

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

noncomputable section
namespace AbsoluteValue

Lean source · statement

theorem spectral_spectralNorm_strong_triangle
    {K L : Type*} [Field K] [Field L] [Algebra K L]
    [Algebra.IsAlgebraic K L]
    (v : AbsoluteValue K ℝ)
    (hnonarch : IsNonarchimedean (v : K → ℝ)) (x y : L) :
    _root_.spectralNorm (WithAbs v) L (x + y) ≤
      max (_root_.spectralNorm (WithAbs v) L x)
        (_root_.spectralNorm (WithAbs v) L y)

theorem

spectral_spectralNorm_eq_zero_iff

L85 ↗

AbsoluteValue.spectral_spectralNorm_eq_zero_iff

Documentation

existence branch: the spectral extension vanishes exactly at zero.

Source context 2 commands

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

noncomputable section
namespace AbsoluteValue

Lean source · statement

theorem spectral_spectralNorm_eq_zero_iff
    {K L : Type*} [Field K] [Field L] [Algebra K L]
    [Algebra.IsAlgebraic K L]
    (v : AbsoluteValue K ℝ) (x : L) :
    _root_.spectralNorm (WithAbs v) L x = 0 ↔ x = 0

theorem

spectral_spectralNorm_mul

L103 ↗

AbsoluteValue.spectral_spectralNorm_mul

Documentation

existence branch: multiplicativity of the spectral extension over an algebraic extension.

Source context 2 commands

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

noncomputable section
namespace AbsoluteValue

Lean source · statement

theorem spectral_spectralNorm_mul
    {K L : Type*} [Field K] [Field L] [Algebra K L]
    [Algebra.IsAlgebraic K L]
    (v : AbsoluteValue K ℝ)
    (hcomplete : CompleteSpace (WithAbs v))
    (hnonarch : IsNonarchimedean (v : K → ℝ))
    (hv : v.IsNontrivial) (x y : L) :
    _root_.spectralNorm (WithAbs v) L (x * y) =
      _root_.spectralNorm (WithAbs v) L x *
        _root_.spectralNorm (WithAbs v) L y

def

spectralExtension

L128 ↗

AbsoluteValue.spectralExtension

Documentation

existence branch: the spectral norm, bundled as the unique nonarchimedean absolute-value extension of the complete base valuation.

Source context 2 commands

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

noncomputable section
namespace AbsoluteValue

Lean source · full declaration

def spectralExtension
    {K L : Type*} [Field K] [Field L] [Algebra K L]
    [Algebra.IsAlgebraic K L]
    (v : AbsoluteValue K ℝ)
    (hcomplete : CompleteSpace (WithAbs v))
    (hnonarch : IsNonarchimedean (v : K → ℝ))
    (hv : v.IsNontrivial) : AbsoluteValue L ℝ where
  toFun := _root_.spectralNorm (WithAbs v) L
  map_mul' x y :=
    spectral_spectralNorm_mul (K := K) (L := L)
      v hcomplete hnonarch hv x y
  nonneg' x := _root_.spectralNorm_nonneg (K := WithAbs v) (L := L) x
  eq_zero' x := spectral_spectralNorm_eq_zero_iff (K := K) (L := L) v x
  add_le' x y := by
    have hstrong :=
      spectral_spectralNorm_strong_triangle v hnonarch x y
    have hx_nonneg :
        0 ≤ _root_.spectralNorm (WithAbs v) L x :=
      _root_.spectralNorm_nonneg (K := WithAbs v) (L := L) x
    have hy_nonneg :
        0 ≤ _root_.spectralNorm (WithAbs v) L y :=
      _root_.spectralNorm_nonneg (K := WithAbs v) (L := L) y
    exact hstrong.trans
      (max_le
        (le_add_of_nonneg_right hy_nonneg)
        (le_add_of_nonneg_left hx_nonneg))

theorem

spectralExtension_isNonarchimedean

L157 ↗

AbsoluteValue.spectralExtension_isNonarchimedean

Documentation

The absolute-value extension constructed is nonarchimedean.

Source context 2 commands

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

noncomputable section
namespace AbsoluteValue

Lean source · statement

theorem spectralExtension_isNonarchimedean
    {K L : Type*} [Field K] [Field L] [Algebra K L]
    [Algebra.IsAlgebraic K L]
    (v : AbsoluteValue K ℝ)
    (hcomplete : CompleteSpace (WithAbs v))
    (hnonarch : IsNonarchimedean (v : K → ℝ))
    (hv : v.IsNontrivial) :
    IsNonarchimedean
      (spectralExtension (K := K) (L := L)
        v hcomplete hnonarch hv : L → ℝ)

theorem

spectralExtension_extends

L173 ↗

AbsoluteValue.spectralExtension_extends

Documentation

The absolute-value extension constructed restricts to the given base valuation.

Source context 2 commands

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

noncomputable section
namespace AbsoluteValue

Lean source · statement

theorem spectralExtension_extends
    {K L : Type*} [Field K] [Field L] [Algebra K L]
    [Algebra.IsAlgebraic K L]
    (v : AbsoluteValue K ℝ)
    (hcomplete : CompleteSpace (WithAbs v))
    (hnonarch : IsNonarchimedean (v : K → ℝ))
    (hv : v.IsNontrivial) :
    Extends v (spectralExtension (K := K) (L := L)
      v hcomplete hnonarch hv)

theorem

spectral_unique_spectralNorm

L185 ↗

AbsoluteValue.spectral_unique_spectralNorm

Documentation

Pointwise uniqueness of the spectral norm among extending absolute values.

Source context 2 commands

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

noncomputable section
namespace AbsoluteValue

Lean source · statement

theorem spectral_unique_spectralNorm
    {K L : Type*} [Field K] [Field L] [Algebra K L]
    [Algebra.IsAlgebraic K L]
    (v : AbsoluteValue K ℝ)
    (hcomplete : CompleteSpace (WithAbs v))
    (hnonarch : IsNonarchimedean (v : K → ℝ))
    (hv : v.IsNontrivial)
    (w : AbsoluteValue L ℝ)
    (hw_ext : Extends v w)
    (x : L) :
    w x = _root_.spectralNorm (WithAbs v) L x

theorem

eq_spectralExtension_of_extends

L214 ↗

AbsoluteValue.eq_spectralExtension_of_extends

Documentation

nonarchimedean complete branch: uniqueness of the absolute-value extension, stated as equality with the constructed extension.

Source context 2 commands

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

noncomputable section
namespace AbsoluteValue

Lean source · statement

theorem eq_spectralExtension_of_extends
    {K L : Type*} [Field K] [Field L] [Algebra K L]
    [Algebra.IsAlgebraic K L]
    (v : AbsoluteValue K ℝ)
    (hcomplete : CompleteSpace (WithAbs v))
    (hnonarch : IsNonarchimedean (v : K → ℝ))
    (hv : v.IsNontrivial)
    (w : AbsoluteValue L ℝ)
    (hw_ext : Extends v w) :
    w = spectralExtension (K := K) (L := L)
      v hcomplete hnonarch hv

Module documentation

Spectral extensions of nonarchimedean absolute values

Declarations