Nyll.ClassFieldTheory.Theorems.LocalClassFieldTheory.FiniteAbelianLocalReciprocityUnramifiedNormalization

Module documentation

Arithmetic normalization of finite local reciprocity

For an unramified finite abelian extension, one and the same Artin map is surjective, has the field-norm kernel, and sends every inverse uniformizer to the arithmetic Frobenius on residues. The statement uses only Mathlib and public Definitions vocabulary; the implementation is used in the proof.

theorem

finiteAbelianLocalReciprocity_unramifiedNormalization

L33 ↗

ClassFieldTheory.finiteAbelianLocalReciprocity_unramifiedNormalization

Documentation

An unramified finite abelian extension admits a norm-kernel Artin map whose value on the inverse of each uniformizer acts by the arithmetic q-power Frobenius on the residue field.

Source context 3 commands

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

open scoped ValuativeRel
noncomputable section
namespace ClassFieldTheory

Lean source · statement

theorem finiteAbelianLocalReciprocity_unramifiedNormalization
    (K L : Type)
    [Field K] [ValuativeRel K] [TopologicalSpace K]
    [IsNonarchimedeanLocalField K]
    [Field L] [ValuativeRel L] [UniformSpace L] [IsUniformAddGroup L]
    [IsNonarchimedeanLocalField L]
    [Algebra K L] [FiniteDimensional K L] [IsAbelianGalois K L]
    [Valuation.HasExtension (ValuativeRel.valuation K)
      (ValuativeRel.valuation L)]
    (hUnram : (𝓂[L] : Ideal 𝒪[L]).ramificationIdx 𝒪[K] = 1) :
    ∃ artin : Kˣ →ₜ* (L ≃ₐ[K] L),
      Function.Surjective artin ∧
        artin.toMonoidHom.ker = fieldNormSubgroup K L ∧
        ∀ (π : 𝒪[K])
          (hπ : (ValuativeRel.valuation K).IsUniformizer (π : K))
          (x : 𝒪[L]),
          ∃ z : 𝒪[L],
            (z : L) =
                (artin ((Units.mk0 (π : K) hπ.ne_zero)⁻¹)) (x : L) ∧
              IsLocalRing.residue 𝒪[L] z =
                (IsLocalRing.residue 𝒪[L] x) ^ Nat.card 𝓀[K]

Module documentation

Arithmetic normalization of finite local reciprocity

Declarations

finiteAbelianLocalReciprocity_unramifiedNormalization