Module

LocalHilbertExponentCompatibility.lean

Nyll.ClassFieldTheory.LocalClassFieldTheory.Kummer.LocalHilbertExponentCompatibility

1 declaration indexed from sourceView source ↗

Module documentation

Compatibility of local Hilbert symbols at divisible exponents

The source Hilbert symbol uses its first argument as the local Artin input and its second as the Kummer radical. Artin restriction along the actual simple Kummer tower makes its values compatible as the exponent varies.

Imports3

Imported by2

theorem

localHilbertSymbol_exponentCompatibility

L27 ↗

LocalClassFieldTheory.Kummer.localHilbertSymbol_exponentCompatibility

Documentation

If m ∣ n, the exponent-m Hilbert value is the (n/m)-th power of the exponent-n value, compared as units of the base field.

Source context 3 commands

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

noncomputable section
namespace LocalClassFieldTheory.Kummer
open RamificationTheory

Lean source · statement

theorem localHilbertSymbol_exponentCompatibility
    (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K]
    [IsNonarchimedeanLocalField K]
    (m n : ℕ+) (hmK : ((m : ℕ) : K) ≠ 0)
    (hnK : ((n : ℕ) : K) ≠ 0)
    (hmuM : (primitiveRoots (m : ℕ) K).Nonempty)
    (hmuN : (primitiveRoots (n : ℕ) K).Nonempty)
    (hmn : (m : ℕ) ∣ (n : ℕ)) (a b : Kˣ) :
    (localHilbertSymbol K m hmK hmuM a b).1 =
      (localHilbertSymbol K n hnK hmuN a b).1 ^ ((n : ℕ) / (m : ℕ))

Module documentation

Compatibility of local Hilbert symbols at divisible exponents

Declarations

localHilbertSymbol_exponentCompatibility