Module

Uniformizer.lean

Nyll.ClassFieldTheory.LocalClassFieldTheory.Finite.Unramified.Uniformizer

2 declarations indexed from sourceView source ↗

Module documentation

Actual unramified norm quotient uniformizer

This file connects the real valuation quotient Kˣ / unramifiedNormSubgroup K n from NormSubgroup with the chosen inverse DVR uniformizer from IdealQuotients. This is the unramified norm calculation uniformizer side of the local reciprocity construction, kept below NormSubgroup to avoid importing the chosen-uniformizer layer into the generic valuation quotient API.

Imports2

Imported by2

theorem

unramifiedNormQuotientEquivZMod_inverseIntegerRingUniformizerFieldUnit

L34 ↗

LocalClassFieldTheory.unramifiedNormQuotientEquivZMod_inverseIntegerRingUniformizerFieldUnit

Documentation

the unramified norm calculation, valuation-quotient side: the chosen inverse prime element has normalized value 1, hence its class maps to 1 : ZMod n. This is the uniformizer-side source matching the normalized Frobenius model.

Source context 5 commands

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

noncomputable section
universe u
namespace LocalClassFieldTheory
open scoped ValuativeRel
open LocalFieldTheory

Lean source · statement

theorem unramifiedNormQuotientEquivZMod_inverseIntegerRingUniformizerFieldUnit
    (K : Type u) [Field K] [ValuativeRel K] [TopologicalSpace K]
    [IsNonarchimedeanLocalField K] (n : Nat) :
    unramifiedNormQuotientEquivZMod K n
        (QuotientGroup.mk (inverseIntegerRingUniformizerFieldUnit K) :
          Kˣ ⧸ unramifiedNormSubgroup K n) =
      Multiplicative.ofAdd (1 : ZMod n)

theorem

unramifiedNormQuotientEquivZMod_inverseIntegerRingUniformizerFieldUnit_zpow

L47 ↗

LocalClassFieldTheory.unramifiedNormQuotientEquivZMod_inverseIntegerRingUniformizerFieldUnit_zpow