Module

UnramifiedNormalization.lean

Nyll.ClassFieldTheory.GlobalClassFieldTheory.Reciprocity.FinitePlaceArtin.UnramifiedNormalization

2 declarations indexed from sourceView source ↗

Module documentation

Unramified normalization of the chosen finite-place Artin map

The chosen order-one input has normalized local valuation -1 in the geometric finite-place construction. Its local Artin image is therefore inverse arithmetic Frobenius in the actual chosen completion.

Imports3

Imported by2

def

chosenFinitePlaceLocalArithmeticFrobenius

L36 ↗

GlobalClassFieldTheory.Reciprocity.chosenFinitePlaceLocalArithmeticFrobenius

Documentation

Arithmetic Frobenius of the actual chosen unramified local extension.

Source context 7 commands

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

open scoped NumberField ValuativeRel
open NumberField IsDedekindDomain
open AlgebraicNumberTheory.Valuations LocalFieldTheory
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
variable {K L : Type}
    [Field K] [NumberField K]
    [Field L] [Algebra K L]
    [hKLfinite : FiniteDimensional K L] [IsAbelianGalois K L]

Lean source · statement

def chosenFinitePlaceLocalArithmeticFrobenius
    (v : HeightOneSpectrum (𝓞 K))
    (hunram : ChosenFinitePlaceIsUnramified (K := K) (L := L) v) :
    ChosenFinitePlaceLocalizedCompletion (K := K) (L := L) v ≃ₐ[
      ChosenFinitePlaceBaseCompletion (K := K) v]
      ChosenFinitePlaceLocalizedCompletion (K := K) (L := L) v

theorem

chosenFinitePlaceLocalArtin_eq_arithmeticFrobenius_inv_of_unramified

L59 ↗

GlobalClassFieldTheory.Reciprocity.chosenFinitePlaceLocalArtin_eq_arithmeticFrobenius_inv_of_unramified