NYLL
Module

FiniteAbelianLocalReciprocity.lean

Nyll.ClassFieldTheory.Theorems.LocalClassFieldTheory.FiniteAbelianLocalReciprocity
1 declaration indexed from sourceView source ↗

Module documentation

Finite abelian local reciprocity

This module states local reciprocity for a finite abelian extension L / K of a nonarchimedean local field. The assumptions provide the finite abelian-Galois extension together with the valuative topology on K. The conclusion supplies a surjective continuous homomorphism from Kˣ to the Galois group whose kernel consists exactly of nonzero field norms from L.

This finite quotient statement deliberately leaves the usual uniformizer normalization and tower functoriality to separate compatibility theorems; it does not claim that the displayed witness is uniquely determined.

Imports5
Imported by1

Declarations

theorem

finiteAbelianLocalReciprocity

L33 ↗
ClassFieldTheory.finiteAbelianLocalReciprocity
Documentation

A finite abelian local extension has a surjective continuous Artin map whose kernel is its field-norm subgroup.

Source context 2 commands

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

noncomputable section
namespace ClassFieldTheory
Lean source · statement
theorem finiteAbelianLocalReciprocity
    (K L : Type)
    [Field K] [Field L] [Algebra K L]
    [FiniteDimensional K L] [IsAbelianGalois K L]
    [ValuativeRel K] [TopologicalSpace K]
    [IsNonarchimedeanLocalField K] :
    ∃ artin : Kˣ →ₜ* (L ≃ₐ[K] L),
      Function.Surjective artin ∧
      ∀ x : Kˣ, artin x = 1 ↔ IsFieldNorm K L x

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.