Module

UnramifiedResidueUniqueness.lean

Nyll.ClassFieldTheory.LocalClassFieldTheory.Finite.LocalReciprocity.UnramifiedResidueUniqueness

3 declarations indexed from sourceView source ↗

Module documentation

Uniqueness of arithmetic Frobenius from its residue action

For an unramified finite abelian extension, the arithmetic q-power action on residues determines the Galois automorphism uniquely. The canonical local Artin map takes an inverse uniformizer to this automorphism.

Imports3

Imported by4

instance

(anonymous instance)

L35 ↗

Source context 4 commands

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

open scoped ValuativeRel
noncomputable section
namespace ClassFieldTheory
variable (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)]
  [LocalFieldTheory.IsNonarchimedeanLocalField.IsUnramifiedValuedExtension K L]

Lean source · statement

instance : IsIntegralClosure 𝒪[L] 𝒪[K] L

instance

(anonymous instance)

L38 ↗

Source context 4 commands

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

open scoped ValuativeRel
noncomputable section
namespace ClassFieldTheory
variable (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)]
  [LocalFieldTheory.IsNonarchimedeanLocalField.IsUnramifiedValuedExtension K L]

Lean source · statement

instance : Module.Finite 𝒪[K] 𝒪[L]

theorem

finiteAbelianLocalArtinMap_inverseUniformizer_residue_pow_iff

L43 ↗

ClassFieldTheory.finiteAbelianLocalArtinMap_inverseUniformizer_residue_pow_iff

Documentation

The residue q-power action characterizes the canonical local Artin image of an inverse uniformizer in an unramified finite abelian extension.

Source context 4 commands

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

open scoped ValuativeRel
noncomputable section
namespace ClassFieldTheory
variable (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)]
  [LocalFieldTheory.IsNonarchimedeanLocalField.IsUnramifiedValuedExtension K L]

Lean source · statement

theorem finiteAbelianLocalArtinMap_inverseUniformizer_residue_pow_iff
    (π : 𝒪[K])
    (hπ : (ValuativeRel.valuation K).IsUniformizer (π : K))
    (σ : L ≃ₐ[K] L) :
    (∀ x : 𝒪[L],
      ∃ z : 𝒪[L],
        (z : L) = σ (x : L) ∧
          IsLocalRing.residue 𝒪[L] z =
            (IsLocalRing.residue 𝒪[L] x) ^ Nat.card 𝓀[K]) ↔
      σ = LocalClassFieldTheory.abelianLocalArtinMap K L
        ((Units.mk0 (π : K) hπ.ne_zero)⁻¹)

Module documentation

Uniqueness of arithmetic Frobenius from its residue action

Declarations

(anonymous instance)

(anonymous instance)

finiteAbelianLocalArtinMap_inverseUniformizer_residue_pow_iff