NYLL
Module

LocalHilbertPairingExists.lean

Nyll.ClassFieldTheory.Theorems.HilbertSymbols.LocalHilbertPairingExists
1 declaration indexed from sourceView source ↗

Module documentation

Existence of the local Hilbert pairing

Let K be a nonarchimedean local field containing the n-th roots of unity, with n nonzero in K. The local Hilbert symbol descends to a bimultiplicative pairing

Kˣ / (Kˣ)^n × Kˣ / (Kˣ)^n → μₙ(K).

The theorem below records the pairing laws without naming a particular implementation of local reciprocity in its statement. Its proof imports the implementation layer. The witness satisfies the Steinberg relation, skew-symmetry, nondegeneracy in both variables, and the Kummer norm-residue vanishing criterion. Multiplicativity is already part of the type HilbertPairing K n. These properties still leave the harmless choice of a normalization of the values in μₙ explicit.

Imports4
Imported by2

Declarations

theorem

exists_localHilbertPairing

L37 ↗
ClassFieldTheory.exists_localHilbertPairing
Documentation

A nonarchimedean local field containing the n-th roots of unity admits a nondegenerate, skew-symmetric Hilbert pairing satisfying the Steinberg and Kummer norm-residue laws.

Source context 2 commands

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

namespace ClassFieldTheory
universe u
Lean source · statement
theorem exists_localHilbertPairing
    (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,
      HilbertPairing.IsLocalHilbertPairing B

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.