ClassFieldTheory.exists_compatibleLocalHilbertPairings_of_dvd
For m ∣ n, there are local Hilbert pairings at exponents m and n whose values satisfy (a,b)ₘ = (a,b)ₙ ^ (n/m) in the base-field unit group. Neither pairing is asserted to be determined by the algebraic laws alone.
Source context 3 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace ClassFieldTheory
universe uLean source · statement
theorem exists_compatibleLocalHilbertPairings_of_dvd
(K : Type u) [Field K] [ValuativeRel K] [TopologicalSpace K]
[IsNonarchimedeanLocalField K]
(m n : ℕ+) (hnK : ((n : ℕ) : K) ≠ 0)
(hmuN : (primitiveRoots (n : ℕ) K).Nonempty)
(hmn : (m : ℕ) ∣ (n : ℕ)) :
∃ Bm : HilbertPairing K m,
HilbertPairing.IsLocalHilbertPairing Bm ∧
∃ Bn : HilbertPairing K n,
HilbertPairing.IsLocalHilbertPairing Bn ∧
∀ a b : Kˣ,
(Bm (powerClass K m a) (powerClass K m b)).1 =
(Bn (powerClass K n a) (powerClass K n b)).1 ^
((n : ℕ) / (m : ℕ))