Module

RayLocalHigherUnitGroup.lean

Nyll.ClassFieldTheory.Definitions.ConductorsAndRayClassFields.RayLocalHigherUnitGroup

2 declarations indexed from sourceView source ↗

Module documentation

Higher-unit subgroups at finite places

Imports1

Mathlib.NumberTheory.NumberField.Completion.FinitePlace

Imported by10

def

rayLocalHigherUnitMap

L26 ↗

ClassFieldTheory.rayLocalHigherUnitMap

Documentation

Reduction of a local integral unit modulo the n-th power of the maximal ideal.

Source context 5 commands

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

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

Lean source · statement

def rayLocalHigherUnitMap
    {K : Type u} [Field K] [NumberField K]
    (v : HeightOneSpectrum (𝓞 K)) (n : ℕ) :
    (v.adicCompletionIntegers K).units →*
      ((v.adicCompletionIntegers K) ⧸
        (IsLocalRing.maximalIdeal (v.adicCompletionIntegers K)) ^ n)ˣ

def

rayLocalHigherUnitGroup

L39 ↗

ClassFieldTheory.rayLocalHigherUnitGroup