Module

UnramifiedReciprocity.lean

Nyll.ClassFieldTheory.LocalClassFieldTheory.Finite.LocalReciprocity.UnramifiedReciprocity

11 declarations indexed from sourceView source ↗

Module documentation

Unramified reciprocity

For a finite unramified Galois extension, this module composes the actual norm quotient with its normalized valuation model, the generator-normalized Frobenius model of the Galois group, and the canonical equivalence with the abelianization of that cyclic group.

Imports2

Imported by3

def

unramifiedLocalReciprocityIsoToGaloisGroup

L31 ↗

LocalClassFieldTheory.unramifiedLocalReciprocityIsoToGaloisGroup

Documentation

The actual unramified local reciprocity equivalence with target GaloisGroup. The norm-subgroup equality and the Frobenius/ZMod normalization are generated internally from the preceding source lemmas, not passed as hypotheses.

Source context 5 commands

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

noncomputable section
namespace LocalClassFieldTheory
open scoped ValuativeRel
open LocalFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField

Lean source · statement

def unramifiedLocalReciprocityIsoToGaloisGroup
    (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)]
    [IsIntegralClosure 𝒪[L] 𝒪[K] L]
    [Module.Finite 𝒪[K] 𝒪[L]]
    [IsUnramifiedValuedExtension K L] :
    NormQuotient K L ≃* Gal(L / K)

theorem

unramifiedLocalReciprocityIsoToGaloisGroup_inverseIntegerRingUniformizerFieldUnit

L47 ↗

LocalClassFieldTheory.unramifiedLocalReciprocityIsoToGaloisGroup_inverseIntegerRingUniformizerFieldUnit

Documentation

The chosen inverse prime element maps to the arithmetic Frobenius under the actual reciprocity equivalence.

Source context 5 commands

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

noncomputable section
namespace LocalClassFieldTheory
open scoped ValuativeRel
open LocalFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField

Lean source · statement

theorem unramifiedLocalReciprocityIsoToGaloisGroup_inverseIntegerRingUniformizerFieldUnit
    (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)]
    [IsIntegralClosure 𝒪[L] 𝒪[K] L]
    [Module.Finite 𝒪[K] 𝒪[L]]
    [IsUnramifiedValuedExtension K L] :
    unramifiedLocalReciprocityIsoToGaloisGroup K L
        (normClass K L (inverseIntegerRingUniformizerFieldUnit K)) =
      arithmeticFrobeniusOfUnramifiedValuation K L

theorem

unramifiedLocalReciprocityIsoToGaloisGroup_inverseIntegerRingUniformizerFieldUnit_zpow

L74 ↗

LocalClassFieldTheory.unramifiedLocalReciprocityIsoToGaloisGroup_inverseIntegerRingUniformizerFieldUnit_zpow

Documentation

Power form of the unramified reciprocity calculation for the chosen inverse prime element.

Source context 5 commands

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

noncomputable section
namespace LocalClassFieldTheory
open scoped ValuativeRel
open LocalFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField

Lean source · statement

theorem unramifiedLocalReciprocityIsoToGaloisGroup_inverseIntegerRingUniformizerFieldUnit_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] [IsGalois K L]
    [Valuation.HasExtension (ValuativeRel.valuation K) (ValuativeRel.valuation L)]
    [IsIntegralClosure 𝒪[L] 𝒪[K] L]
    [Module.Finite 𝒪[K] 𝒪[L]]
    [IsUnramifiedValuedExtension K L] (m : Int) :
    unramifiedLocalReciprocityIsoToGaloisGroup K L
        ((normClass K L (inverseIntegerRingUniformizerFieldUnit K)) ^ m) =
      (arithmeticFrobeniusOfUnramifiedValuation K L) ^ m

theorem

unramifiedLocalReciprocityIsoToGaloisGroup_normClass

L92 ↗

LocalClassFieldTheory.unramifiedLocalReciprocityIsoToGaloisGroup_normClass

Documentation

The actual reciprocity equivalence to GaloisGroup sends any field unit class to the corresponding power of arithmetic Frobenius, with exponent its normalized valuation.

Source context 5 commands

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

noncomputable section
namespace LocalClassFieldTheory
open scoped ValuativeRel
open LocalFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField

Lean source · statement

theorem unramifiedLocalReciprocityIsoToGaloisGroup_normClass
    (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)]
    [IsIntegralClosure 𝒪[L] 𝒪[K] L]
    [Module.Finite 𝒪[K] 𝒪[L]]
    [IsUnramifiedValuedExtension K L] (x : Kˣ) :
    unramifiedLocalReciprocityIsoToGaloisGroup K L (normClass K L x) =
      (arithmeticFrobeniusOfUnramifiedValuation K L) ^
        LocalFieldTheory.IsNonarchimedeanLocalField.valuationMap K (Additive.ofMul x)

def

unramifiedLocalReciprocityIso

L120 ↗

LocalClassFieldTheory.unramifiedLocalReciprocityIso

Documentation

The actual unramified local reciprocity equivalence with abelianized target. It composes the valuation quotient and normalized Frobenius model, then passes to the abelianization of the cyclic Galois group.

Source context 5 commands

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

noncomputable section
namespace LocalClassFieldTheory
open scoped ValuativeRel
open LocalFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField

Lean source · statement

def unramifiedLocalReciprocityIso
    (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)]
    [IsIntegralClosure 𝒪[L] 𝒪[K] L]
    [Module.Finite 𝒪[K] 𝒪[L]]
    [IsUnramifiedValuedExtension K L] :
    NormQuotient K L ≃* Abelianization (Gal(L / K))

theorem

unramifiedLocalReciprocityIso_inverseIntegerRingUniformizerFieldUnit

L136 ↗

LocalClassFieldTheory.unramifiedLocalReciprocityIso_inverseIntegerRingUniformizerFieldUnit

Documentation

With abelianized target, the chosen inverse prime element maps to the class of the arithmetic Frobenius.

Source context 5 commands

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

noncomputable section
namespace LocalClassFieldTheory
open scoped ValuativeRel
open LocalFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField

Lean source · statement

theorem unramifiedLocalReciprocityIso_inverseIntegerRingUniformizerFieldUnit
    (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)]
    [IsIntegralClosure 𝒪[L] 𝒪[K] L]
    [Module.Finite 𝒪[K] 𝒪[L]]
    [IsUnramifiedValuedExtension K L] :
    unramifiedLocalReciprocityIso K L
        (normClass K L (inverseIntegerRingUniformizerFieldUnit K)) =
      Abelianization.of (arithmeticFrobeniusOfUnramifiedValuation K L)

theorem

unramifiedLocalReciprocityIso_inverseIntegerRingUniformizerFieldUnit_zpow

L158 ↗

LocalClassFieldTheory.unramifiedLocalReciprocityIso_inverseIntegerRingUniformizerFieldUnit_zpow

Documentation

Power form of the unramified reciprocity calculation with abelianized target.

Source context 5 commands

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

noncomputable section
namespace LocalClassFieldTheory
open scoped ValuativeRel
open LocalFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField

Lean source · statement

theorem unramifiedLocalReciprocityIso_inverseIntegerRingUniformizerFieldUnit_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] [IsGalois K L]
    [Valuation.HasExtension (ValuativeRel.valuation K) (ValuativeRel.valuation L)]
    [IsIntegralClosure 𝒪[L] 𝒪[K] L]
    [Module.Finite 𝒪[K] 𝒪[L]]
    [IsUnramifiedValuedExtension K L] (m : Int) :
    unramifiedLocalReciprocityIso K L
        ((normClass K L (inverseIntegerRingUniformizerFieldUnit K)) ^ m) =
      (Abelianization.of (arithmeticFrobeniusOfUnramifiedValuation K L)) ^ m

theorem

unramifiedLocalReciprocityIso_normClass

L176 ↗

LocalClassFieldTheory.unramifiedLocalReciprocityIso_normClass

Documentation

The unramified reciprocity map on a general field unit is the arithmetic Frobenius class raised to the normalized valuation.

Source context 5 commands

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

noncomputable section
namespace LocalClassFieldTheory
open scoped ValuativeRel
open LocalFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField

Lean source · statement

theorem unramifiedLocalReciprocityIso_normClass
    (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)]
    [IsIntegralClosure 𝒪[L] 𝒪[K] L]
    [Module.Finite 𝒪[K] 𝒪[L]]
    [IsUnramifiedValuedExtension K L] (x : Kˣ) :
    unramifiedLocalReciprocityIso K L (normClass K L x) =
      (Abelianization.of (arithmeticFrobeniusOfUnramifiedValuation K L)) ^
        LocalFieldTheory.IsNonarchimedeanLocalField.valuationMap K (Additive.ofMul x)

def

unramifiedLocalArtinMap

L200 ↗

LocalClassFieldTheory.unramifiedLocalArtinMap

Documentation

The actual unramified Artin map induced by the certificate-free reciprocity equivalence. This avoids introducing LocalReciprocityDataReal as an assumption package.

Source context 5 commands

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

noncomputable section
namespace LocalClassFieldTheory
open scoped ValuativeRel
open LocalFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField

Lean source · statement

def unramifiedLocalArtinMap
    (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)]
    [IsIntegralClosure 𝒪[L] 𝒪[K] L]
    [Module.Finite 𝒪[K] 𝒪[L]]
    [IsUnramifiedValuedExtension K L] :
    Kˣ →* Abelianization (Gal(L / K))

theorem

unramifiedLocalArtinMap_apply

L214 ↗

LocalClassFieldTheory.unramifiedLocalArtinMap_apply

Documentation

States the theorem unramifiedLocalArtinMap_apply.

Source context 5 commands

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

noncomputable section
namespace LocalClassFieldTheory
open scoped ValuativeRel
open LocalFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField

Lean source · statement

theorem unramifiedLocalArtinMap_apply
    (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)]
    [IsIntegralClosure 𝒪[L] 𝒪[K] L]
    [Module.Finite 𝒪[K] 𝒪[L]]
    [IsUnramifiedValuedExtension K L] (x : Kˣ) :
    unramifiedLocalArtinMap K L x =
      unramifiedLocalReciprocityIso K L (normClass K L x)

theorem

unramifiedLocalArtinMap_eq_frobenius_zpow

L230 ↗

LocalClassFieldTheory.unramifiedLocalArtinMap_eq_frobenius_zpow

Documentation

In the arithmetic-Frobenius convention, the actual local Artin map sends x to the arithmetic Frobenius class raised to v_K(x).

Source context 5 commands

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

noncomputable section
namespace LocalClassFieldTheory
open scoped ValuativeRel
open LocalFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField

Lean source · statement

theorem unramifiedLocalArtinMap_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] [IsGalois K L]
    [Valuation.HasExtension (ValuativeRel.valuation K) (ValuativeRel.valuation L)]
    [IsIntegralClosure 𝒪[L] 𝒪[K] L]
    [Module.Finite 𝒪[K] 𝒪[L]]
    [IsUnramifiedValuedExtension K L] (x : Kˣ) :
    unramifiedLocalArtinMap K L x =
      (Abelianization.of (arithmeticFrobeniusOfUnramifiedValuation K L)) ^
        LocalFieldTheory.IsNonarchimedeanLocalField.valuationMap K (Additive.ofMul x)

Module documentation

Unramified reciprocity

Declarations