The Brauer class of the real quaternions has order two #
This file applies the general Brauer-group API to the real quaternions. Quaternion conjugation
identifies ℍ[ℝ] with its opposite algebra, so its Brauer class is self-inverse; and ℍ[ℝ] is a
central division algebra of dimension 4, so that class is not the identity
(TauCeti.BrauerGroup.mk_eq_one_iff_finrank_eq_one). Together these say the class has order exactly
2, and in particular BrauerGroup ℝ is not trivial. Complexification kills the class, in the two
ways TauCeti/Algebra/BrauerGroup/BaseChange.lean offers, so the kernel of base change to ℂ is
strictly larger than the trivial subgroup.
That [ℍ[ℝ]] generates BrauerGroup ℝ, that is, that BrauerGroup ℝ ≃ ℤ/2, needs the
classification of the finite-dimensional real division algebras with centre ℝ -- only ℝ and
ℍ[ℝ] occur -- and is proved in TauCeti/Algebra/BrauerGroup/Real.lean
(TauCeti.Quaternion.brauerGroupMulEquiv) on top of the order computation here.
Main results #
TauCeti.Quaternion.mk_ne_one: the Brauer class ofℍ[ℝ]is not the identity.TauCeti.Quaternion.orderOf_mk_eq_two: that class has order exactly2, soBrauerGroup ℝcontains a copy ofℤ/2;TauCeti.Quaternion.nontrivial_brauerGroupis the qualitative form.
References #
This is the Brauer-group half of the Hamilton-quaternion worked example of the
semisimple algebras roadmap
("ℍ[ℝ] ⊗_ℝ ℍ[ℝ] ≃ M₄(ℝ), so [ℍ] has order 2"), whose algebra half is
TauCeti/Algebra/CentralSimple/Quaternion.lean. See P. Gille, T. Szamuely, Central Simple Algebras
and Galois Cohomology, CUP (2006), §1.1 and §2.4.
The Brauer class of the real quaternions is not the identity. ℍ[ℝ] is a central division
algebra over ℝ of dimension 4, and a central division algebra has the identity class only when
it is one-dimensional, that is, only when it is the base field.
The Brauer class of the real quaternions has order exactly 2.
Quaternion conjugation is an ℝ-algebra isomorphism ℍ[ℝ] ≃ₐ[ℝ] ℍ[ℝ]ᵐᵒᵖ (Mathlib's
Quaternion.starAe), so the class is its own inverse and its order divides 2; concretely that
self-inverseness is the isomorphism ℍ[ℝ] ⊗[ℝ] ℍ[ℝ] ≃ₐ[ℝ] M₄(ℝ) of
TauCeti.Quaternion.tensorSelfAlgEquivMatrix. It is not order 1 because the class is not the
identity (TauCeti.Quaternion.mk_ne_one).
The Brauer group of the reals is not trivial, witnessed by the class of ℍ[ℝ]. Contrast
TauCeti.subsingleton_brauerGroup_of_isAlgClosed and
TauCeti.subsingleton_brauerGroup_of_finite: over ℝ there is a central division algebra other
than the base field, so the Brauer group has something in it.
The universes are pinned because BrauerGroup.{u, v} carries its group structure, hence its
identity element, only for v = u.