ClassFieldTheory.globalHilbertPairing_mulSupport_subset_finitePlaceHilbertBadSet
The finite-place factors of a locally Hilbert family are trivial where the exponent and both arguments are valuation-ring units.
Source context 4 commands
Surrounding namespaces, section variables, and local commands at this declaration.
open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace ClassFieldTheoryLean source · full declaration
theorem globalHilbertPairing_mulSupport_subset_finitePlaceHilbertBadSet
(F : Type) [Field F] [NumberField F]
(n : ℕ+) (hmu : (primitiveRoots (n : ℕ) F).Nonempty)
(B : GlobalHilbertPairingFamily F n)
(hB : GlobalHilbertPairingFamily.IsLocallyHilbert F B)
(a b : Fˣ) :
Function.mulSupport
(fun v : HeightOneSpectrum (𝓞 F) =>
GlobalHilbertPairingFamily.finiteFactor F B hmu v a b) ⊆
finitePlaceHilbertBadSet F n a b := by
intro v hv
by_contra hvBad
change ¬ (v.valuation F (a : F) ≠ 1 ∨
v.valuation F (b : F) ≠ 1 ∨
v.valuation F ((n : ℕ) : F) ≠ 1) at hvBad
have hva : v.valuation F (a : F) = 1 := by
by_contra h
exact hvBad (Or.inl h)
have hvb : v.valuation F (b : F) = 1 := by
by_contra h
exact hvBad (Or.inr (Or.inl h))
have hvn : v.valuation F ((n : ℕ) : F) = 1 := by
by_contra h
exact hvBad (Or.inr (Or.inr h))
let C := finitePlaceAdicHilbertPairingFamily F n hmu
have hC : GlobalHilbertPairingFamily.IsLocallyHilbert F C :=
finitePlaceAdicHilbertPairingFamily_isLocallyHilbert F n hmu
have hnF : ((n : ℕ) : F) ≠ 0 := Nat.cast_ne_zero.mpr n.ne_zero
have hsource :
GlobalClassFieldTheory.Reciprocity.finitePlaceHilbertSymbol
F n hnF hmu v a b = 1 :=
GlobalClassFieldTheory.Reciprocity.finitePlaceHilbertSymbol_eq_one_of_valuation_eq_one
F n hnF hmu a b v hva hvb hvn
have hCfactor :
GlobalHilbertPairingFamily.finiteFactor F C hmu v a b = 1 := by
rw [finitePlaceAdicHilbertPairingFamily_finiteFactor F n hnF hmu v a b]
change KummerTheory.nthRootsSubgroupEquivRootsOfUnity F (n : ℕ)
(GlobalClassFieldTheory.Reciprocity.finitePlaceHilbertSymbol
F n hnF hmu v a b) = 1
rw [hsource, map_one]
let : NeZero (n : ℕ) := ⟨n.ne_zero⟩
let e : rootsOfUnity (n : ℕ) F ≃*
rootsOfUnity (n : ℕ) (v.adicCompletion F) :=
rootsOfUnityEquivOfPrimitiveRoots
(algebraMap F (v.adicCompletion F)).injective hmu
let av : (v.adicCompletion F)ˣ :=
Units.map (algebraMap F (v.adicCompletion F)).toMonoidHom a
let bv : (v.adicCompletion F)ˣ :=
Units.map (algebraMap F (v.adicCompletion F)).toMonoidHom b
have hzero :
GlobalHilbertPairingFamily.finiteFactor F C hmu v a b = 1 ↔
GlobalHilbertPairingFamily.finiteFactor F B hmu v a b = 1 := by
change e.symm ((C v).symbol av bv) = 1 ↔
e.symm ((B v).symbol av bv) = 1
simp only [MulEquiv.map_eq_one_iff]
exact ((hC v).2.2.2 av bv).trans ((hB v).2.2.2 av bv).symm
exact hv (hzero.mp hCfactor)