NYLL
Module

FiniteAbelianLocalReciprocityQuotient.lean

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

Module documentation

Quotient form of finite abelian local reciprocity

This module states the quotient formulation of local reciprocity for a finite abelian extension L / K of a nonarchimedean local field. Under the finite-dimensional, abelian-Galois, valuative, and topological assumptions, the conclusion identifies Kˣ / N_{L/K}(Lˣ) with the ordinary Galois group by a continuous multiplicative equivalence.

Imports6
Imported by1

Declarations

theorem

finiteAbelianLocalReciprocity_quotient

L30 ↗
ClassFieldTheory.finiteAbelianLocalReciprocity_quotient
Documentation

The field-norm quotient is continuously multiplicatively equivalent to the finite abelian Galois group.

Source context 2 commands

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

noncomputable section
namespace ClassFieldTheory
Lean source · statement
theorem finiteAbelianLocalReciprocity_quotient
    (K L : Type)
    [Field K] [Field L] [Algebra K L]
    [FiniteDimensional K L] [IsAbelianGalois K L]
    [ValuativeRel K] [TopologicalSpace K]
    [IsNonarchimedeanLocalField K] :
    Nonempty
      (FieldNormQuotient K L ≃ₜ* (L ≃ₐ[K] L))

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