The quaternion symbol as a cup product

Let K be a field in which 2 is invertible. This file proves that the comparison TauCeti.brauerCohomologyEquiv K : Br(K) ≃ H²_cont(G_K, (Kˢ)ˣ) sends the quaternion symbol [(a, b)] to the image under TauCeti.h2MuToUnits K of the cup product (a) ∪ (b) of the Kummer classes of a and b (TauCeti.brauerCohomologyEquiv_quaternionClass). Read through the 2-torsion comparison TauCeti.brauer2EquivH2 K : Br(K)[2] ≃ H²_cont(G_K, 𝔽₂), this is the classical identity ι [(a, b)] = (a) ∪ (b) (TauCeti.brauer2EquivH2_quaternionClass).

If a is a square, both sides vanish. Otherwise, choose square roots α of a and β of b in Kˢ, and let L = K(α), a quadratic Galois subextension of Kˢ. The computation has three steps.

• The quaternion algebra (a, b) is the crossed product of the quadratic cocycle of b over L (TauCeti.BrauerGroup.crossedProductClass_quadratic), so the comparison sends [(a, b)] to the inflation of that cocycle, c(g, k) = b if neither g nor k fixes α, and 1 otherwise (TauCeti.brauerCohomologyEquiv_crossedProductClass).
• On explicit cocycles, (a) and (b) are χ_α(g) = [g α ≠ α] and χ_β(k) = [k β ≠ β], their cup product is χ_α(g) χ_β(k), and h2MuToUnits K sends it to the class of w(g, k) = (-1) ^ (χ_α(g) χ_β(k)).
• The two cocycles differ by the coboundary of the continuous cochain f(g) = (g β) ^ χ_α(g): c = w · d f. This is a direct check on the eight cases g α = ± α, k α = ± α, k β = ± β.

Main results

• TauCeti.TwoCocycle.inflateClass_quadratic_eq_h2MuToUnits_cup: the cyclic class represented by the quadratic cocycle of b inflates to the image of (a) ∪ (b) in the multiplicative coefficients.
• TauCeti.brauerCohomologyEquiv_quaternionClass: the comparison sends [(a, b)] to h2MuToUnits K ((a) ∪ (b)).
• TauCeti.brauer2EquivH2_quaternionClass: the 2-torsion comparison sends [(a, b)] to (a) ∪ (b).

References

• J.-P. Serre, Local Fields, Graduate Texts in Mathematics 67, Springer (1979), Chapter XIV, §2, Proposition 5.
• P. Gille and T. Szamuely, Central Simple Algebras and Galois Cohomology (2006), Proposition 4.7.1.

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

The trivial 𝔽₂ coefficients are a discrete G_K-module.

theorem TauCeti.instLocallyCompactSpaceAbsoluteGaloisGroup {K : Type} [Field K] : LocallyCompactSpace (AbsoluteGaloisGroup K)

The absolute Galois group is locally compact, being compact and Hausdorff. Instance search does not find this within its default budget under the imports of this file, so it is assembled here from the Krull topology being Hausdorff.

The cup product of Kummer classes on explicit cocycles

The coboundary

theorem TauCeti.TwoCocycle.inflateClass_quadratic_eq_h2MuToUnits_cup {K : Type} [Field K] [Invertible 2] {a b : Kˣ} {α : (SeparableClosure K)ˣ} (hα : α ^ 2 = (Units.map ↑(algebraMap K (SeparableClosure K))) a) (L : IntermediateField K (SeparableClosure K)) [FiniteDimensional K ↥L] [IsGalois K ↥L] (hcard : Nat.card Gal(↥L/K) = 2) (hr : ∀ (g : AbsoluteGaloisGroup K), (AlgEquiv.restrictNormalHom ↥L) g = 1 ↔ g • α = α) : inflateClass L (quadratic hcard b) = (TopModuleCat.Hom.hom (h2MuToUnits K)) ((((trivialF2TopPairing (AbsoluteGaloisGroup K)).cup 1 1) (kummerClass a)) (kummerClass b))

The cyclic class of b inflates to (a) ∪ (b). Let L/K be a quadratic Galois subextension of Kˢ/K, and suppose that restriction to L is trivial exactly on the automorphisms that fix a chosen square root α of a. Then the inflation of the quadratic cocycle with value b is the image under h2MuToUnits of the cup product of the Kummer classes of a and b.

Together with TauCeti.quadraticNormQuotientEquiv_mk, this says that under H²(Gal(L/K), Lˣ) ≃ Kˣ / N_{L/K}(Lˣ), the class of b inflates to (a) ∪ (b).

The symbol as a cup product

theorem TauCeti.brauerCohomologyEquiv_quaternionClass {K : Type} [Field K] [Invertible 2] (a b : Kˣ) : (brauerCohomologyEquiv K) (Additive.ofMul (BrauerGroup.quaternionClass a b)) = (TopModuleCat.Hom.hom (h2MuToUnits K)) ((((trivialF2TopPairing (AbsoluteGaloisGroup K)).cup 1 1) (kummerClass a)) (kummerClass b))

The quaternion symbol as a cup product. The comparison Br(K) ≃ H²_cont(G_K, (Kˢ)ˣ) sends the quaternion symbol [(a, b)] to the image under h2MuToUnits K of the cup product (a) ∪ (b) ∈ H²_cont(G_K, 𝔽₂) of the Kummer classes of a and b.

theorem TauCeti.brauer2EquivH2_quaternionClass {K : Type} [Field K] [Invertible 2] (a b : Kˣ) : (brauer2EquivH2 K) (Additive.ofMul ⟨BrauerGroup.quaternionClass a b, ⋯⟩) = (((trivialF2TopPairing (AbsoluteGaloisGroup K)).cup 1 1) (kummerClass a)) (kummerClass b)

The symbol as a cup product, ι [(a, b)] = (a) ∪ (b). The identification Br(K)[2] ≃ H²_cont(G_K, 𝔽₂) sends the quaternion symbol [(a, b)] to the cup product of the Kummer classes of a and b.