Module

FiniteAbelianLocalReciprocityFamily.lean

Nyll.ClassFieldTheory.Theorems.LocalClassFieldTheory.FiniteAbelianLocalReciprocityFamily

1 declaration indexed from sourceView source ↗

Module documentation

A coherent family of finite local Artin maps

The finite-level Artin maps can be chosen simultaneously for all finite abelian subextensions of a fixed separable closure. Their norm kernels and restriction compatibility refer to the same family, not to independently chosen maps for each tower. The arithmetic-Frobenius normalization is a separate property of this family. This theorem currently uses the source construction at Type 0; arbitrary-universe transport remains separate.

Imports2

Imported by1

Nyll.ClassFieldTheory.Theorems.LocalClassFieldTheory.All

theorem

finiteAbelianLocalReciprocity_family

L27 ↗

ClassFieldTheory.finiteAbelianLocalReciprocity_family

Documentation

One family of continuous local Artin maps has the expected norm kernels and commutes with inclusion of finite abelian subextensions.

Source context 2 commands

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

noncomputable section
namespace ClassFieldTheory

Lean source · statement

theorem finiteAbelianLocalReciprocity_family
    (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K]
    [IsNonarchimedeanLocalField K] :
    ∃ artin : (E : FiniteAbelianLocalExtension K) →
        Kˣ →ₜ* (E.1 ≃ₐ[K] E.1),
      (∀ E : FiniteAbelianLocalExtension K,
        Function.Surjective (artin E) ∧
          (artin E).toMonoidHom.ker = E.normSubgroup) ∧
      ∀ (E F : FiniteAbelianLocalExtension K)
        (hEF : E.1 ≤ F.1) (x : Kˣ) (y : E.1),
        IntermediateField.inclusion hEF ((artin E x) y) =
          (artin F x) (IntermediateField.inclusion hEF y)

Module documentation

A coherent family of finite local Artin maps

Declarations

finiteAbelianLocalReciprocity_family