Module

UnitTopology.lean

Nyll.ValuedFieldTheory.LocalField.NonarchimedeanLocalField.UnitTopology

3 declarations indexed from sourceView source ↗

Module documentation

The unit subgroup of a nonarchimedean local field

This module identifies the image of valuation-ring units in the field unit group with the valuation-one sphere and records that this subgroup is open in the native topology of a nonarchimedean local field.

Imports1

Nyll.ValuedFieldTheory.LocalField.NonarchimedeanLocalField.Basic

Imported by3

def

localBaseUnitSubgroup

L29 ↗

LocalFieldTheory.localBaseUnitSubgroup

Documentation

The image of valuation-ring units in the field unit group.

Source context 5 commands

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

noncomputable section
universe u
namespace LocalFieldTheory
open scoped ValuativeRel
open _root_.LocalFieldTheory.IsNonarchimedeanLocalField

Lean source · statement

def localBaseUnitSubgroup
    (K : Type u) [Field K] [ValuativeRel K] : Subgroup Kˣ

theorem

mem_localBaseUnitSubgroup_iff_valuation_eq_one

L35 ↗

LocalFieldTheory.mem_localBaseUnitSubgroup_iff_valuation_eq_one

Documentation

A field unit lies in the image of valuation-ring units exactly when its valuation is one.

Source context 5 commands

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

noncomputable section
universe u
namespace LocalFieldTheory
open scoped ValuativeRel
open _root_.LocalFieldTheory.IsNonarchimedeanLocalField

Lean source · statement

theorem mem_localBaseUnitSubgroup_iff_valuation_eq_one
    (K : Type u) [Field K] [ValuativeRel K] (x : Kˣ) :
    x ∈ localBaseUnitSubgroup K ↔ ValuativeRel.valuation K (x : K) = 1

theorem

localBaseUnitSubgroup_isOpen

L57 ↗

LocalFieldTheory.localBaseUnitSubgroup_isOpen

Documentation

The image of valuation-ring units is open in the native topology of a nonarchimedean local field.

Source context 5 commands

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

noncomputable section
universe u
namespace LocalFieldTheory
open scoped ValuativeRel
open _root_.LocalFieldTheory.IsNonarchimedeanLocalField

Lean source · statement

theorem localBaseUnitSubgroup_isOpen
    (K : Type u) [Field K] [ValuativeRel K] [TopologicalSpace K]
    [IsNonarchimedeanLocalField K] :
    IsOpen (localBaseUnitSubgroup K : Set Kˣ)

Module documentation

The unit subgroup of a nonarchimedean local field

Declarations

localBaseUnitSubgroup

mem_localBaseUnitSubgroup_iff_valuation_eq_one

localBaseUnitSubgroup_isOpen