Module

Completeness.lean

Nyll.ValuedFieldTheory.Valuation.AbsoluteValue.Completeness

8 declarations indexed from sourceView source ↗

Module documentation

Minimal absolute-value norm API

This file keeps only the lightweight explicit definitions used by the current Section 4 formalization. The old experimental completion and norm formula development was removed because it duplicated mathlib APIs and no longer compiled.

Imports4

Mathlib.Analysis.Normed.Field.WithAbs
Mathlib.Analysis.SpecialFunctions.Pow.Real
Mathlib.RingTheory.Norm.Defs
Mathlib.Topology.UniformSpace.AbsoluteValue

Imported by8

def

IsCompleteForAbsoluteValue

L28 ↗

AlgebraicNumberTheory.Valuations.IsCompleteForAbsoluteValue

Documentation

A valued field is complete if it is complete for the uniformity induced by its absolute value.

Source context 3 commands

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

noncomputable section
namespace AlgebraicNumberTheory
namespace Valuations

Lean source · statement

def IsCompleteForAbsoluteValue {K : Type*} [Field K] (v : AbsoluteValue K ℝ) : Prop

theorem

absoluteValue_uniformSpace_eq_toNormedField

L34 ↗

AlgebraicNumberTheory.Valuations.absoluteValue_uniformSpace_eq_toNormedField

Documentation

The uniformity attached directly to an absolute value agrees with the uniformity coming from the normed-field structure induced by that absolute value.

Source context 3 commands

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

noncomputable section
namespace AlgebraicNumberTheory
namespace Valuations

Lean source · statement

theorem absoluteValue_uniformSpace_eq_toNormedField
    {K : Type*} [Field K] (v : AbsoluteValue K ℝ) :
    v.uniformSpace = (AbsoluteValue.toNormedField v).toUniformSpace

theorem

absoluteValueCompleteness_completeSpace_withAbs_iff_complete

L49 ↗

AlgebraicNumberTheory.Valuations.absoluteValueCompleteness_completeSpace_withAbs_iff_complete

Documentation

Completeness in the absolute-value uniformity is the same as completeness of the corresponding WithAbs normed field.

Source context 3 commands

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

noncomputable section
namespace AlgebraicNumberTheory
namespace Valuations

Lean source · statement

theorem absoluteValueCompleteness_completeSpace_withAbs_iff_complete
    {K : Type*} [Field K] (v : AbsoluteValue K ℝ) :
    CompleteSpace (WithAbs v) ↔ IsCompleteForAbsoluteValue v

theorem

completeSpace_withAbs_of_isCompleteForAbsoluteValue

L68 ↗

AlgebraicNumberTheory.Valuations.completeSpace_withAbs_of_isCompleteForAbsoluteValue

Documentation

A complete valued field is complete as the corresponding WithAbs normed field.

Source context 3 commands

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

noncomputable section
namespace AlgebraicNumberTheory
namespace Valuations

Lean source · statement

theorem completeSpace_withAbs_of_isCompleteForAbsoluteValue
    {K : Type*} [Field K] (v : AbsoluteValue K ℝ)
    (hcomplete : IsCompleteForAbsoluteValue v) :
    CompleteSpace (WithAbs v)

theorem

absoluteValueCompleteness_complete_iff_cauchySeq_converges

L76 ↗

AlgebraicNumberTheory.Valuations.absoluteValueCompleteness_complete_iff_cauchySeq_converges

Documentation

Sequence form of the sequential completeness criterion: a complete valued field is exactly one where every Cauchy sequence in the absolute-value topology converges.

Source context 3 commands

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

noncomputable section
namespace AlgebraicNumberTheory
namespace Valuations

Lean source · statement

theorem absoluteValueCompleteness_complete_iff_cauchySeq_converges
    {K : Type*} [Field K] (v : AbsoluteValue K ℝ) :
    IsCompleteForAbsoluteValue v ↔
      ∀ u : ℕ → WithAbs v, CauchySeq u →
        ∃ a : WithAbs v, Filter.Tendsto u Filter.atTop (nhds a)

def

withAbsNontriviallyNormedField

L93 ↗

AlgebraicNumberTheory.Valuations.withAbsNontriviallyNormedField

Documentation

The nontrivial-valuation convention excludes the trivial valuation; this supplies the corresponding mathlib NontriviallyNormedField instance for WithAbs v.

Source context 3 commands

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

noncomputable section
namespace AlgebraicNumberTheory
namespace Valuations

Lean source · statement

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

def

finiteExtensionNormFormulaValue

L107 ↗

AlgebraicNumberTheory.Valuations.finiteExtensionNormFormulaValue

Documentation

The finite-degree norm-formula candidate: x ↦ |N_{L/K}(x)|^{1/[L:K]}.

Source context 3 commands

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

noncomputable section
namespace AlgebraicNumberTheory
namespace Valuations

Lean source · statement

def finiteExtensionNormFormulaValue
    {K L : Type*} [Field K] [Field L] [Algebra K L] [FiniteDimensional K L]
    (v : AbsoluteValue K ℝ) (x : L) : ℝ

theorem

finiteExtensionNormFormulaValue_nonneg

L113 ↗

AlgebraicNumberTheory.Valuations.finiteExtensionNormFormulaValue_nonneg

Documentation

The finite-degree norm formula candidate is nonnegative.

Source context 3 commands

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

noncomputable section
namespace AlgebraicNumberTheory
namespace Valuations

Lean source · statement

theorem finiteExtensionNormFormulaValue_nonneg
    {K L : Type*} [Field K] [Field L] [Algebra K L] [FiniteDimensional K L]
    (v : AbsoluteValue K ℝ) (x : L) :
    0 ≤ finiteExtensionNormFormulaValue v x

Module documentation

Minimal absolute-value norm API

Declarations