Module

ValuedAdicComplete.lean

Nyll.ValuedFieldTheory.Valuation.ValuedAdicComplete

4 declarations indexed from sourceView source ↗

Module documentation

Adic completeness of complete rank-one discrete valued fields

This file supplies the common source used in the valuation-topology and adic-completeness arguments: on a rank-one discrete valued field, the native topology of the valuation ring is its maximal-ideal adic topology. Consequently a complete valued field has an adically complete valuation ring.

Imports5

Nyll.ValuedFieldTheory.Valuation.DiscreteValuationField.Complete
Mathlib.RingTheory.AdicCompletion.Topology
Mathlib.RingTheory.Valuation.Discrete.RankOne
Mathlib.GroupTheory.ArchimedeanDensely
Mathlib.Topology.Algebra.Valued.ValuedField

Imported by12

theorem

rankOneDiscreteValuationSubring_isDiscreteValuationRing

L35 ↗

ValuationTheory.Valuations.rankOneDiscreteValuationSubring_isDiscreteValuationRing

Documentation

The valuation ring of a rank-one discrete valued field is a discrete valuation ring.

Source context 5 commands

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

universe u v
namespace ValuationTheory
noncomputable section
namespace Valuations
open DiscreteValuationField

Lean source · statement

theorem rankOneDiscreteValuationSubring_isDiscreteValuationRing
    {K : Type u} [Field K] {Gamma : Type v}
    [LinearOrderedCommGroupWithZero Gamma]
    [Valued K Gamma]
    [(Valued.v : Valuation K Gamma).IsRankOneDiscrete] :
    IsDiscreteValuationRing
      (Valued.v : Valuation K Gamma).valuationSubring

theorem

rankOneDiscreteValuationSubring_isAdic

L49 ↗

ValuationTheory.Valuations.rankOneDiscreteValuationSubring_isAdic

Documentation

The native subtype topology on the valuation ring of a rank-one discrete valued field is its maximal-ideal adic topology.

Source context 5 commands

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

universe u v
namespace ValuationTheory
noncomputable section
namespace Valuations
open DiscreteValuationField

Lean source · statement

theorem rankOneDiscreteValuationSubring_isAdic
    {K : Type u} [Field K] {Gamma : Type v}
    [LinearOrderedCommGroupWithZero Gamma]
    [Valued K Gamma]
    [(Valued.v : Valuation K Gamma).IsRankOneDiscrete] :
    IsAdic
      (IsLocalRing.maximalIdeal
        (Valued.v : Valuation K Gamma).valuationSubring)

theorem

rankOneDiscreteValuationSubring_isAdicComplete

L120 ↗

ValuationTheory.Valuations.rankOneDiscreteValuationSubring_isAdicComplete

Documentation

Completeness of a rank-one discrete valued field produces adic completeness of its valuation ring; no adic-completeness assumption is exposed.

Source context 5 commands

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

universe u v
namespace ValuationTheory
noncomputable section
namespace Valuations
open DiscreteValuationField

Lean source · statement

theorem rankOneDiscreteValuationSubring_isAdicComplete
    {K : Type u} [Field K] {Gamma : Type v}
    [LinearOrderedCommGroupWithZero Gamma]
    [Valued K Gamma]
    [(Valued.v : Valuation K Gamma).IsRankOneDiscrete]
    [CompleteSpace K] :
    IsAdicComplete
      (IsLocalRing.maximalIdeal
        (Valued.v : Valuation K Gamma).valuationSubring)
      (Valued.v : Valuation K Gamma).valuationSubring

def

completeDVFOfCompleteValuedField

L142 ↗

ValuationTheory.Valuations.completeDVFOfCompleteValuedField

Documentation

A complete rank-one discrete valued field, equipped with its distinguished valuation, gives a CompleteDVF by construction.

Source context 5 commands

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

universe u v
namespace ValuationTheory
noncomputable section
namespace Valuations
open DiscreteValuationField

Lean source · full declaration

def completeDVFOfCompleteValuedField
    {K : Type u} [Field K] {Gamma : Type v}
    [LinearOrderedCommGroupWithZero Gamma]
    [Valued K Gamma]
    [(Valued.v : Valuation K Gamma).IsRankOneDiscrete]
    [CompleteSpace K] :
    CompleteDVF.{u, v} K where
  ValueGroup := Gamma
  valuation := Valued.v
  instCompleteDiscrete :=
    { isRankOneDiscrete := inferInstance
      isAdicComplete := rankOneDiscreteValuationSubring_isAdicComplete }

Module documentation

Adic completeness of complete rank-one discrete valued fields

Declarations

rankOneDiscreteValuationSubring_isDiscreteValuationRing

rankOneDiscreteValuationSubring_isAdic

rankOneDiscreteValuationSubring_isAdicComplete

completeDVFOfCompleteValuedField