Quaternion algebras as crossed products

Let L/K be a Galois extension of degree two with nontrivial automorphism σ, and let α ∈ L with α² = a ∈ Kˣ and α ∉ K, so that L = K(√a) and σ α = -α. For b ∈ Kˣ, the crossed product of the quadratic cocycle TauCeti.TwoCocycle.quadratic h b, whose only nontrivial value is c(σ, σ) = b, is generated over K by i = α and j = u_σ with

i² = a, j² = b, j i = σ(α) j = -i j,

which are the relations of the quaternion algebra ℍ[K, a, b]. Both algebras have dimension four, and the quaternion algebra is simple, so the resulting homomorphism ℍ[K, a, b] → (L, σ, b) is an isomorphism (TauCeti.CrossedProduct.nonempty_quaternionAlgebra_algEquiv_quadratic). In the Brauer group, the class of the quadratic cocycle of b is therefore the quaternion symbol [(a, b)] (TauCeti.BrauerGroup.crossedProductClass_quadratic).

This is the step at which a cocycle meets an algebra in the computation ι [(a, b)] = (a) ∪ (b) of the quaternion symbol as a cup product.

Main results

• TauCeti.CrossedProduct.nonempty_quaternionAlgebra_algEquiv_quadratic: the crossed product of the quadratic cocycle of b over K(√a) is isomorphic to ℍ[K, a, b].
• TauCeti.BrauerGroup.crossedProductClass_quadratic: its Brauer class is [(a, b)].

References

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

theorem TauCeti.CrossedProduct.nonempty_quaternionAlgebra_algEquiv_quadratic {K : Type u} {L : Type v} [Field K] [Field L] [Algebra K L] [FiniteDimensional K L] [IsGalois K L] (h : Nat.card Gal(L/K) = 2) {a : Kˣ} {α : L} [Invertible 2] (hα : α ^ 2 = (algebraMap K L) ↑a) (hαK : α ∉ Set.range ⇑(algebraMap K L)) (b : Kˣ) : Nonempty (QuaternionAlgebra K (↑a) 0 ↑b ≃ₐ[K] CrossedProduct (TwoCocycle.quadratic h b))

The quaternion algebra (a, b) is the crossed product of the quadratic cocycle of b over K(√a). If L/K is Galois with automorphism group of order two and α ∈ L ∖ K has α² = a, the crossed product of TauCeti.TwoCocycle.quadratic h b is isomorphic to ℍ[K, a, b], by i ↦ α and j ↦ u_σ for the nontrivial automorphism σ.

theorem TauCeti.BrauerGroup.crossedProductClass_quadratic {K L : Type u} [Field K] [Field L] [Algebra K L] [FiniteDimensional K L] [IsGalois K L] (h : Nat.card Gal(L/K) = 2) {a : Kˣ} {α : L} [Invertible 2] (hα : α ^ 2 = (algebraMap K L) ↑a) (hαK : α ∉ Set.range ⇑(algebraMap K L)) (b : Kˣ) : crossedProductClass (TwoCocycle.quadratic h b) = quaternionClass a b

The Brauer class of the quadratic cocycle of b over K(√a) is the quaternion symbol [(a, b)].