NYLL
Module

FiniteNormCompleteExtension.lean

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

Module documentation

Complete valuations on arbitrary finite extensions

The field norm constructs a discrete extension with the original value group. The complete absolute-value extension supplies adic completeness through its actual norm formula. Separability and residue-field perfection are not required.

Imports9
Imported by4

Declarations

theorem

completeSpace_of_completeDiscreteValuation

L32 ↗
ValuationTheory.DiscreteValuationField.ValuedExtension.completeSpace_of_completeDiscreteValuation
Documentation

Adic completeness of a discrete valuation ring implies completeness for its actual valuation uniformity, with an arbitrary ambient value group.

Source context 5 commands

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

noncomputable section
namespace ValuationTheory.DiscreteValuationField.ValuedExtension
open AlgebraicNumberTheory.Valuations
open scoped NNReal
universe u v w
Lean source · statement
theorem completeSpace_of_completeDiscreteValuation
    {F Γ : Type*} [Field F] [LinearOrderedCommGroupWithZero Γ]
    (v : _root_.Valuation F Γ) [Valuation.IsCompleteDiscrete v] :
    @CompleteSpace F (Valued.mk' v).toUniformSpace
theorem

finiteNormValuation_isRankOneDiscrete_general

L74 ↗
ValuationTheory.DiscreteValuationField.ValuedExtension.finiteNormValuation_isRankOneDiscrete_general
Documentation

The norm valuation takes values in the cyclic value group of the base.

Source context 9 commands

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

noncomputable section
namespace ValuationTheory.DiscreteValuationField.ValuedExtension
open AlgebraicNumberTheory.Valuations
open scoped NNReal
universe u v w
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_isRankOneDiscrete_general
    [(Valued.v : _root_.Valuation K Γ).IsRankOneDiscrete] :
    (finiteNormValuation (K := K) (L := L) (Γ := Γ)).IsRankOneDiscrete
theorem

normAbsoluteValue_complete

L87 ↗
ValuationTheory.DiscreteValuationField.ValuedExtension.normAbsoluteValue_complete
Source context 9 commands

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

noncomputable section
namespace ValuationTheory.DiscreteValuationField.ValuedExtension
open AlgebraicNumberTheory.Valuations
open scoped NNReal
universe u v w
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 normAbsoluteValue_complete
    (F : Type*) [NormedField F] [CompleteSpace F] :
    IsCompleteForAbsoluteValue (NormedField.toAbsoluteValue F)
theorem

finiteNormValuation_isCompleteDiscrete

L101 ↗
ValuationTheory.DiscreteValuationField.ValuedExtension.finiteNormValuation_isCompleteDiscrete
Documentation

Finite extensions carry a complete norm valuation, including inseparable extensions.

Source context 9 commands

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

noncomputable section
namespace ValuationTheory.DiscreteValuationField.ValuedExtension
open AlgebraicNumberTheory.Valuations
open scoped NNReal
universe u v w
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_isCompleteDiscrete
    [(Valued.v : _root_.Valuation K Γ).IsRankOneDiscrete] :
    Valuation.IsCompleteDiscrete
      (finiteNormValuation (K := K) (L := L) (Γ := Γ))
def

finiteExtension

L157 ↗
ValuationTheory.DiscreteValuationField.CompleteDVF.finiteExtension
Documentation

The complete norm valuation on an arbitrary finite field extension.

Source context 4 commands

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

noncomputable section
namespace ValuationTheory.DiscreteValuationField.CompleteDVF
universe u v w
variable {K : Type u} [Field K]
Lean source · statement
def finiteExtension (base : CompleteDVF.{u, v} K)
    (L : Type w) [Field L] [Algebra K L] [FiniteDimensional K L] :
    CompleteDVF.{w, v} L
theorem

finiteExtension_hasExtension

L172 ↗
ValuationTheory.DiscreteValuationField.CompleteDVF.finiteExtension_hasExtension
Documentation

The constructed complete valuation extends the original one.

Source context 4 commands

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

noncomputable section
namespace ValuationTheory.DiscreteValuationField.CompleteDVF
universe u v w
variable {K : Type u} [Field K]
Lean source · statement
theorem finiteExtension_hasExtension (base : CompleteDVF.{u, v} K)
    (L : Type w) [Field L] [Algebra K L] [FiniteDimensional K L] :
    base.valuation.HasExtension (base.finiteExtension L).valuation

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