Nyll.ClassFieldTheory.Theorems.LocalClassFieldTheory.FiniteAbelianLocalReciprocityTower

Module documentation

Tower compatibility of finite local reciprocity

The canonical finite local Artin maps are compatible with restriction in a tower of finite abelian extensions. This is stronger than separately choosing the maps supplied by the finite-level existence theorem; the proof uses the single compatible construction in the implementation layer.

theorem

finiteAbelianLocalReciprocity_tower

L26 ↗

ClassFieldTheory.finiteAbelianLocalReciprocity_tower

Documentation

In a finite abelian tower K ⊆ E ⊆ L, one can choose the two continuous Artin maps so that restriction of the upper map equals the lower map. Both maps retain the expected norm kernels.

Source context 2 commands

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

noncomputable section
namespace ClassFieldTheory

Lean source · statement

theorem finiteAbelianLocalReciprocity_tower
    (K E L : Type)
    [Field K] [Field E] [Field L]
    [Algebra K E] [Algebra E L] [Algebra K L]
    [IsScalarTower K E L]
    [FiniteDimensional K E] [FiniteDimensional K L]
    [IsAbelianGalois K E] [IsAbelianGalois K L]
    [ValuativeRel K] [TopologicalSpace K]
    [IsNonarchimedeanLocalField K] :
    ∃ artinL : Kˣ →ₜ* (L ≃ₐ[K] L),
      ∃ artinE : Kˣ →ₜ* (E ≃ₐ[K] E),
        Function.Surjective artinL ∧
        Function.Surjective artinE ∧
        artinL.ker = fieldNormSubgroup K L ∧
        artinE.ker = fieldNormSubgroup K E ∧
        (AlgEquiv.restrictNormalHom E).comp artinL.toMonoidHom =
          artinE.toMonoidHom

Module documentation

Tower compatibility of finite local reciprocity

Declarations

finiteAbelianLocalReciprocity_tower