Module

LocalUnramifiedKummerHilbertValuation.lean

Nyll.SawinTotallyRealTowers.UnramifiedProPRelationRank.Kummer.LocalUnramifiedKummerHilbertValuation

3 declarations indexed from sourceView source ↗

Module documentation

Unramified Kummer Hilbert characters and valuation

For a chosen simple Kummer extension which is unramified, its Hilbert character is a Frobenius scalar times normalized valuation. The argument uses the full unramified local Artin formula and therefore also applies at places above the Kummer exponent.

Imports4

Imported by2

def

IsUnramifiedChosenSimpleKummer

L36 ↗

ClassFieldTower.Martinet.Shafarevich.IsUnramifiedChosenSimpleKummer

Documentation

The chosen simple Kummer extension, with its canonical spectral valuation, is unramified.

Source context 8 commands

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

open scoped ValuativeRel
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open KummerTheory LocalClassFieldTheory LocalClassFieldTheory.Kummer
open LocalFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField
variable (K : Type) [Field K] [CharZero K]
variable [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K]

Lean source · statement

def IsUnramifiedChosenSimpleKummer
    (n : ℕ+) (hnK : ((n : ℕ) : K) ≠ 0) (a : Kˣ) : Prop

def

unramifiedChosenSimpleKummerFrobeniusRoot

L57 ↗

ClassFieldTower.Martinet.Shafarevich.unramifiedChosenSimpleKummerFrobeniusRoot

Documentation

Frobenius acts on the chosen Kummer root through this base-field root of unity.

Source context 8 commands

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

open scoped ValuativeRel
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open KummerTheory LocalClassFieldTheory LocalClassFieldTheory.Kummer
open LocalFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField
variable (K : Type) [Field K] [CharZero K]
variable [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K]

Lean source · statement

def unramifiedChosenSimpleKummerFrobeniusRoot
    (n : ℕ+) (hnK : ((n : ℕ) : K) ≠ 0)
    (hmu : (primitiveRoots (n : ℕ) K).Nonempty) (a : Kˣ)
    (ha : IsUnramifiedChosenSimpleKummer K n hnK a) :
    nthRootsSubgroup K (n : ℕ)

theorem

localHilbertSymbol_eq_unramifiedFrobenius_zpow

L89 ↗

ClassFieldTower.Martinet.Shafarevich.localHilbertSymbol_eq_unramifiedFrobenius_zpow

Documentation

For any unramified chosen simple Kummer extension, the Hilbert character of its radical is a Frobenius scalar times normalized valuation. No tame residue-characteristic hypothesis is used.

Source context 9 commands

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

open scoped ValuativeRel
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open KummerTheory LocalClassFieldTheory LocalClassFieldTheory.Kummer
open LocalFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField
variable (K : Type) [Field K] [CharZero K]
variable [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K]
omit [CharZero K] in

Lean source · statement

theorem localHilbertSymbol_eq_unramifiedFrobenius_zpow
    (n : ℕ+) (hnK : ((n : ℕ) : K) ≠ 0)
    (hmu : (primitiveRoots (n : ℕ) K).Nonempty)
    (a b : Kˣ) (ha : IsUnramifiedChosenSimpleKummer K n hnK a) :
    localHilbertSymbol K n hnK hmu a b =
      (unramifiedChosenSimpleKummerFrobeniusRoot K n hnK hmu a ha) ^
        (-valuationMap K (Additive.ofMul b))

Module documentation

Unramified Kummer Hilbert characters and valuation

Declarations

IsUnramifiedChosenSimpleKummer

unramifiedChosenSimpleKummerFrobeniusRoot

localHilbertSymbol_eq_unramifiedFrobenius_zpow