Division-algebra representatives of Brauer classes

Every class in the Brauer group of a field has a representative which is a finite-dimensional central division algebra, and this representative is unique up to isomorphism as an algebra over the base field.

Existence is the Wedderburn--Artin theorem. A representative A of the class has a presentation A ≃ₐ[K] Mₙ(D) for a central division algebra D; an algebra isomorphism and passage to matrices both preserve the Brauer class, so [A] = [D].

For uniqueness, if central division algebras D and E have the same class, Brauer equivalence gives positive n and m and an algebra isomorphism Mₙ(D) ≃ₐ[K] Mₘ(E). The algebra-linear Wedderburn uniqueness theorem TauCeti.nonempty_algEquiv_of_algEquiv_matrix then gives D ≃ₐ[K] E. Its algebra linearity is load-bearing: ring-level Wedderburn uniqueness alone would not say that the resulting isomorphism fixes the chosen copy of K.

Main results

• TauCeti.BrauerGroup.exists_eq_mk_centralDivisionRing: every Brauer class is represented by a finite-dimensional central division algebra.
• TauCeti.BrauerGroup.nonempty_algEquiv_of_mk_eq_mk: two central division algebras representing the same class are isomorphic over the base field.
• TauCeti.BrauerGroup.isBrauerEquivalent_iff_nonempty_algEquiv: Brauer equivalence of two central division algebras is equivalent to the existence of that algebra isomorphism.

References

This proves the “unique division-algebra representative” target in Layer 6 of the semisimple algebras roadmap. See P. Gille and T. Szamuely, Central Simple Algebras and Galois Cohomology, §2.4, and R. S. Pierce, Associative Algebras, Chapter 12.

theorem TauCeti.BrauerGroup.exists_eq_mk_centralDivisionRing (K : Type u) [Field K] (x : BrauerGroup K) : ∃ (D : Type v) (x_1 : DivisionRing D) (x_2 : Algebra K D) (x_3 : Algebra.IsCentral K D) (x_4 : FiniteDimensional K D), x = mk (CSA.of K D)

Every Brauer class has a central division-algebra representative. More precisely, for every x : BrauerGroup K there is a finite-dimensional central division K-algebra D whose Brauer class is x.

The representative is not chosen as data: the theorem records its existence, while TauCeti.BrauerGroup.nonempty_algEquiv_of_mk_eq_mk says that any two choices are isomorphic over K.

theorem TauCeti.BrauerGroup.nonempty_algEquiv_of_mk_eq_mk {K : Type u} [Field K] {D E : Type v} [DivisionRing D] [Algebra K D] [Algebra.IsCentral K D] [FiniteDimensional K D] [DivisionRing E] [Algebra K E] [Algebra.IsCentral K E] [FiniteDimensional K E] (h : mk (CSA.of K D) = mk (CSA.of K E)) : Nonempty (D ≃ₐ[K] E)

Central division algebras in the same Brauer class are isomorphic over the base field.

Equality of classes produces a Brauer equivalence, hence an algebra isomorphism between positive matrix algebras over D and E. Algebra-linear Wedderburn uniqueness recovers an isomorphism of the coefficient division algebras themselves.

@[simp]

theorem TauCeti.BrauerGroup.isBrauerEquivalent_iff_nonempty_algEquiv {K : Type u} [Field K] {D E : Type v} [DivisionRing D] [Algebra K D] [Algebra.IsCentral K D] [FiniteDimensional K D] [DivisionRing E] [Algebra K E] [Algebra.IsCentral K E] [FiniteDimensional K E] : IsBrauerEquivalent (CSA.of K D) (CSA.of K E) ↔ Nonempty (D ≃ₐ[K] E)

Two central division algebras are Brauer equivalent exactly when they are isomorphic as algebras over the base field.

The reverse implication is the general fact that algebra isomorphisms preserve Brauer classes; the forward implication is the uniqueness of division-algebra representatives.