Module

Complete.lean

Nyll.EtaleFundamentalGroups.Completions.StandardDVF.Complete

2 declarations indexed from sourceView source ↗

Module documentation

The standard complete discrete valuation field attached to a complete DVR

The standard rank-one valuation attached to a DVR becomes a CompleteDVF when the DVR is complete for its maximal-ideal-adic topology. This is the base object needed to apply the finite-integral-closure construction after completing a height-one local ring.

Imports3

Imported by2

def

standardCompleteDVFOfCompleteDVR

L31 ↗

EtaleFundamentalGroups.standardCompleteDVFOfCompleteDVR

Documentation

The canonical complete discrete valuation on the fraction field of a maximal-adically complete DVR.

Source context 5 commands

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

noncomputable section
namespace EtaleFundamentalGroups
open ValuationTheory
open ValuationTheory.DiscreteValuationField
universe uV uK

Lean source · full declaration

def standardCompleteDVFOfCompleteDVR
    (V : Type uV) (K : Type uK)
    [CommRing V] [IsDomain V] [IsDiscreteValuationRing V]
    [Field K] [Algebra V K] [IsFractionRing V K]
    [IsAdicComplete (IsLocalRing.maximalIdeal V) V] :
    CompleteDVF.{uK, 0} K where
  ValueGroup := WithZero (Multiplicative ℤ)
  valuation := (IsDiscreteValuationRing.maximalIdeal V).valuation K
  instCompleteDiscrete :=
    { isRankOneDiscrete := inferInstance
      isAdicComplete := by
        let v := (IsDiscreteValuationRing.maximalIdeal V).valuation K
        let e : V ≃+* v.valuationSubring :=
          IsDiscreteValuationRing.equivValuationSubring (A := V) (K := K)
        have hcomplete :
            IsAdicComplete
              ((IsLocalRing.maximalIdeal V).map e.toRingHom)
              v.valuationSubring :=
          ValuationTheory.DiscreteValuationField.isAdicComplete_map_ringEquiv
            (I := IsLocalRing.maximalIdeal V) e
        have hmap :
            (IsLocalRing.maximalIdeal V).map e.toRingHom =
              IsLocalRing.maximalIdeal v.valuationSubring :=
          ValuationTheory.ringEquiv_map_maximalIdeal e
        rw [hmap] at hcomplete
        exact hcomplete }

theorem

standardCompleteDVFOfCompleteDVR_toDVF

L60 ↗

EtaleFundamentalGroups.standardCompleteDVFOfCompleteDVR_toDVF