ClassFieldTheory.globalHilbertPairingFamilyCongr_productFormula
The Hilbert product formula survives transport of the local-pairing family across a number-field equivalence.
Source context 5 commands
Surrounding namespaces, section variables, and local commands at this declaration.
open scoped BigOperators NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace ClassFieldTheory
universe u vLean source · statement
theorem globalHilbertPairingFamilyCongr_productFormula
{F : Type u} {G : Type v}
[Field F] [NumberField F] [Field G] [NumberField G]
(e : F ≃ₐ[ℚ] G) (n : ℕ+)
(hmuF : (primitiveRoots (n : ℕ) F).Nonempty)
(hmuG : (primitiveRoots (n : ℕ) G).Nonempty)
(BF : GlobalHilbertPairingFamily F n)
(hBF : ∀ a b : Fˣ,
(∏ v : InfinitePlace F,
globalInfinitePlaceHilbertSymbol F n v a b) *
∏ᶠ v : HeightOneSpectrum (𝓞 F),
GlobalHilbertPairingFamily.finiteFactor F BF hmuF v a b = 1) :
∀ a b : Gˣ,
(∏ W : InfinitePlace G,
globalInfinitePlaceHilbertSymbol G n W a b) *
∏ᶠ W : HeightOneSpectrum (𝓞 G),
GlobalHilbertPairingFamily.finiteFactor G
(globalHilbertPairingFamilyCongr e n hmuF BF) hmuG W a b = 1