Documentation

TauCeti.Algebra.BrauerGroup.Real

The Brauer group of the reals is ℤ/2 #

TauCeti/Algebra/BrauerGroup/Quaternion.lean shows that the Brauer class of ℍ[ℝ] has order 2. This file shows that it is the only class besides the identity, so BrauerGroup ℝ is cyclic of order 2.

The input is Frobenius' theorem, TauCeti.nonempty_algEquiv_real_or_quaternion: a finite-dimensional central division algebra over ℝ is ℝ or ℍ[ℝ]. Every Brauer class has such a representative (TauCeti.BrauerGroup.exists_eq_mk_centralDivisionRing), and the class of ℝ is the identity, so there are at most the two classes already known. They are distinct by TauCeti.Quaternion.mk_ne_one, so [ℍ[ℝ]] generates a group of exactly two elements, and Mathlib's zmodMulEquivOfGenerator names the resulting isomorphism.

Main results #

References #

This is the "real base field" target of Layer 6 of the semisimple algebras roadmap: "BrauerGroup ℝ ≃ ℤ/2, generated by the class of the Hamilton quaternions ℍ[ℝ]". See P. Gille, T. Szamuely, Central Simple Algebras and Galois Cohomology, CUP (2006), §1.1 and §2.4.

source
theorem TauCeti.Quaternion.eq_one_or_eq_mk (x : BrauerGroup ℝ) :
x = 1 ∨ x = BrauerGroup.mk (CSA.of ℝ (Quaternion ℝ))

Every Brauer class over ℝ is the identity or the class of the real quaternions.

The class has a central division-algebra representative, which by Frobenius' theorem is ℝ or ℍ[ℝ]; the class of ℝ is the identity.

source
theorem TauCeti.Quaternion.zpowers_mk_eq_top :
Subgroup.zpowers (BrauerGroup.mk (CSA.of ℝ (Quaternion ℝ))) = ⊤

The Brauer class of ℍ[ℝ] generates the Brauer group of ℝ.

source
@[simp]
theorem TauCeti.Quaternion.card_brauerGroup_eq_two :
Nat.card (BrauerGroup ℝ) = 2

The Brauer group of ℝ has exactly two elements. It is generated by the class of ℍ[ℝ], whose order is 2.

source
noncomputable def TauCeti.Quaternion.brauerGroupMulEquiv :
BrauerGroup ℝ ≃* Multiplicative (ZMod 2)

The Brauer group of the reals is ℤ/2, generated by the class of the Hamilton quaternions.

This is the summit of the real base field target: alongside TauCeti.subsingleton_brauerGroup_of_isAlgClosed and TauCeti.subsingleton_brauerGroup_of_finite, it is the first Brauer group computed in Tau Ceti that is nontrivial. The isomorphism is characterised by TauCeti.Quaternion.brauerGroupMulEquiv_mk and its inverse by TauCeti.Quaternion.brauerGroupMulEquiv_symm_ofAdd_one.

Equations
Instances For
    source
    @[simp]
    theorem TauCeti.Quaternion.brauerGroupMulEquiv_mk :
    brauerGroupMulEquiv (BrauerGroup.mk (CSA.of ℝ (Quaternion ℝ))) = Multiplicative.ofAdd 1

    The characterisation of TauCeti.Quaternion.brauerGroupMulEquiv: it sends the Brauer class of ℍ[ℝ] to Multiplicative.ofAdd 1, the generator of Multiplicative (ZMod 2). Since that class generates (TauCeti.Quaternion.zpowers_mk_eq_top), this determines the isomorphism.

    source
    @[simp]
    theorem TauCeti.Quaternion.brauerGroupMulEquiv_symm_ofAdd_one :
    brauerGroupMulEquiv.symm (Multiplicative.ofAdd 1) = BrauerGroup.mk (CSA.of ℝ (Quaternion ℝ))

    The inverse of TauCeti.Quaternion.brauerGroupMulEquiv sends the generator Multiplicative.ofAdd 1 of Multiplicative (ZMod 2) back to the Brauer class of ℍ[ℝ], the other half of the characterisation in TauCeti.Quaternion.brauerGroupMulEquiv_mk.

    Worked examples #