Nyll.ClassFieldTheory.Theorems.LocalClassFieldTheory.FiniteAbelianLocalReciprocityFamilyUnramifiedNormalization

Module documentation

Frobenius normalization of one coherent finite local reciprocity family

The same family has norm kernels and restriction compatibility, and at each unramified valued realization sends an inverse uniformizer to arithmetic Frobenius on the residue field. The local-field structures on an intermediate field are explicit because the chosen separable closure does not currently carry a canonical valued-field structure in the public definitions.

theorem

finiteAbelianLocalReciprocity_family_unramifiedNormalization

L35 ↗

ClassFieldTheory.finiteAbelianLocalReciprocity_family_unramifiedNormalization

Documentation

One coherent family of finite local Artin maps is normalized by arithmetic Frobenius at every unramified valued realization of a member. The valuation of the member must extend the valuation of K.

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_family_unramifiedNormalization
    (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)) ∧
      ∀ (E : FiniteAbelianLocalExtension K)
        [ValuativeRel E.1] [UniformSpace E.1] [IsUniformAddGroup E.1]
        [IsNonarchimedeanLocalField E.1]
        [Valuation.HasExtension (ValuativeRel.valuation K)
          (ValuativeRel.valuation E.1)],
        (𝓂[E.1] : Ideal 𝒪[E.1]).ramificationIdx 𝒪[K] = 1 →
        ∀ (π : 𝒪[K])
          (hπ : (ValuativeRel.valuation K).IsUniformizer (π : K))
          (x : 𝒪[E.1]),
          ∃ z : 𝒪[E.1],
            (z : E.1) =
                (artin E ((Units.mk0 (π : K) hπ.ne_zero)⁻¹)) (x : E.1) ∧
              IsLocalRing.residue 𝒪[E.1] z =
                (IsLocalRing.residue 𝒪[E.1] x) ^ Nat.card 𝓀[K]

Module documentation

Frobenius normalization of one coherent finite local reciprocity family

Declarations

finiteAbelianLocalReciprocity_family_unramifiedNormalization