Module

RayLocalHigherUnitOpen.lean

Nyll.ClassFieldTheory.Theorems.ConductorsAndRayClassFields.RayLocalHigherUnitOpen

1 declaration indexed from sourceView source ↗

Module documentation

Openness of local higher-unit groups

For every depth, including zero, the higher-unit subgroup is open in the multiplicative group of the finite completion.

Imports2

Imported by1

Nyll.ClassFieldTheory.Theorems.ConductorsAndRayClassFields.All

theorem

isOpen_rayLocalHigherUnitGroup

L28 ↗

ClassFieldTheory.isOpen_rayLocalHigherUnitGroup

Documentation

Every local higher-unit group is open in the local multiplicative group.

Source context 5 commands

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

open scoped NumberField
noncomputable section
namespace ClassFieldTheory
universe u
open NumberField IsDedekindDomain

Lean source · statement

theorem isOpen_rayLocalHigherUnitGroup
    {K : Type u} [Field K] [NumberField K]
    (v : HeightOneSpectrum (𝓞 K)) (n : ℕ) :
    IsOpen ((rayLocalHigherUnitGroup v n :
      Subgroup (v.adicCompletion K)ˣ) : Set (v.adicCompletion K)ˣ)

Module documentation

Openness of local higher-unit groups

Declarations

isOpen_rayLocalHigherUnitGroup