Module

GlobalHilbertPairingFiniteSupport.lean

Nyll.ClassFieldTheory.Theorems.HilbertSymbols.GlobalHilbertPairingFiniteSupport

1 declaration indexed from sourceView source ↗

Module documentation

Finite support of every local Hilbert-pairing family

The norm-residue criterion determines exactly where a local symbol equals one, even though it does not determine the symbol's other values. Hence the finite support of one constructed family transfers to every family satisfying the local Hilbert-pairing laws. No product-formula assumption is made about the family being studied.

Imports2

Imported by1

Nyll.ClassFieldTheory.Theorems.HilbertSymbols.All

theorem

globalHilbertPairing_hasFiniteSupport_of_isLocallyHilbert

L31 ↗

ClassFieldTheory.globalHilbertPairing_hasFiniteSupport_of_isLocallyHilbert

Documentation

The local norm-residue law alone forces finite support of the finite-place values on any fixed pair of nonzero global elements.

Source context 5 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace ClassFieldTheory
universe u

Lean source · statement

theorem globalHilbertPairing_hasFiniteSupport_of_isLocallyHilbert
    (F : Type u) [Field F] [NumberField F]
    (n : ℕ+) (hmu : (primitiveRoots (n : ℕ) F).Nonempty)
    (B : GlobalHilbertPairingFamily F n)
    (hB : GlobalHilbertPairingFamily.IsLocallyHilbert F B) :
    GlobalHilbertPairingFamily.HasFiniteSupport F B hmu

Module documentation

Finite support of every local Hilbert-pairing family

Declarations

globalHilbertPairing_hasFiniteSupport_of_isLocallyHilbert