Comparing the two mod-two Kummer cups

The Kummer cup with roots-of-unity coefficients and the cup with trivial 𝔽₂ coefficients have the same vanishing criterion. The coefficient dictionary sends the pairing selected by a primitive second root of unity to multiplication in 𝔽₂. Naturality of the explicit cup and the supplied comparisons with canonical continuous cohomology then identify the two cups.

Consequently the cohomological local symbol, formed from the roots-of-unity cup and any additive identification of its degree-two cohomology with ZMod 2, vanishes exactly when the norm equation b = x² - a y² is solvable. Translating 0, 1 : ZMod 2 to +1, -1 upgrades this vanishing criterion to equality with the norm-equation Hilbert symbol. The cup comparison itself requires no local-field hypothesis and no choice of a degree-two invariant.

References

• J.-P. Serre, Local Fields, GTM 67 (1979), XIV §2, Propositions 4–5.
• J. Neukirch, A. Schmidt, K. Wingberg, Cohomology of Number Fields, second edition, (6.2.1)–(6.2.2).

theorem TauCeti.instContinuousSMulAbsoluteGaloisGroupVIntTrivialF2_2 {K : Type u} [Field K] : ContinuousSMul (AbsoluteGaloisGroup K) ↑(trivialF2 (AbsoluteGaloisGroup K))

theorem TauCeti.kummerCoeffEquiv_kummerCoeffPairing {K : Type u} [Field K] [Invertible 2] {ζ : K} (hζ : IsPrimitiveRoot ζ 2) (x y : KummerCoeff K 2) : (kummerCoeffEquiv K) (((ClassFieldTheory.kummerCoeffPairing (ClassFieldTheory.kummerCupPairing ζ hζ)) x) y) = ((trivialF2Pairing (AbsoluteGaloisGroup K)) ((kummerCoeffEquiv K) x)) ((kummerCoeffEquiv K) y)

The μ₂ ≃ 𝔽₂ dictionary carries the pairing of a primitive second root of unity to multiplication in 𝔽₂.

theorem TauCeti.cup_muNRepH1Equiv_eq_zero_iff {K : Type u} [Field K] [Invertible 2] {ζ : K} (hζ : IsPrimitiveRoot ζ 2) (x y : ContCohomology.H1 (AbsoluteGaloisGroup K) (KummerCoeff K 2)) : (((ClassFieldTheory.kummerCupPairing ζ hζ).cup 1 1) ((ClassFieldTheory.muNRepH1Equiv 2 K) x)) ((ClassFieldTheory.muNRepH1Equiv 2 K) y) = 0 ↔ (((trivialF2TopPairing (AbsoluteGaloisGroup K)).cup 1 1) ((TopModuleCat.Hom.hom (kummerCohomMap K)) ((ContCohomology.explicitH1AddEquivContinuousCohomology (AbsoluteGaloisGroup K) (KummerCoeff K 2)) x))) ((TopModuleCat.Hom.hom (kummerCohomMap K)) ((ContCohomology.explicitH1AddEquivContinuousCohomology (AbsoluteGaloisGroup K) (KummerCoeff K 2)) y)) = 0

Transporting arbitrary degree-one classes through the two coefficient dictionaries preserves cup vanishing: the roots-of-unity cup vanishes exactly when the corresponding trivial-𝔽₂ cup does.

@[simp]

theorem TauCeti.cup_muNRep_kummerClass_eq_zero_iff {K : Type u} [Field K] [Invertible 2] {ζ : K} (hζ : IsPrimitiveRoot ζ 2) (a b : Kˣ) : (((ClassFieldTheory.kummerCupPairing ζ hζ).cup 1 1) (ClassFieldTheory.kummerClass K ⋯ a)) (ClassFieldTheory.kummerClass K ⋯ b) = 0 ↔ (((trivialF2TopPairing (AbsoluteGaloisGroup K)).cup 1 1) (kummerClass a)) (kummerClass b) = 0

The roots-of-unity cup and the trivial-𝔽₂ cup have the same vanishing criterion on Kummer classes, over every field in which 2 is invertible.

theorem TauCeti.localSymbol_eq_zero_iff_cup {K : Type u} [Field K] [Invertible 2] {ζ : K} (hζ : IsPrimitiveRoot ζ 2) (tr : ↑(continuousCohomology 2 (ClassFieldTheory.muNRep 2 K)).toModuleCat ≃+ ZMod 2) (a b : Kˣ) : ((ClassFieldTheory.localSymbol (ClassFieldTheory.kummerCupPairing ζ hζ) tr) (ClassFieldTheory.kummerClass K ⋯ a)) (ClassFieldTheory.kummerClass K ⋯ b) = 0 ↔ (((trivialF2TopPairing (AbsoluteGaloisGroup K)).cup 1 1) (kummerClass a)) (kummerClass b) = 0

The mod-two local symbol vanishes exactly when the canonical trivial-𝔽₂ Kummer cup vanishes. The statement is independent of the additive degree-two identification.

theorem TauCeti.localSymbol_eq_zero_iff_hilbertSymbol_eq_one {F : Type} [Field F] [Invertible 2] {ζ : F} (hζ : IsPrimitiveRoot ζ 2) (tr : ↑(continuousCohomology 2 (ClassFieldTheory.muNRep 2 F)).toModuleCat ≃+ ZMod 2) (a b : Fˣ) : ((ClassFieldTheory.localSymbol (ClassFieldTheory.kummerCupPairing ζ hζ) tr) (ClassFieldTheory.kummerClass F ⋯ a)) (ClassFieldTheory.kummerClass F ⋯ b) = 0 ↔ hilbertSymbol a b = 1

The roots-of-unity local symbol vanishes exactly when the norm-equation Hilbert symbol is 1. This criterion applies to any additive identification of degree-two cohomology.

theorem TauCeti.localSymbol_eq_zero_iff {F : Type} [Field F] [Invertible 2] {ζ : F} (hζ : IsPrimitiveRoot ζ 2) (tr : ↑(continuousCohomology 2 (ClassFieldTheory.muNRep 2 F)).toModuleCat ≃+ ZMod 2) (a b : Fˣ) : ((ClassFieldTheory.localSymbol (ClassFieldTheory.kummerCupPairing ζ hζ) tr) (ClassFieldTheory.kummerClass F ⋯ a)) (ClassFieldTheory.kummerClass F ⋯ b) = 0 ↔ ∃ (x : F) (y : F), ↑b = x ^ 2 - ↑a * y ^ 2

The cohomological mod-two local symbol detects solvability of the quadratic norm equation.

theorem TauCeti.hilbertSymbol_eq_cohomological {F : Type} [Field F] [Invertible 2] {ζ : F} (hζ : IsPrimitiveRoot ζ 2) (tr : ↑(continuousCohomology 2 (ClassFieldTheory.muNRep 2 F)).toModuleCat ≃+ ZMod 2) (a b : Fˣ) : hilbertSymbol a b = hilbertSign (((ClassFieldTheory.localSymbol (ClassFieldTheory.kummerCupPairing ζ hζ) tr) (ClassFieldTheory.kummerClass F ⋯ a)) (ClassFieldTheory.kummerClass F ⋯ b))

The norm-equation Hilbert symbol agrees with the cohomological mod-two local symbol after translating its additive invariant to a sign.