Nyll.ClassFieldTheory.Theorems.LocalClassFieldTheory.FiniteAbelianLocalReciprocityFamilyArithmeticFrobenius

Module documentation

Arithmetic Frobenius in the coherent local reciprocity family

For an unramified member of one coherent finite local Artin family, the inverse of every uniformizer maps to the unique Galois automorphism whose reduction is the arithmetic q-power Frobenius. The uniqueness clause is essential: residue-field behavior is a normalization of the same family, not a separate independently chosen reciprocity map.

theorem

finiteAbelianLocalReciprocity_family_arithmeticFrobenius

L33 ↗

ClassFieldTheory.finiteAbelianLocalReciprocity_family_arithmeticFrobenius

Documentation

A coherent finite local reciprocity family whose inverse-uniformizer value is characterized uniquely by arithmetic Frobenius on residues.

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_arithmeticFrobenius
    (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))
          (σ : E.1 ≃ₐ[K] E.1),
          (∀ x : 𝒪[E.1],
            ∃ z : 𝒪[E.1],
              (z : E.1) = σ (x : E.1) ∧
                IsLocalRing.residue 𝒪[E.1] z =
                  (IsLocalRing.residue 𝒪[E.1] x) ^ Nat.card 𝓀[K]) ↔
            σ = artin E ((Units.mk0 (π : K) hπ.ne_zero)⁻¹)

Module documentation

Arithmetic Frobenius in the coherent local reciprocity family

Declarations

finiteAbelianLocalReciprocity_family_arithmeticFrobenius