Module

StandardOpenSubgroups.lean

Nyll.ValuedFieldTheory.LocalField.NonarchimedeanLocalField.StandardOpenSubgroups

4 declarations indexed from sourceView source ↗

Module documentation

Standard open subgroups of a nonarchimedean local field

An open finite-index subgroup of a nonarchimedean local field multiplicative group contains a standard subgroup built from a uniformizer and a sufficiently deep principal-unit group.

Imports1

Nyll.ValuedFieldTheory.LocalField.NonarchimedeanLocalField.PrincipalUnitQuotients

Imported by11

def

fieldPrincipalUnits

L32 ↗

LocalFieldTheory.fieldPrincipalUnits

Documentation

The n-th principal-unit group, viewed as a subgroup of the field's multiplicative group.

Source context 6 commands

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

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

Lean source · statement

def fieldPrincipalUnits
    (K : Type u) [Field K] [ValuativeRel K] (n : ℕ) : Subgroup Kˣ

def

uniformizerPrincipalSubgroup

L38 ↗

LocalFieldTheory.uniformizerPrincipalSubgroup

Documentation

The standard subgroup (ϖ^d) · U^n used in the existence theorem. The product of the two commuting subgroups is written as their supremum.

Source context 6 commands

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

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

Lean source · statement

def uniformizerPrincipalSubgroup
    (K : Type u) [Field K] [ValuativeRel K]
    (ϖ : Kˣ) (d n : ℕ) : Subgroup Kˣ

theorem

exists_fieldPrincipalUnits_le_of_isOpen

L45 ↗

LocalFieldTheory.exists_fieldPrincipalUnits_le_of_isOpen

Documentation

Every open subgroup of the multiplicative group of a nonarchimedean local field contains a sufficiently deep positive principal-unit group.

Source context 6 commands

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

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

Lean source · statement

theorem exists_fieldPrincipalUnits_le_of_isOpen
    (K : Type u) [Field K] [ValuativeRel K] [TopologicalSpace K]
    [IsNonarchimedeanLocalField K]
    (H : Subgroup Kˣ) (hH : IsOpen (H : Set Kˣ)) :
    ∃ n : ℕ, 1 ≤ n ∧ fieldPrincipalUnits K n ≤ H

theorem

exists_uniformizerPrincipalSubgroup_le_of_isOpen_finiteIndex

L85 ↗

LocalFieldTheory.exists_uniformizerPrincipalSubgroup_le_of_isOpen_finiteIndex

Documentation

An open finite-index subgroup contains a standard subgroup generated by a uniformizer power and a sufficiently deep principal-unit group.

Source context 6 commands

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

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

Lean source · statement

theorem exists_uniformizerPrincipalSubgroup_le_of_isOpen_finiteIndex
    (K : Type u) [Field K] [ValuativeRel K] [TopologicalSpace K]
    [IsNonarchimedeanLocalField K]
    (H : Subgroup Kˣ) [H.FiniteIndex] (hH : IsOpen (H : Set Kˣ)) :
    ∃ (ϖ : Kˣ) (d n : ℕ),
      v K (Additive.ofMul ϖ) = 1 ∧
      0 < d ∧ 1 ≤ n ∧
      uniformizerPrincipalSubgroup K ϖ d n ≤ H

Module documentation

Standard open subgroups of a nonarchimedean local field

Declarations

fieldPrincipalUnits

uniformizerPrincipalSubgroup

exists_fieldPrincipalUnits_le_of_isOpen

exists_uniformizerPrincipalSubgroup_le_of_isOpen_finiteIndex