Module

PrincipalUnitValuationTopology.lean

Nyll.ValuedFieldTheory.LocalField.Analytic.PrincipalUnitValuationTopology

2 declarations indexed from sourceView source ↗

Module documentation

The valuation topology on principal units is the adic topology

The comparison uses the actual valuation topology and does not require a finite residue field. The valued-field structure is fixed once in the context.

Imports3

Imported by2

theorem

principalUnit_valuationTopology_eq_adic

L29 ↗

LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.principalUnit_valuationTopology_eq_adic

Documentation

The inherited topology on principal units equals their intrinsic adic topology.

Source context 5 commands

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

namespace LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation
universe u
variable {K : Type u} [Field K] [Valued K (WithZero (Multiplicative ℤ))]
variable [ValuationTheory.DiscreteValuationField.Valuation.IsCompleteDiscrete
  (Valued.v : _root_.Valuation K (WithZero (Multiplicative ℤ)))]
open CompleteDVF.higherPrincipalUnitGroup

Lean source · statement

theorem principalUnit_valuationTopology_eq_adic :
    (inferInstance : TopologicalSpace
      (Additive (CompleteDVF.higherPrincipalUnitGroup
        (completeDVFOfWithZeroValuation (Valued.v : _root_.Valuation K
          (WithZero (Multiplicative ℤ)))) 1))) =
      principalUnitAdicTopology (completeDVFOfWithZeroValuation
        (Valued.v : _root_.Valuation K (WithZero (Multiplicative ℤ))))

def

principalUnitAdicContinuousAddEquiv

L56 ↗

LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.principalUnitAdicContinuousAddEquiv