Module

ProfiniteLocalReciprocity.lean

Nyll.ClassFieldTheory.Theorems.LocalClassFieldTheory.ProfiniteLocalReciprocity

1 declaration indexed from sourceView source ↗

Module documentation

Profinite local reciprocity

For a nonarchimedean local field K, the profinite completion of Kˣ with respect to its open finite-index normal subgroups is continuously multiplicatively equivalent to the topological abelianization of Mathlib's absolute Galois group of K.

Imports4

Nyll.ClassFieldTheory.Definitions.LocalClassFieldTheory.TopologicalProfiniteCompletion
Nyll.ClassFieldTheory.LocalClassFieldTheory.Infinite.ProfiniteLocalReciprocity
Mathlib.FieldTheory.AbsoluteGaloisGroup
Mathlib.NumberTheory.LocalField.Basic

Imported by1

Nyll.ClassFieldTheory.Theorems.LocalClassFieldTheory.All

theorem

profiniteLocalReciprocity

L28 ↗

ClassFieldTheory.profiniteLocalReciprocity

Documentation

Profinite local reciprocity. The topological profinite completion of the multiplicative group of a nonarchimedean local field is continuously multiplicatively equivalent to its absolute Galois abelianization.

Source context 2 commands

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

noncomputable section
namespace ClassFieldTheory

Lean source · statement

theorem profiniteLocalReciprocity
    (K : Type)
    [Field K] [ValuativeRel K] [TopologicalSpace K]
    [IsNonarchimedeanLocalField K] :
    Nonempty
      (LocalClassFieldTheory.TopologicalProfiniteCompletion Kˣ ≃ₜ*
        _root_.Field.absoluteGaloisGroupAbelianization K)

Module documentation

Profinite local reciprocity

Declarations

profiniteLocalReciprocity