Module

HilbertProductFormula.lean

Nyll.ClassFieldTheory.Theorems.HilbertSymbols.HilbertProductFormula

1 declaration indexed from sourceView source ↗

Module documentation

Existence of a coherent global Hilbert-pairing family

For a number field containing the n-th roots of unity, local class field theory supplies a Hilbert pairing on every finite completion. These pairings can be chosen coherently: their values on two nonzero elements of the number field have finite multiplicative support, and together with the explicit infinite-place factors they satisfy the Hilbert product formula.

The statement is existential on purpose. Mathlib provides the completions, power-class groups, and roots of unity, but it does not choose a local Artin map or a Hilbert symbol. Consequently this theorem asserts the existence of one family satisfying all the stated local pairing laws, including the Kummer norm-residue criterion, and the global formula. It does not disguise the remaining choice of a value normalization as a definition.

Imports8

Imported by2

theorem

exists_globalHilbertPairingFamily_productFormula

L44 ↗

ClassFieldTheory.exists_globalHilbertPairingFamily_productFormula

Documentation

Hilbert product formula. There is a family of local Hilbert pairings on the finite completions whose global evaluations have finite support and whose product, including the canonical infinite-place factors, is one.

Source context 4 commands

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

open scoped BigOperators NumberField
open NumberField IsDedekindDomain
namespace ClassFieldTheory
universe u

Lean source · statement

theorem exists_globalHilbertPairingFamily_productFormula
    (F : Type u) [Field F] [NumberField F]
    (n : ℕ+) (hmu : (primitiveRoots (n : ℕ) F).Nonempty) :
    ∃ B : GlobalHilbertPairingFamily F n,
      GlobalHilbertPairingFamily.IsLocallyHilbert F B ∧
      GlobalHilbertPairingFamily.HasFiniteSupport F B hmu ∧
      ∀ a b : Fˣ,
        (∏ v : InfinitePlace F,
            globalInfinitePlaceHilbertSymbol F n v a b) *
          ∏ᶠ v : HeightOneSpectrum (𝓞 F),
            GlobalHilbertPairingFamily.finiteFactor F B hmu v a b = 1

Module documentation

Existence of a coherent global Hilbert-pairing family

Declarations

exists_globalHilbertPairingFamily_productFormula