ClassFieldTheory.globalHilbertPairingFamily_finiteFactor_congr
Transporting a local Hilbert pairing through a compatible equivalence of completions transports its finite factor through the equivalence of global roots of unity.
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 vLean source · statement
theorem globalHilbertPairingFamily_finiteFactor_congr
{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)
(v : HeightOneSpectrum (𝓞 F)) (W : HeightOneSpectrum (𝓞 G))
(ec : v.adicCompletion F ≃+* W.adicCompletion G)
(hcomm : ∀ x : F,
ec (algebraMap F (v.adicCompletion F) x) =
algebraMap G (W.adicCompletion G) (e x))
(hmuC : (primitiveRoots (n : ℕ) (v.adicCompletion F)).Nonempty)
(BF : GlobalHilbertPairingFamily F n)
(BG : GlobalHilbertPairingFamily G n)
(hB : BG W = hilbertPairingOfRingEquiv ec n hmuC (BF v))
(a b : Fˣ) :
rootsOfUnityEquivOfRingEquiv e n hmuF
(GlobalHilbertPairingFamily.finiteFactor F BF hmuF v a b) =
GlobalHilbertPairingFamily.finiteFactor G BG hmuG W
(Units.mapEquiv e.toMulEquiv a)
(Units.mapEquiv e.toMulEquiv b)