NYLL
Module

UnramifiedNormalization.lean

Nyll.ClassFieldTheory.LocalClassFieldTheory.Finite.LocalReciprocity.UnramifiedNormalization
23 declarations indexed from sourceView source ↗

Module documentation

Canonical unramified normalization

The canonical local norm-residue symbol is identified with the field-facing unramified Artin map. An element of normalized valuation one maps to arithmetic Frobenius, both algebraically and in the topological abelianization.

Canonical norm-residue normalization

Equality with the field-facing unramified reciprocity map

Continuous Frobenius normalization

Imports10
Imported by13

Declarations

abbrev

G

L36 ↗
LocalClassFieldTheory.G
Source context 5 commands

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

noncomputable section
namespace LocalClassFieldTheory
open scoped IsMulCommutative ValuativeRel
open LocalFieldTheory RamificationTheory CyclicCohomology KummerTheory
open ClassFormation
Lean source · statement
abbrev G (K : Type) [Field K]
abbrev

A

L39 ↗
LocalClassFieldTheory.A
Source context 5 commands

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

noncomputable section
namespace LocalClassFieldTheory
open scoped IsMulCommutative ValuativeRel
open LocalFieldTheory RamificationTheory CyclicCohomology KummerTheory
open ClassFormation
Lean source · statement
abbrev A (K : Type) [Field K] : Rep ℤ (G K)
abbrev

B

L42 ↗
LocalClassFieldTheory.B
Source context 5 commands

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

noncomputable section
namespace LocalClassFieldTheory
open scoped IsMulCommutative ValuativeRel
open LocalFieldTheory RamificationTheory CyclicCohomology KummerTheory
open ClassFormation
Lean source · statement
abbrev B (K : Type) [Field K] : ClosedSubgroup (G K)
def

extensionQuotientEquivOfEq

L45 ↗
LocalClassFieldTheory.extensionQuotientEquivOfEq
Source context 5 commands

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

noncomputable section
namespace LocalClassFieldTheory
open scoped IsMulCommutative ValuativeRel
open LocalFieldTheory RamificationTheory CyclicCohomology KummerTheory
open ClassFormation
Lean source · statement
def extensionQuotientEquivOfEq
    {Γ : Type} [Group Γ] [TopologicalSpace Γ]
    {K L K' L' : ClosedSubgroup Γ}
    (hLK : L.toSubgroup ≤ K.toSubgroup)
    (hL'K' : L'.toSubgroup ≤ K'.toSubgroup)
    (hK : K = K') (hL : L = L') :
    (K.toSubgroup ⧸ extensionSubgroup K L hLK) ≃
      (K'.toSubgroup ⧸ extensionSubgroup K' L' hL'K')
theorem

localHenselianValuation_valuationAt_baseUnit

L64 ↗
LocalClassFieldTheory.localHenselianValuation_valuationAt_baseUnit
Source context 7 commands

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

noncomputable section
namespace LocalClassFieldTheory
open scoped IsMulCommutative ValuativeRel
open LocalFieldTheory RamificationTheory CyclicCohomology KummerTheory
open ClassFormation
section BasePrime
variable (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K]
  [IsNonarchimedeanLocalField K]
Lean source · statement
theorem localHenselianValuation_valuationAt_baseUnit
    (x : Kˣ) :
    (((localHenselianValuation K).valuationAt (intrinsicFiniteAbstractBase K)
      (baseUnitsEquivGaloisAmbientFixed K (SeparableClosure K)
        (Additive.ofMul x)) :
        (localHenselianValuation K).valueGroup) : ZHat) =
      Int.castRingHom ZHat
        (LocalFieldTheory.IsNonarchimedeanLocalField.valuationMap K
          (Additive.ofMul x))
def

localAbstractPrimeFieldUnit

L123 ↗
LocalClassFieldTheory.localAbstractPrimeFieldUnit
Documentation

The concrete base-field unit represented by the canonical prime element of the local henselian valuation.

Source context 7 commands

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

noncomputable section
namespace LocalClassFieldTheory
open scoped IsMulCommutative ValuativeRel
open LocalFieldTheory RamificationTheory CyclicCohomology KummerTheory
open ClassFormation
section BasePrime
variable (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K]
  [IsNonarchimedeanLocalField K]
Lean source · statement
def localAbstractPrimeFieldUnit : Kˣ
theorem

valuationMap_localAbstractPrimeFieldUnit_mod

L131 ↗
LocalClassFieldTheory.valuationMap_localAbstractPrimeFieldUnit_mod
Documentation

The canonical abstract prime has normalized valuation one modulo every positive integer after transport to the actual local field.

Source context 7 commands

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

noncomputable section
namespace LocalClassFieldTheory
open scoped IsMulCommutative ValuativeRel
open LocalFieldTheory RamificationTheory CyclicCohomology KummerTheory
open ClassFormation
section BasePrime
variable (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K]
  [IsNonarchimedeanLocalField K]
Lean source · statement
theorem valuationMap_localAbstractPrimeFieldUnit_mod
    (n : ℕ) (hn : 0 < n) :
    (LocalFieldTheory.IsNonarchimedeanLocalField.valuationMap K
        (Additive.ofMul (localAbstractPrimeFieldUnit K)) : ZMod n) = 1
instance

normalizationIntegerRingIsIntegralClosure

L173 ↗
LocalClassFieldTheory.normalizationIntegerRingIsIntegralClosure
Source context 7 commands

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

noncomputable section
namespace LocalClassFieldTheory
open scoped IsMulCommutative ValuativeRel
open LocalFieldTheory RamificationTheory CyclicCohomology KummerTheory
open ClassFormation
section UnramifiedPrimeClass
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] [IsGalois K L]
  [Valuation.HasExtension (ValuativeRel.valuation K)
    (ValuativeRel.valuation L)]
Lean source · statement
instance normalizationIntegerRingIsIntegralClosure :
    IsIntegralClosure 𝒪[L] 𝒪[K] L
theorem

normClass_localAbstractPrimeFieldUnit_eq_uniformizer

L183 ↗
LocalClassFieldTheory.normClass_localAbstractPrimeFieldUnit_eq_uniformizer
Documentation

In the actual unramified norm quotient, the canonical abstract prime and the chosen inverse DVR uniformizer define the same normalized generator.

Source context 9 commands

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

noncomputable section
namespace LocalClassFieldTheory
open scoped IsMulCommutative ValuativeRel
open LocalFieldTheory RamificationTheory CyclicCohomology KummerTheory
open ClassFormation
section UnramifiedPrimeClass
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] [IsGalois K L]
  [Valuation.HasExtension (ValuativeRel.valuation K)
    (ValuativeRel.valuation L)]
variable
  [LocalFieldTheory.IsNonarchimedeanLocalField.IsUnramifiedValuedExtension K L]
omit [IsUniformAddGroup L] in
Lean source · statement
theorem normClass_localAbstractPrimeFieldUnit_eq_uniformizer :
    normClass K L (localAbstractPrimeFieldUnit K) =
      normClass K L
        (inverseIntegerRingUniformizerFieldUnit K)
theorem

localArtinMonoidHom_localAbstractPrimeFieldUnit

L204 ↗
LocalClassFieldTheory.localArtinMonoidHom_localAbstractPrimeFieldUnit
Documentation

The canonical norm-residue symbol sends the transported abstract prime to the arithmetic Frobenius class.

Source context 9 commands

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

noncomputable section
namespace LocalClassFieldTheory
open scoped IsMulCommutative ValuativeRel
open LocalFieldTheory RamificationTheory CyclicCohomology KummerTheory
open ClassFormation
section UnramifiedPrimeClass
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] [IsGalois K L]
  [Valuation.HasExtension (ValuativeRel.valuation K)
    (ValuativeRel.valuation L)]
variable
  [LocalFieldTheory.IsNonarchimedeanLocalField.IsUnramifiedValuedExtension K L]
omit [IsUniformAddGroup L] in
Lean source · statement
theorem localArtinMonoidHom_localAbstractPrimeFieldUnit :
    localArtinMonoidHom K L (localAbstractPrimeFieldUnit K) =
      Abelianization.of
        (arithmeticFrobeniusOfUnramifiedValuation K L)
theorem

abelianizationEquivNormQuotient_symm_eq_unramifiedLocalReciprocityIso

L308 ↗
LocalClassFieldTheory.abelianizationEquivNormQuotient_symm_eq_unramifiedLocalReciprocityIso
Documentation

On an unramified extension, the inverse of the canonical reciprocity isomorphism is exactly the field-facing Frobenius-normalized isomorphism.

Source context 8 commands

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

noncomputable section
namespace LocalClassFieldTheory
open scoped IsMulCommutative ValuativeRel
open LocalFieldTheory RamificationTheory CyclicCohomology KummerTheory
open ClassFormation
section UnramifiedPrimeClass
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] [IsGalois K L]
  [Valuation.HasExtension (ValuativeRel.valuation K)
    (ValuativeRel.valuation L)]
variable
  [LocalFieldTheory.IsNonarchimedeanLocalField.IsUnramifiedValuedExtension K L]
Lean source · statement
theorem abelianizationEquivNormQuotient_symm_eq_unramifiedLocalReciprocityIso :
    (abelianizationEquivNormQuotient K L).symm =
      unramifiedLocalReciprocityIso K L
theorem

localArtinMonoidHom_eq_unramifiedLocalArtinMap

L362 ↗
LocalClassFieldTheory.localArtinMonoidHom_eq_unramifiedLocalArtinMap
Documentation

The canonical local norm-residue symbol is the field-facing unramified Artin map.

Source context 8 commands

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

noncomputable section
namespace LocalClassFieldTheory
open scoped IsMulCommutative ValuativeRel
open LocalFieldTheory RamificationTheory CyclicCohomology KummerTheory
open ClassFormation
section UnramifiedPrimeClass
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] [IsGalois K L]
  [Valuation.HasExtension (ValuativeRel.valuation K)
    (ValuativeRel.valuation L)]
variable
  [LocalFieldTheory.IsNonarchimedeanLocalField.IsUnramifiedValuedExtension K L]
Lean source · statement
theorem localArtinMonoidHom_eq_unramifiedLocalArtinMap :
    localArtinMonoidHom K L =
      unramifiedLocalArtinMap K L
theorem

localArtinMonoidHom_inverseIntegerRingUniformizerFieldUnit

L375 ↗
LocalClassFieldTheory.localArtinMonoidHom_inverseIntegerRingUniformizerFieldUnit
Documentation

Frobenius normalization on the chosen inverse prime element.

Source context 8 commands

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

noncomputable section
namespace LocalClassFieldTheory
open scoped IsMulCommutative ValuativeRel
open LocalFieldTheory RamificationTheory CyclicCohomology KummerTheory
open ClassFormation
section UnramifiedPrimeClass
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] [IsGalois K L]
  [Valuation.HasExtension (ValuativeRel.valuation K)
    (ValuativeRel.valuation L)]
variable
  [LocalFieldTheory.IsNonarchimedeanLocalField.IsUnramifiedValuedExtension K L]
Lean source · statement
theorem localArtinMonoidHom_inverseIntegerRingUniformizerFieldUnit :
    localArtinMonoidHom K L
        (inverseIntegerRingUniformizerFieldUnit K) =
      Abelianization.of
        (arithmeticFrobeniusOfUnramifiedValuation K L)
theorem

localArtinMonoidHom_eq_frobenius_zpow

L392 ↗
LocalClassFieldTheory.localArtinMonoidHom_eq_frobenius_zpow
Documentation

Full unramified Artin formula for the canonical local norm-residue symbol.

Source context 8 commands

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

noncomputable section
namespace LocalClassFieldTheory
open scoped IsMulCommutative ValuativeRel
open LocalFieldTheory RamificationTheory CyclicCohomology KummerTheory
open ClassFormation
section UnramifiedPrimeClass
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] [IsGalois K L]
  [Valuation.HasExtension (ValuativeRel.valuation K)
    (ValuativeRel.valuation L)]
variable
  [LocalFieldTheory.IsNonarchimedeanLocalField.IsUnramifiedValuedExtension K L]
Lean source · statement
theorem localArtinMonoidHom_eq_frobenius_zpow (x : Kˣ) :
    localArtinMonoidHom K L x =
      (Abelianization.of
        (arithmeticFrobeniusOfUnramifiedValuation K L)) ^
          LocalFieldTheory.IsNonarchimedeanLocalField.valuationMap K
            (Additive.ofMul x)
theorem

localArtinMap_eq_frobenius_zpow

L405 ↗
LocalClassFieldTheory.localArtinMap_eq_frobenius_zpow
Documentation

The continuous local Artin map sends every field unit to the topological class of arithmetic Frobenius raised to its normalized valuation.

Source context 8 commands

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

noncomputable section
namespace LocalClassFieldTheory
open scoped IsMulCommutative ValuativeRel
open LocalFieldTheory RamificationTheory CyclicCohomology KummerTheory
open ClassFormation
section UnramifiedPrimeClass
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] [IsGalois K L]
  [Valuation.HasExtension (ValuativeRel.valuation K)
    (ValuativeRel.valuation L)]
variable
  [LocalFieldTheory.IsNonarchimedeanLocalField.IsUnramifiedValuedExtension K L]
Lean source · statement
theorem localArtinMap_eq_frobenius_zpow (x : Kˣ) :
    localArtinMap K L x =
      (topologicalAbelianization_finite_equiv K L
        (Abelianization.of
          (arithmeticFrobeniusOfUnramifiedValuation K L))) ^
            LocalFieldTheory.IsNonarchimedeanLocalField.valuationMap K
              (Additive.ofMul x)
theorem

localArtinMap_localAbstractPrimeFieldUnit

L429 ↗
LocalClassFieldTheory.localArtinMap_localAbstractPrimeFieldUnit
Documentation

The transported canonical abstract prime maps to arithmetic Frobenius in the topological abelianization.

Source context 9 commands

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

noncomputable section
namespace LocalClassFieldTheory
open scoped IsMulCommutative ValuativeRel
open LocalFieldTheory RamificationTheory CyclicCohomology KummerTheory
open ClassFormation
section UnramifiedPrimeClass
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] [IsGalois K L]
  [Valuation.HasExtension (ValuativeRel.valuation K)
    (ValuativeRel.valuation L)]
variable
  [LocalFieldTheory.IsNonarchimedeanLocalField.IsUnramifiedValuedExtension K L]
omit [IsUniformAddGroup L] in
Lean source · statement
theorem localArtinMap_localAbstractPrimeFieldUnit :
    localArtinMap K L (localAbstractPrimeFieldUnit K) =
      topologicalAbelianization_finite_equiv K L
        (Abelianization.of
          (arithmeticFrobeniusOfUnramifiedValuation K L))
theorem

localArtinMap_uniformizer

L446 ↗
LocalClassFieldTheory.localArtinMap_uniformizer
Documentation

A chosen inverse DVR uniformizer maps to arithmetic Frobenius.

Source context 8 commands

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

noncomputable section
namespace LocalClassFieldTheory
open scoped IsMulCommutative ValuativeRel
open LocalFieldTheory RamificationTheory CyclicCohomology KummerTheory
open ClassFormation
section UnramifiedPrimeClass
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] [IsGalois K L]
  [Valuation.HasExtension (ValuativeRel.valuation K)
    (ValuativeRel.valuation L)]
variable
  [LocalFieldTheory.IsNonarchimedeanLocalField.IsUnramifiedValuedExtension K L]
Lean source · statement
theorem localArtinMap_uniformizer :
    localArtinMap K L (inverseIntegerRingUniformizerFieldUnit K) =
      topologicalAbelianization_finite_equiv K L
        (Abelianization.of
          (arithmeticFrobeniusOfUnramifiedValuation K L))
theorem

localArtinMap_eq_one_of_valuationMap_eq_zero

L457 ↗
LocalClassFieldTheory.localArtinMap_eq_one_of_valuationMap_eq_zero
Documentation

Elements of normalized valuation zero lie in the kernel of the unramified local Artin map.

Source context 8 commands

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

noncomputable section
namespace LocalClassFieldTheory
open scoped IsMulCommutative ValuativeRel
open LocalFieldTheory RamificationTheory CyclicCohomology KummerTheory
open ClassFormation
section UnramifiedPrimeClass
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] [IsGalois K L]
  [Valuation.HasExtension (ValuativeRel.valuation K)
    (ValuativeRel.valuation L)]
variable
  [LocalFieldTheory.IsNonarchimedeanLocalField.IsUnramifiedValuedExtension K L]
Lean source · statement
theorem localArtinMap_eq_one_of_valuationMap_eq_zero
    (x : Kˣ)
    (hx : LocalFieldTheory.IsNonarchimedeanLocalField.valuationMap K
      (Additive.ofMul x) = 0) :
    localArtinMap K L x = 1
theorem

localArtinMap_units_unramified

L469 ↗
LocalClassFieldTheory.localArtinMap_units_unramified
Documentation

Every valuation-ring unit has trivial unramified Artin symbol.

Source context 9 commands

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

noncomputable section
namespace LocalClassFieldTheory
open scoped IsMulCommutative ValuativeRel
open LocalFieldTheory RamificationTheory CyclicCohomology KummerTheory
open ClassFormation
section UnramifiedPrimeClass
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] [IsGalois K L]
  [Valuation.HasExtension (ValuativeRel.valuation K)
    (ValuativeRel.valuation L)]
variable
  [LocalFieldTheory.IsNonarchimedeanLocalField.IsUnramifiedValuedExtension K L]
open _root_.LocalFieldTheory.IsNonarchimedeanLocalField (
  integerUnitsToFieldUnits
) in
Lean source · statement
theorem localArtinMap_units_unramified (u : 𝒪[K]ˣ) :
    localArtinMap K L (integerUnitsToFieldUnits K u) = 1
theorem

abelianLocalArtinMonoidHom_eq_frobenius_zpow

L491 ↗
LocalClassFieldTheory.abelianLocalArtinMonoidHom_eq_frobenius_zpow
Documentation

The canonical local Artin map for an abelian unramified extension sends each field unit to actual arithmetic Frobenius raised to its normalized valuation.

Source context 7 commands

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

noncomputable section
namespace LocalClassFieldTheory
open scoped IsMulCommutative ValuativeRel
open LocalFieldTheory RamificationTheory CyclicCohomology KummerTheory
open ClassFormation
section AbelianUnramifiedPrimeClass
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 abelianLocalArtinMonoidHom_eq_frobenius_zpow (x : Kˣ) :
    abelianLocalArtinMonoidHom K L x =
      (arithmeticFrobeniusOfUnramifiedValuation K L) ^
        LocalFieldTheory.IsNonarchimedeanLocalField.valuationMap K
          (Additive.ofMul x)
theorem

finiteAbelianLocalArtinMap_eq_frobenius_zpow

L517 ↗
ClassFieldTheory.finiteAbelianLocalArtinMap_eq_frobenius_zpow
Documentation

The canonical Artin map of an abelian unramified local extension is arithmetic Frobenius raised to the normalized valuation.

Source context 3 commands

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

noncomputable section
namespace ClassFieldTheory
open scoped ValuativeRel
Lean source · statement
theorem finiteAbelianLocalArtinMap_eq_frobenius_zpow
    (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]
    (x : Kˣ) :
    LocalClassFieldTheory.abelianLocalArtinMap K L x =
      (LocalFieldTheory.arithmeticFrobeniusOfUnramifiedValuation K L) ^
        LocalFieldTheory.IsNonarchimedeanLocalField.valuationMap K
          (Additive.ofMul x)
theorem

finiteAbelianLocalArtinMap_uniformizer

L542 ↗
ClassFieldTheory.finiteAbelianLocalArtinMap_uniformizer
Documentation

Every element of normalized valuation one maps to arithmetic Frobenius; there is no further choice of an Artin map at this finite level.

Source context 3 commands

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

noncomputable section
namespace ClassFieldTheory
open scoped ValuativeRel
Lean source · statement
theorem finiteAbelianLocalArtinMap_uniformizer
    (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]
    (π : Kˣ)
    (hπ : LocalFieldTheory.IsNonarchimedeanLocalField.valuationMap K
      (Additive.ofMul π) = 1) :
    LocalClassFieldTheory.abelianLocalArtinMap K L π =
      LocalFieldTheory.arithmeticFrobeniusOfUnramifiedValuation K L
theorem

finiteAbelianLocalArtinMap_inverseUniformizer_residue_pow

L563 ↗
ClassFieldTheory.finiteAbelianLocalArtinMap_inverseUniformizer_residue_pow
Documentation

At an inverse uniformizer, the normalized local Artin automorphism acts on the residue field by the arithmetic q-power Frobenius. This states the normalization through the reduction of integral elements, without exposing the implementation's chosen residue-field automorphism in the conclusion.

Source context 3 commands

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

noncomputable section
namespace ClassFieldTheory
open scoped ValuativeRel
Lean source · statement
theorem finiteAbelianLocalArtinMap_inverseUniformizer_residue_pow
    (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]
    (π : Kˣ)
    (hπ : LocalFieldTheory.IsNonarchimedeanLocalField.valuationMap K
      (Additive.ofMul π) = 1)
    (x : 𝒪[L]) :
    ∃ z : 𝒪[L],
      (z : L) = (LocalClassFieldTheory.abelianLocalArtinMap K L π) (x : L) ∧
        IsLocalRing.residue 𝒪[L] z =
          (IsLocalRing.residue 𝒪[L] x) ^ Nat.card 𝓀[K]

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.