Module

WithZeroValuationTopology.lean

Nyll.ValuedFieldTheory.LocalField.DiscreteValuationField.WithZeroValuationTopology

3 declarations indexed from sourceView source ↗

Module documentation

The direct topology of a standard multiplicative integer valuation

This file transfers completeness from the actual-range restriction of a complete discrete valuation back to the topology obtained directly from Valued.mk' v.

Imports12

Imported by2

def

completeDVF

L46 ↗

LocalFieldTheory.DiscreteValuationField.WithZeroValuationTopology.completeDVF

Documentation

The complete-DVF package attached to a standard ℤᵐ⁰-valued complete discrete valuation.

Source context 9 commands

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

noncomputable section
universe u
open Filter
open scoped Valued
open LocalFieldTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField
namespace LocalFieldTheory.DiscreteValuationField
namespace WithZeroValuationTopology
variable {K : Type u} [Field K]

Lean source · full declaration

def completeDVF
    (v : _root_.Valuation K (WithZero (Multiplicative ℤ)))
    [Valuation.IsCompleteDiscrete v] : CompleteDVF.{u, 0} K where
  ValueGroup := WithZero (Multiplicative ℤ)
  valuation := v
  instCompleteDiscrete := inferInstance

theorem

valuedMk_uniformSpace_eq_mrangeRestrict

L58 ↗

LocalFieldTheory.DiscreteValuationField.WithZeroValuationTopology.valuedMk_uniformSpace_eq_mrangeRestrict

Documentation

Restricting a standard ℤᵐ⁰-valued valuation to its actual range does not change the uniform structure on the field.

Source context 10 commands

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

noncomputable section
universe u
open Filter
open scoped Valued
open LocalFieldTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField
namespace LocalFieldTheory.DiscreteValuationField
namespace WithZeroValuationTopology
variable {K : Type u} [Field K]
open _root_.LocalFieldTheory.DiscreteValuationField.CompleteDVF (
  mrangeRestrictValued
) in

Lean source · statement

theorem valuedMk_uniformSpace_eq_mrangeRestrict
    (v : _root_.Valuation K (WithZero (Multiplicative ℤ)))
    [Valuation.IsCompleteDiscrete v] :
    (Valued.mk' v).toUniformSpace =
      (mrangeRestrictValued (completeDVF v)).toUniformSpace

theorem

completeSpace_ofWithZeroValuation

L83 ↗

LocalFieldTheory.DiscreteValuationField.WithZeroValuationTopology.completeSpace_ofWithZeroValuation

Documentation

A standard complete discrete valuation with finite residue field makes the field complete for the topology obtained directly from Valued.mk' v.

Source context 10 commands

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

noncomputable section
universe u
open Filter
open scoped Valued
open LocalFieldTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField
namespace LocalFieldTheory.DiscreteValuationField
namespace WithZeroValuationTopology
variable {K : Type u} [Field K]
open _root_.LocalFieldTheory.DiscreteValuationField.CompleteDVF (
  mrangeRestrict_nontriviallyNormedField
  mrangeRestrict_completeSpace_of_residueField_finite
) in

Lean source · full declaration

theorem completeSpace_ofWithZeroValuation
    (v : _root_.Valuation K (WithZero (Multiplicative ℤ)))
    [Valuation.IsCompleteDiscrete v]
    [Finite (IsLocalRing.ResidueField v.valuationSubring)] :
    letI : Valued K (WithZero (Multiplicative ℤ)) := Valued.mk' v
    CompleteSpace K := by
  let F : CompleteDVF.{u, 0} K := completeDVF v
  let direct : Valued K (WithZero (Multiplicative ℤ)) := Valued.mk' v
  let restrictedNormed : NontriviallyNormedField K :=
    mrangeRestrict_nontriviallyNormedField F
  have : Finite F.residueField := by
    change Finite (IsLocalRing.ResidueField v.valuationSubring)
    infer_instance
  have hcomplete : @CompleteSpace K restrictedNormed.toUniformSpace := by
    exact mrangeRestrict_completeSpace_of_residueField_finite F
  have huniform : direct.toUniformSpace = restrictedNormed.toUniformSpace := by
    change
      (Valued.mk' v).toUniformSpace =
        (mrangeRestrict_nontriviallyNormedField
          (completeDVF v)).toUniformSpace
    calc
      (Valued.mk' v).toUniformSpace =
          (_root_.LocalFieldTheory.DiscreteValuationField.CompleteDVF.mrangeRestrictValued
            (completeDVF v)).toUniformSpace :=
        valuedMk_uniformSpace_eq_mrangeRestrict v
      _ =
          (mrangeRestrict_nontriviallyNormedField
            (completeDVF v)).toUniformSpace := by
        rfl
  let : Valued K (WithZero (Multiplicative ℤ)) := direct
  change @CompleteSpace K direct.toUniformSpace
  rw [huniform]
  exact hcomplete

Module documentation

The direct topology of a standard multiplicative integer valuation

Declarations

completeDVF

valuedMk_uniformSpace_eq_mrangeRestrict

completeSpace_ofWithZeroValuation