NYLL
Module

FiniteNormValuation.lean

Nyll.ValuedFieldTheory.Valuation.DiscreteValuationField.FiniteNormValuation
7 declarations indexed from sourceView source ↗

Module documentation

The field norm as a valuation on a finite extension

For a complete rank-one valued field, the field norm gives a valuation on any finite field extension. The strong triangle inequality follows from the actual spectral absolute-value extension. Separability is not needed.

Imports6
Imported by2

Declarations

theorem

normAbsoluteValue_complete

L30 ↗
ValuationTheory.DiscreteValuationField.ValuedExtension.normAbsoluteValue_complete
Source context 4 commands

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

noncomputable section
namespace ValuationTheory.DiscreteValuationField.ValuedExtension
open AlgebraicNumberTheory.Valuations
universe u v w
Lean source · statement
theorem normAbsoluteValue_complete
    (K : Type u) [NormedField K] [CompleteSpace K] :
    IsCompleteForAbsoluteValue (NormedField.toAbsoluteValue K)
theorem

valuation_norm_add_le_max

L54 ↗
ValuationTheory.DiscreteValuationField.ValuedExtension.valuation_norm_add_le_max
Documentation

The field norm satisfies the valuation triangle inequality over a complete rank-one valued base, including for inseparable finite extensions.

Source context 9 commands

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

noncomputable section
namespace ValuationTheory.DiscreteValuationField.ValuedExtension
open AlgebraicNumberTheory.Valuations
universe u v w
section General
variable {K : Type u} {L : Type w} [Field K] [Field L] [Algebra K L]
variable [FiniteDimensional K L]
variable {Γ : Type v} [LinearOrderedCommGroupWithZero Γ] [Valued K Γ]
variable [(Valued.v : _root_.Valuation K Γ).RankOne] [CompleteSpace K]
Lean source · statement
theorem valuation_norm_add_le_max (x y : L) :
    (Valued.v : _root_.Valuation K Γ) (Algebra.norm K (x + y)) ≤
      max (Valued.v (Algebra.norm K x)) (Valued.v (Algebra.norm K y))
def

finiteNormValuation

L85 ↗
ValuationTheory.DiscreteValuationField.ValuedExtension.finiteNormValuation
Documentation

The valuation obtained by applying the base valuation to the actual field norm. Its restriction is the degree-th power of the base valuation.

Source context 9 commands

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

noncomputable section
namespace ValuationTheory.DiscreteValuationField.ValuedExtension
open AlgebraicNumberTheory.Valuations
universe u v w
section General
variable {K : Type u} {L : Type w} [Field K] [Field L] [Algebra K L]
variable [FiniteDimensional K L]
variable {Γ : Type v} [LinearOrderedCommGroupWithZero Γ] [Valued K Γ]
variable [(Valued.v : _root_.Valuation K Γ).RankOne] [CompleteSpace K]
Lean source · full declaration
def finiteNormValuation : _root_.Valuation L Γ where
  toFun x := (Valued.v : _root_.Valuation K Γ) (Algebra.norm K x)
  map_zero' := by rw [Algebra.norm_zero, map_zero]
  map_one' := by rw [map_one, map_one]
  map_mul' x y := by rw [map_mul, map_mul]
  map_add_le_max' := valuation_norm_add_le_max
theorem

finiteNormValuation_algebraMap

L93 ↗
ValuationTheory.DiscreteValuationField.ValuedExtension.finiteNormValuation_algebraMap
Documentation

Restriction of the norm valuation to the base field.

Source context 9 commands

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

noncomputable section
namespace ValuationTheory.DiscreteValuationField.ValuedExtension
open AlgebraicNumberTheory.Valuations
universe u v w
section General
variable {K : Type u} {L : Type w} [Field K] [Field L] [Algebra K L]
variable [FiniteDimensional K L]
variable {Γ : Type v} [LinearOrderedCommGroupWithZero Γ] [Valued K Γ]
variable [(Valued.v : _root_.Valuation K Γ).RankOne] [CompleteSpace K]
Lean source · statement
theorem finiteNormValuation_algebraMap (x : K) :
    finiteNormValuation (K := K) (L := L) (Γ := Γ) (algebraMap K L x) =
      (Valued.v : _root_.Valuation K Γ) x ^ Module.finrank K L
theorem

finiteNormValuation_hasExtension

L101 ↗
ValuationTheory.DiscreteValuationField.ValuedExtension.finiteNormValuation_hasExtension
Documentation

The actual norm valuation extends the original valuation in the valuation-ring sense.

Source context 9 commands

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

noncomputable section
namespace ValuationTheory.DiscreteValuationField.ValuedExtension
open AlgebraicNumberTheory.Valuations
universe u v w
section General
variable {K : Type u} {L : Type w} [Field K] [Field L] [Algebra K L]
variable [FiniteDimensional K L]
variable {Γ : Type v} [LinearOrderedCommGroupWithZero Γ] [Valued K Γ]
variable [(Valued.v : _root_.Valuation K Γ).RankOne] [CompleteSpace K]
Lean source · statement
theorem finiteNormValuation_hasExtension :
    (Valued.v : _root_.Valuation K Γ).HasExtension
      (finiteNormValuation (K := K) (L := L) (Γ := Γ))
theorem

finiteNormValuation_isNontrivial

L114 ↗
ValuationTheory.DiscreteValuationField.ValuedExtension.finiteNormValuation_isNontrivial
Documentation

The norm valuation is nontrivial because its restriction is a positive power of the nontrivial base valuation.

Source context 9 commands

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

noncomputable section
namespace ValuationTheory.DiscreteValuationField.ValuedExtension
open AlgebraicNumberTheory.Valuations
universe u v w
section General
variable {K : Type u} {L : Type w} [Field K] [Field L] [Algebra K L]
variable [FiniteDimensional K L]
variable {Γ : Type v} [LinearOrderedCommGroupWithZero Γ] [Valued K Γ]
variable [(Valued.v : _root_.Valuation K Γ).RankOne] [CompleteSpace K]
Lean source · statement
theorem finiteNormValuation_isNontrivial :
    (finiteNormValuation (K := K) (L := L) (Γ := Γ)).IsNontrivial
theorem

finiteNormValuation_isRankOneDiscrete

L129 ↗
ValuationTheory.DiscreteValuationField.ValuedExtension.finiteNormValuation_isRankOneDiscrete
Documentation

In the integer-valued case the actual finite-extension norm valuation is discrete: its nonzero value group is a nontrivial subgroup of the integers.

Source context 4 commands

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

noncomputable section
namespace ValuationTheory.DiscreteValuationField.ValuedExtension
open AlgebraicNumberTheory.Valuations
universe u v w
Lean source · statement
theorem finiteNormValuation_isRankOneDiscrete
    {K : Type u} {L : Type w} [Field K] [Field L] [Algebra K L]
    [FiniteDimensional K L] [Valued K (WithZero (Multiplicative ℤ))]
    [(Valued.v : _root_.Valuation K (WithZero (Multiplicative ℤ))).RankOne]
    [CompleteSpace K] :
    (finiteNormValuation (K := K) (L := L)
      (Γ := WithZero (Multiplicative ℤ))).IsRankOneDiscrete

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