Module

RayLocalHigherUnitMembership.lean

Nyll.ClassFieldTheory.Theorems.ConductorsAndRayClassFields.RayLocalHigherUnitMembership

1 declaration indexed from sourceView source ↗

Module documentation

Congruence description of local higher units

An element of the n-th higher-unit group is an integral unit congruent to 1 modulo the n-th power of the maximal ideal. This also applies at n = 0, where the condition reduces to being an integral unit.

Imports3

Nyll.ClassFieldTheory.Definitions.ConductorsAndRayClassFields.RayLocalHigherUnitGroup
Nyll.ClassFieldTheory.AlgebraicNumberTheory.RayClass.Basic
Mathlib.RingTheory.Ideal.Quotient.Defs

Imported by2

theorem

mem_rayLocalHigherUnitGroup_iff

L31 ↗

ClassFieldTheory.mem_rayLocalHigherUnitGroup_iff

Documentation

Membership in the n-th local higher-unit group is precisely the congruence y ≡ 1 (mod 𝔪_v^n) for an integral-unit representative.

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 mem_rayLocalHigherUnitGroup_iff
    {K : Type u} [Field K] [NumberField K]
    (v : HeightOneSpectrum (𝓞 K)) (n : ℕ)
    (x : (v.adicCompletion K)ˣ) :
    x ∈ rayLocalHigherUnitGroup v n ↔
      ∃ y : (v.adicCompletionIntegers K)ˣ,
        ((v.adicCompletionIntegers K).toSubmonoid.unitsEquivUnitsType.symm y :
          (v.adicCompletion K)ˣ) = x ∧
        (y : v.adicCompletionIntegers K) - 1 ∈
          (IsLocalRing.maximalIdeal (v.adicCompletionIntegers K)) ^ n

Module documentation

Congruence description of local higher units

Declarations

mem_rayLocalHigherUnitGroup_iff