Module

LocalHilbertPairingPerfectExists.lean

Nyll.ClassFieldTheory.Theorems.HilbertSymbols.LocalHilbertPairingPerfectExists

1 declaration indexed from sourceView source ↗

Module documentation

A perfect local Hilbert pairing

For a nonarchimedean local field in which n is nonzero and the n-th roots of unity are present, the Hilbert pairing identifies power classes with all μₙ-valued characters of the power-class group.

Imports5

Imported by1

Nyll.ClassFieldTheory.Theorems.HilbertSymbols.All

theorem

exists_perfectLocalHilbertPairing

L27 ↗

ClassFieldTheory.exists_perfectLocalHilbertPairing

Documentation

There is a local Hilbert pairing whose adjoint map to the full μₙ-valued character group is bijective.

Source context 2 commands

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

namespace ClassFieldTheory
universe u

Lean source · statement

theorem exists_perfectLocalHilbertPairing
    (K : Type u) [Field K] [ValuativeRel K] [TopologicalSpace K]
    [IsNonarchimedeanLocalField K]
    (n : ℕ+) (hnK : ((n : ℕ) : K) ≠ 0)
    (hmu : (primitiveRoots (n : ℕ) K).Nonempty) :
    ∃ B : HilbertPairing K n,
      B.IsLocalHilbertPairing ∧ Function.Bijective B

Module documentation

A perfect local Hilbert pairing

Declarations

exists_perfectLocalHilbertPairing