Brauer classes of Clifford algebras #
A central simple algebra isomorphic to a Clifford algebra has a self-inverse Brauer class:
Mathlib's CliffordAlgebra.reverseOpEquiv identifies the Clifford algebra with its opposite.
This gives the even-rank case of two-torsion for the Clifford invariant.
Main results #
TauCeti.BrauerGroup.inv_mk_eq_mk_of_algEquiv_cliffordAlgebra: a central simple algebra isomorphic to a Clifford algebra has a self-inverse Brauer class.
theorem
TauCeti.BrauerGroup.inv_mk_eq_mk_of_algEquiv_cliffordAlgebra
{K : Type u}
[Field K]
{W : Type u_1}
[AddCommGroup W]
[Module K W]
{P : QuadraticForm K W}
(A : CSA K)
(e : CliffordAlgebra P ≃ₐ[K] ↑A.toAlgCat)
:
A central simple algebra isomorphic to a Clifford algebra has a self-inverse Brauer class:
the reversion identifies a Clifford algebra with its opposite algebra. No hypothesis on the form
is needed beyond the central simplicity carried by A.