NYLL
Module

AbsoluteCompletion.lean

Nyll.EtaleFundamentalGroups.Completions.StandardDVF.AbsoluteCompletion
21 declarations indexed from sourceView source ↗

Module documentation

Absolute-value and valued-field completions of a DVR fraction field

The standard height-one valuation of a DVR gives two concrete completion models: the completion of its fixed real-valued adic absolute value, and the valued-field completion used by standardDVFCompletionField. This file constructs the canonical K-algebra equivalence between them.

The map is obtained by extending the identity on K. Its surjectivity is proved from density of K in the valued-field completion and closedness of the image of an isometry; it is not supplied as an assumption.

Imports4
Imported by1

Declarations

def

standardDVRAbsoluteValueScale

L36 ↗
EtaleFundamentalGroups.standardDVRAbsoluteValueScale
Documentation

The fixed scale used to turn every standard DVR valuation into a real absolute value.

Source context 5 commands

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

noncomputable section
open scoped NNReal Valued
open IsDedekindDomain
namespace EtaleFundamentalGroups
universe uV uK
Lean source · statement
def standardDVRAbsoluteValueScale : ℝ≥0
theorem

standardDVRAbsoluteValueScale_one_lt

L38 ↗
EtaleFundamentalGroups.standardDVRAbsoluteValueScale_one_lt
Source context 5 commands

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

noncomputable section
open scoped NNReal Valued
open IsDedekindDomain
namespace EtaleFundamentalGroups
universe uV uK
Lean source · statement
theorem standardDVRAbsoluteValueScale_one_lt :
    1 < standardDVRAbsoluteValueScale
def

standardDVRAbsoluteValue

L44 ↗
EtaleFundamentalGroups.standardDVRAbsoluteValue
Documentation

The standard real-valued absolute value attached to a DVR, with the globally fixed scale 2.

Source context 5 commands

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

noncomputable section
open scoped NNReal Valued
open IsDedekindDomain
namespace EtaleFundamentalGroups
universe uV uK
Lean source · statement
def standardDVRAbsoluteValue
    (V : Type uV) (K : Type uK)
    [CommRing V] [IsDomain V] [IsDiscreteValuationRing V]
    [Field K] [Algebra V K] [IsFractionRing V K] :
    AbsoluteValue K ℝ
theorem

standardDVRAbsoluteValue_apply

L54 ↗
EtaleFundamentalGroups.standardDVRAbsoluteValue_apply
Documentation

The fixed absolute value is the strictly monotone real presentation of the standard multiplicative DVR valuation.

Source context 5 commands

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

noncomputable section
open scoped NNReal Valued
open IsDedekindDomain
namespace EtaleFundamentalGroups
universe uV uK
Lean source · statement
theorem standardDVRAbsoluteValue_apply
    (V : Type uV) (K : Type uK)
    [CommRing V] [IsDomain V] [IsDiscreteValuationRing V]
    [Field K] [Algebra V K] [IsFractionRing V K]
    (x : K) :
    standardDVRAbsoluteValue V K x =
      WithZeroMulInt.toNNReal
        (ne_zero_of_lt standardDVRAbsoluteValueScale_one_lt)
        ((IsDiscreteValuationRing.maximalIdeal V).valuation K x)
theorem

standardDVRAbsoluteValue_isNontrivial

L66 ↗
EtaleFundamentalGroups.standardDVRAbsoluteValue_isNontrivial
Documentation

The standard DVR absolute value is nontrivial.

Source context 5 commands

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

noncomputable section
open scoped NNReal Valued
open IsDedekindDomain
namespace EtaleFundamentalGroups
universe uV uK
Lean source · statement
theorem standardDVRAbsoluteValue_isNontrivial
    (V : Type uV) (K : Type uK)
    [CommRing V] [IsDomain V] [IsDiscreteValuationRing V]
    [Field K] [Algebra V K] [IsFractionRing V K] :
    (standardDVRAbsoluteValue V K).IsNontrivial
def

standardDVRAbsoluteCompletionBaseMap

L82 ↗
EtaleFundamentalGroups.standardDVRAbsoluteCompletionBaseMap
Documentation

The canonical map from the absolute-valued copy of K to the valued completion of the standard DVR valuation.

Source context 5 commands

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

noncomputable section
open scoped NNReal Valued
open IsDedekindDomain
namespace EtaleFundamentalGroups
universe uV uK
Lean source · statement
def standardDVRAbsoluteCompletionBaseMap
    (V : Type uV) (K : Type uK)
    [CommRing V] [IsDomain V] [IsDiscreteValuationRing V]
    [Field K] [Algebra V K] [IsFractionRing V K] :
    WithAbs (standardDVRAbsoluteValue V K) →+*
      standardDVFCompletionField V K
theorem

standardDVRAbsoluteCompletionBaseMap_apply

L92 ↗
EtaleFundamentalGroups.standardDVRAbsoluteCompletionBaseMap_apply
Source context 5 commands

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

noncomputable section
open scoped NNReal Valued
open IsDedekindDomain
namespace EtaleFundamentalGroups
universe uV uK
Lean source · statement
theorem standardDVRAbsoluteCompletionBaseMap_apply
    (V : Type uV) (K : Type uK)
    [CommRing V] [IsDomain V] [IsDiscreteValuationRing V]
    [Field K] [Algebra V K] [IsFractionRing V K]
    (x : WithAbs (standardDVRAbsoluteValue V K)) :
    standardDVRAbsoluteCompletionBaseMap V K x =
      standardDVFCompletionMap V K
        (WithAbs.equiv (standardDVRAbsoluteValue V K) x)
theorem

standardDVFCompletionIsRankOneDiscrete

L103 ↗
EtaleFundamentalGroups.standardDVFCompletionIsRankOneDiscrete
Documentation

The completed valuation is still discrete rank one.

Source context 5 commands

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

noncomputable section
open scoped NNReal Valued
open IsDedekindDomain
namespace EtaleFundamentalGroups
universe uV uK
Lean source · statement
theorem standardDVFCompletionIsRankOneDiscrete
    (V : Type uV) (K : Type uK)
    [CommRing V] [IsDomain V] [IsDiscreteValuationRing V]
    [Field K] [Algebra V K] [IsFractionRing V K] :
    (Valued.v : Valuation (standardDVFCompletionField V K)
      (WithZero (Multiplicative ℤ))).IsRankOneDiscrete
def

standardDVRAbsoluteCompletionRankOne

L116 ↗
EtaleFundamentalGroups.standardDVRAbsoluteCompletionRankOne
Documentation

The rank-one structure on the completed valuation, normalized with the same scale as standardDVRAbsoluteValue.

Source context 5 commands

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

noncomputable section
open scoped NNReal Valued
open IsDedekindDomain
namespace EtaleFundamentalGroups
universe uV uK
Lean source · statement
def standardDVRAbsoluteCompletionRankOne
    (V : Type uV) (K : Type uK)
    [CommRing V] [IsDomain V] [IsDiscreteValuationRing V]
    [Field K] [Algebra V K] [IsFractionRing V K] :
    (Valued.v : Valuation (standardDVFCompletionField V K)
      (WithZero (Multiplicative ℤ))).RankOne
theorem

standardDVRAbsoluteCompletionRankOne_hom'_eq

L130 ↗
EtaleFundamentalGroups.standardDVRAbsoluteCompletionRankOne_hom'_eq
Source context 5 commands

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

noncomputable section
open scoped NNReal Valued
open IsDedekindDomain
namespace EtaleFundamentalGroups
universe uV uK
Lean source · full declaration
theorem standardDVRAbsoluteCompletionRankOne_hom'_eq
    (V : Type uV) (K : Type uK)
    [CommRing V] [IsDomain V] [IsDiscreteValuationRing V]
    [Field K] [Algebra V K] [IsFractionRing V K] :
    letI : (Valued.v : Valuation (standardDVFCompletionField V K)
        (WithZero (Multiplicative ℤ))).IsRankOneDiscrete :=
      standardDVFCompletionIsRankOneDiscrete V K
    (standardDVRAbsoluteCompletionRankOne V K).hom' =
        (WithZeroMulInt.toNNReal
          (ne_zero_of_lt standardDVRAbsoluteValueScale_one_lt)).comp
          (Valuation.IsRankOneDiscrete.valueGroup₀_equiv_withZeroMulInt
            (Valued.v : Valuation (standardDVFCompletionField V K)
              (WithZero (Multiplicative ℤ)))).toMonoidWithZeroHom := by
  let : (Valued.v : Valuation (standardDVFCompletionField V K)
      (WithZero (Multiplicative ℤ))).IsRankOneDiscrete :=
    standardDVFCompletionIsRankOneDiscrete V K
  rfl
theorem

standardDVFCompletionValuation_surjective

L149 ↗
EtaleFundamentalGroups.standardDVFCompletionValuation_surjective
Documentation

The completed standard valuation is onto its normalized value group.

Source context 5 commands

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

noncomputable section
open scoped NNReal Valued
open IsDedekindDomain
namespace EtaleFundamentalGroups
universe uV uK
Lean source · statement
theorem standardDVFCompletionValuation_surjective
    (V : Type uV) (K : Type uK)
    [CommRing V] [IsDomain V] [IsDiscreteValuationRing V]
    [Field K] [Algebra V K] [IsFractionRing V K] :
    Function.Surjective
      (Valued.v : standardDVFCompletionField V K →
        WithZero (Multiplicative ℤ))
theorem

standardDVRAbsoluteCompletionBaseMap_norm

L161 ↗
EtaleFundamentalGroups.standardDVRAbsoluteCompletionBaseMap_norm
Documentation

With the common normalization, the dense base map is an isometry.

Source context 5 commands

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

noncomputable section
open scoped NNReal Valued
open IsDedekindDomain
namespace EtaleFundamentalGroups
universe uV uK
Lean source · full declaration
theorem standardDVRAbsoluteCompletionBaseMap_norm
    (V : Type uV) (K : Type uK)
    [CommRing V] [IsDomain V] [IsDiscreteValuationRing V]
    [Field K] [Algebra V K] [IsFractionRing V K]
    (x : WithAbs (standardDVRAbsoluteValue V K)) :
    letI : (Valued.v : Valuation (standardDVFCompletionField V K)
        (WithZero (Multiplicative ℤ))).RankOne :=
      standardDVRAbsoluteCompletionRankOne V K
    ‖standardDVRAbsoluteCompletionBaseMap V K x‖ = ‖x‖ := by
  let v := (IsDiscreteValuationRing.maximalIdeal V).valuation K
  let : (Valued.v : Valuation (standardDVFCompletionField V K)
      (WithZero (Multiplicative ℤ))).IsRankOneDiscrete :=
    standardDVFCompletionIsRankOneDiscrete V K
  let : (Valued.v : Valuation (standardDVFCompletionField V K)
      (WithZero (Multiplicative ℤ))).RankOne :=
    standardDVRAbsoluteCompletionRankOne V K
  rw [standardDVRAbsoluteCompletionBaseMap_apply]
  change
    (((standardDVRAbsoluteCompletionRankOne V K).hom'
      ((Valued.v : Valuation v.Completion (WithZero (Multiplicative ℤ))).restrict
        (standardDVFCompletionMap V K
          (WithAbs.equiv (standardDVRAbsoluteValue V K) x))) : ℝ≥0) : ℝ) =
      standardDVRAbsoluteValue V K
        (WithAbs.equiv (standardDVRAbsoluteValue V K) x)
  rw [standardDVRAbsoluteCompletionRankOne_hom'_eq]
  change
    ((WithZeroMulInt.toNNReal
      (ne_zero_of_lt standardDVRAbsoluteValueScale_one_lt)
      ((Valuation.IsRankOneDiscrete.valueGroup₀_equiv_withZeroMulInt
        (Valued.v : Valuation v.Completion (WithZero (Multiplicative ℤ))))
        ((Valued.v : Valuation v.Completion
          (WithZero (Multiplicative ℤ))).restrict
          (standardDVFCompletionMap V K
            (WithAbs.equiv (standardDVRAbsoluteValue V K) x)))) : ℝ≥0) : ℝ) = _
  rw [Valuation.IsRankOneDiscrete.valueGroup₀_equiv_withZeroMulInt_restrict_apply_of_surjective
      (standardDVFCompletionValuation_surjective V K)
      (standardDVFCompletionMap V K
        (WithAbs.equiv (standardDVRAbsoluteValue V K) x))]
  rw [show (Valued.v : Valuation v.Completion
      (WithZero (Multiplicative ℤ)))
        (standardDVFCompletionMap V K
          (WithAbs.equiv (standardDVRAbsoluteValue V K) x)) =
      v (WithAbs.equiv (standardDVRAbsoluteValue V K) x) by
    change (Valued.v : Valuation v.Completion
      (WithZero (Multiplicative ℤ)))
        (((WithVal.equiv v).symm
          (WithAbs.equiv (standardDVRAbsoluteValue V K) x) : WithVal v) :
            v.Completion) = _
    rw [Valued.valuedCompletion_apply]
    rfl]
  rw [standardDVRAbsoluteValue_apply]
theorem

standardDVRAbsoluteCompletionBaseMap_isometry

L213 ↗
EtaleFundamentalGroups.standardDVRAbsoluteCompletionBaseMap_isometry
Source context 5 commands

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

noncomputable section
open scoped NNReal Valued
open IsDedekindDomain
namespace EtaleFundamentalGroups
universe uV uK
Lean source · full declaration
theorem standardDVRAbsoluteCompletionBaseMap_isometry
    (V : Type uV) (K : Type uK)
    [CommRing V] [IsDomain V] [IsDiscreteValuationRing V]
    [Field K] [Algebra V K] [IsFractionRing V K] :
    letI : (Valued.v : Valuation (standardDVFCompletionField V K)
        (WithZero (Multiplicative ℤ))).RankOne :=
      standardDVRAbsoluteCompletionRankOne V K
    Isometry (standardDVRAbsoluteCompletionBaseMap V K) := by
  let : (Valued.v : Valuation (standardDVFCompletionField V K)
      (WithZero (Multiplicative ℤ))).RankOne :=
    standardDVRAbsoluteCompletionRankOne V K
  exact AddMonoidHomClass.isometry_of_norm _
    (standardDVRAbsoluteCompletionBaseMap_norm V K)
def

standardDVRAbsoluteCompletionRingHom

L229 ↗
EtaleFundamentalGroups.standardDVRAbsoluteCompletionRingHom
Documentation

Extension of the canonical dense base map to the absolute-value completion.

Source context 5 commands

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

noncomputable section
open scoped NNReal Valued
open IsDedekindDomain
namespace EtaleFundamentalGroups
universe uV uK
Lean source · statement
def standardDVRAbsoluteCompletionRingHom
    (V : Type uV) (K : Type uK)
    [CommRing V] [IsDomain V] [IsDiscreteValuationRing V]
    [Field K] [Algebra V K] [IsFractionRing V K] :
    (standardDVRAbsoluteValue V K).Completion →+*
      standardDVFCompletionField V K
theorem

standardDVRAbsoluteCompletionRingHom_coe

L243 ↗
EtaleFundamentalGroups.standardDVRAbsoluteCompletionRingHom_coe
Source context 5 commands

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

noncomputable section
open scoped NNReal Valued
open IsDedekindDomain
namespace EtaleFundamentalGroups
universe uV uK
Lean source · statement
theorem standardDVRAbsoluteCompletionRingHom_coe
    (V : Type uV) (K : Type uK)
    [CommRing V] [IsDomain V] [IsDiscreteValuationRing V]
    [Field K] [Algebra V K] [IsFractionRing V K]
    (x : WithAbs (standardDVRAbsoluteValue V K)) :
    standardDVRAbsoluteCompletionRingHom V K
        (x : (standardDVRAbsoluteValue V K).Completion) =
      standardDVRAbsoluteCompletionBaseMap V K x
theorem

standardDVRAbsoluteCompletionRingHom_isometry

L258 ↗
EtaleFundamentalGroups.standardDVRAbsoluteCompletionRingHom_isometry
Source context 5 commands

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

noncomputable section
open scoped NNReal Valued
open IsDedekindDomain
namespace EtaleFundamentalGroups
universe uV uK
Lean source · full declaration
theorem standardDVRAbsoluteCompletionRingHom_isometry
    (V : Type uV) (K : Type uK)
    [CommRing V] [IsDomain V] [IsDiscreteValuationRing V]
    [Field K] [Algebra V K] [IsFractionRing V K] :
    letI : (Valued.v : Valuation (standardDVFCompletionField V K)
        (WithZero (Multiplicative ℤ))).RankOne :=
      standardDVRAbsoluteCompletionRankOne V K
    Isometry (standardDVRAbsoluteCompletionRingHom V K) := by
  let : (Valued.v : Valuation (standardDVFCompletionField V K)
      (WithZero (Multiplicative ℤ))).RankOne :=
    standardDVRAbsoluteCompletionRankOne V K
  exact (standardDVRAbsoluteCompletionBaseMap_isometry V K).completion_extension
theorem

standardDVFCompletionMap_denseRange

L272 ↗
EtaleFundamentalGroups.standardDVFCompletionMap_denseRange
Documentation

The canonical copy of K is dense in the valued-field completion.

Source context 5 commands

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

noncomputable section
open scoped NNReal Valued
open IsDedekindDomain
namespace EtaleFundamentalGroups
universe uV uK
Lean source · statement
theorem standardDVFCompletionMap_denseRange
    (V : Type uV) (K : Type uK)
    [CommRing V] [IsDomain V] [IsDiscreteValuationRing V]
    [Field K] [Algebra V K] [IsFractionRing V K] :
    DenseRange (standardDVFCompletionMap V K)
theorem

standardDVRAbsoluteCompletionRingHom_surjective

L288 ↗
EtaleFundamentalGroups.standardDVRAbsoluteCompletionRingHom_surjective
Documentation

The extended map is onto, by density of the base field and closedness of the image of an isometry.

Source context 5 commands

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

noncomputable section
open scoped NNReal Valued
open IsDedekindDomain
namespace EtaleFundamentalGroups
universe uV uK
Lean source · statement
theorem standardDVRAbsoluteCompletionRingHom_surjective
    (V : Type uV) (K : Type uK)
    [CommRing V] [IsDomain V] [IsDiscreteValuationRing V]
    [Field K] [Algebra V K] [IsFractionRing V K] :
    Function.Surjective (standardDVRAbsoluteCompletionRingHom V K)
def

standardDVRAbsoluteCompletionRingEquiv

L316 ↗
EtaleFundamentalGroups.standardDVRAbsoluteCompletionRingEquiv
Documentation

Canonical ring equivalence between the absolute-value completion and the valued-field completion of the standard DVR valuation.

Source context 5 commands

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

noncomputable section
open scoped NNReal Valued
open IsDedekindDomain
namespace EtaleFundamentalGroups
universe uV uK
Lean source · statement
def standardDVRAbsoluteCompletionRingEquiv
    (V : Type uV) (K : Type uK)
    [CommRing V] [IsDomain V] [IsDiscreteValuationRing V]
    [Field K] [Algebra V K] [IsFractionRing V K] :
    (standardDVRAbsoluteValue V K).Completion ≃+*
      standardDVFCompletionField V K
theorem

standardDVRAbsoluteCompletionRingEquiv_algebraMap

L333 ↗
EtaleFundamentalGroups.standardDVRAbsoluteCompletionRingEquiv_algebraMap
Documentation

The comparison is the identity on the dense copy of K.

Source context 5 commands

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

noncomputable section
open scoped NNReal Valued
open IsDedekindDomain
namespace EtaleFundamentalGroups
universe uV uK
Lean source · statement
theorem standardDVRAbsoluteCompletionRingEquiv_algebraMap
    (V : Type uV) (K : Type uK)
    [CommRing V] [IsDomain V] [IsDiscreteValuationRing V]
    [Field K] [Algebra V K] [IsFractionRing V K]
    (x : K) :
    standardDVRAbsoluteCompletionRingEquiv V K
        (algebraMap K (standardDVRAbsoluteValue V K).Completion x) =
      standardDVFCompletionMap V K x
def

standardDVRAbsoluteCompletionAlgEquiv

L350 ↗
EtaleFundamentalGroups.standardDVRAbsoluteCompletionAlgEquiv
Documentation

The absolute-value completion and the standard valued-field completion are canonically equivalent as K-algebras.

Source context 5 commands

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

noncomputable section
open scoped NNReal Valued
open IsDedekindDomain
namespace EtaleFundamentalGroups
universe uV uK
Lean source · full declaration
def standardDVRAbsoluteCompletionAlgEquiv
    (V : Type uV) (K : Type uK)
    [CommRing V] [IsDomain V] [IsDiscreteValuationRing V]
    [Field K] [Algebra V K] [IsFractionRing V K] :
    letI : Algebra K (standardDVFCompletionField V K) :=
      standardDVFCompletionAlgebra V K
    (standardDVRAbsoluteValue V K).Completion ≃ₐ[K]
      standardDVFCompletionField V K := by
  letI : Algebra K (standardDVFCompletionField V K) :=
    standardDVFCompletionAlgebra V K
  exact
    { __ := standardDVRAbsoluteCompletionRingEquiv V K
      commutes' := standardDVRAbsoluteCompletionRingEquiv_algebraMap V K }

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