Brauer equivalence: bundling central simple algebras, matrices, and the tensor product

Two finite-dimensional central simple K-algebras are Brauer equivalent when they become isomorphic after passing to matrix algebras over them: IsBrauerEquivalent A B is Mathlib's ∃ n m ≠ 0, Mₙ(A) ≃ₐ[K] Mₘ(B). Mathlib defines this relation, checks that it is an equivalence relation, and forms the quotient BrauerGroup K -- but the quotient carries no algebraic structure yet, and nothing is on record for the relation to be fed: CSA K is a structure over AlgCat K, so its constructor takes a bundled object rather than an algebra, and Mathlib names no member of it -- not even Mₙ(A).

This file supplies the working API. It builds the constructors that the theory needs (TauCeti.CSA.of, and on top of it TauCeti.CSA.base, TauCeti.CSA.matrix and TauCeti.CSA.tensorProduct), records the two moves that leave a Brauer class unchanged -- an isomorphism of algebras, and passage to matrices over the algebra -- and proves that the tensor product respects Brauer equivalence, so that it descends to BrauerGroup K.

The group law itself is deliberately not installed here. Multiplication, commutativity, associativity and the identity are all available from the statements below, but the inverse is not: it rests on the separate opposite isomorphism A ⊗[K] Aᵐᵒᵖ ≃ₐ[K] M_{finrank K A}(K), which belongs to the theory of the Azumaya map rather than to the Brauer-equivalence bookkeeping done here. Installing a monoid structure now, to replace it by a group structure later, would only create work; so BrauerGroup K is left as Mathlib's bare quotient. Which algebras are in the identity class is the subject of TauCeti/Algebra/BrauerGroup/Trivial.lean, which builds on this file.

Matrix absorption

The one genuine computation is Mₘ(A) ⊗[K] Mₙ(B) ≃ₐ[K] M_{mn}(A ⊗[K] B). It is not proved here: it is Mathlib's Kronecker product of matrix algebras, Matrix.kroneckerTMulAlgEquiv, whose target is indexed by Fin m × Fin n, transported along finProdFinEquiv to the Fin (m * n) indexing that IsBrauerEquivalent is stated in. Since neither central simplicity nor positivity of the sizes enters, it is stated in that generality first, as Matrix.kroneckerTMulFinAlgEquiv, over any commutative semiring and any two algebras over it; TauCeti.CSA.tensorProductMatrixAlgEquiv is the bundled CSA reading that Brauer equivalence consumes. Everything about the tensor product below is a consequence of it and of the transport Algebra.TensorProduct.congr.

Universes

CSA.{u, v} K places the algebra in a universe v of its own, and IsBrauerEquivalent compares two algebras in the same v. The general lemmas below are therefore stated for an arbitrary v, but every statement mentioning the base field -- TauCeti.CSA.base, and so TauCeti.isBrauerEquivalent_tensorProduct_base -- needs v = u, since K : Type u cannot be moved. This is not a restriction in practice: BrauerGroup K is the interesting object at v = u.

Main definitions

• TauCeti.CSA.of: an algebra with the three central-simple instances, as a term of CSA K; TauCeti.CSA.base K is K itself.
• TauCeti.CSA.matrix A n and TauCeti.CSA.tensorProduct A B: Mₙ(A) and A ⊗[K] B as terms of CSA K. The underlying type of each is the expected one by definition.
• Matrix.kroneckerTMulFinAlgEquiv: matrix absorption Mₘ(A) ⊗[R] Mₙ(B) ≃ₐ[R] M_{mn}(A ⊗[R] B) for arbitrary algebras and sizes, and TauCeti.CSA.tensorProductMatrixAlgEquiv, its bundled CSA reading.

Main results

• TauCeti.IsBrauerEquivalent.of_algEquiv and TauCeti.isBrauerEquivalent_matrix: the two moves that leave a Brauer class unchanged -- an isomorphism of algebras, and passage to matrices over the algebra. The second is the reason IsBrauerEquivalent is coarser than isomorphism, and it is what makes the Brauer class of a split algebra the identity.
• TauCeti.isBrauerEquivalent_tensorProduct_congr: the tensor product respects Brauer equivalence, so it descends to BrauerGroup K. With TauCeti.isBrauerEquivalent_tensorProduct_comm, TauCeti.isBrauerEquivalent_tensorProduct_assoc and TauCeti.isBrauerEquivalent_tensorProduct_base this is the commutative-monoid half of the group law.

References

• Semisimple algebras, Artin-Wedderburn, and the structure of their modules roadmap, Layer 6, "Brauer-triviality prerequisites".
• P. Gille, T. Szamuely, Central Simple Algebras and Galois Cohomology, CUP (2006), §2.4.
• R. S. Pierce, Associative Algebras, Springer GTM 88 (1982), Chapter 12.

Constructing central simple algebras

@[reducible, inline]

abbrev TauCeti.CSA.of (K : Type u) [Field K] (A : Type v) [Ring A] [Algebra K A] [Algebra.IsCentral K A] [IsSimpleRing A] [FiniteDimensional K A] : CSA K

A finite-dimensional central simple K-algebra, bundled as a term of Mathlib's CSA K.

Mathlib's CSA K carries its algebra as an AlgCat K together with three instance fields; this is the constructor turning the unbundled hypotheses used everywhere else into that bundling. It is an abbrev so that the carrier of TauCeti.CSA.of K A is reducibly A, and instances stated for A are found for it.

Equations

• TauCeti.CSA.of K A = { toAlgCat := ↧A, isCentral := inst✝², isSimple := inst✝¹, fin_dim := inst✝ }

theorem TauCeti.CSA.coe_of (K : Type u) [Field K] (A : Type v) [Ring A] [Algebra K A] [Algebra.IsCentral K A] [IsSimpleRing A] [FiniteDimensional K A] : ↑(of K A).toAlgCat = A

@[reducible, inline]

abbrev TauCeti.CSA.base (K : Type u) [Field K] : CSA K

The base field as a central simple algebra over itself. This is the Brauer class of the split algebras, and the intended identity of BrauerGroup K.

Equations

• TauCeti.CSA.base K = TauCeti.CSA.of K K

@[reducible, inline]

abbrev TauCeti.CSA.matrix {K : Type u} [Field K] (A : CSA K) (n : ℕ) [NeZero n] : CSA K

The n × n matrices over a central simple K-algebra, again a central simple K-algebra. Brauer equivalence is exactly the relation that identifies this with A (TauCeti.isBrauerEquivalent_matrix).

Equations

• TauCeti.CSA.matrix A n = TauCeti.CSA.of K (Matrix (Fin n) (Fin n) ↑A.toAlgCat)

@[reducible, inline]

abbrev TauCeti.CSA.tensorProduct {K : Type u} [Field K] (A B : CSA K) : CSA K

The tensor product of two central simple K-algebras, again a central simple K-algebra by TauCeti.Algebra.IsCentral.tensorProduct and TauCeti.IsSimpleRing.tensorProduct. This is the operation that descends to the group law on BrauerGroup K (TauCeti.isBrauerEquivalent_tensorProduct_congr).

Equations

• TauCeti.CSA.tensorProduct A B = TauCeti.CSA.of K (TensorProduct K ↑A.toAlgCat ↑B.toAlgCat)

The two moves that preserve a Brauer class

theorem TauCeti.IsBrauerEquivalent.of_algEquiv (K : Type u) [Field K] {A B : CSA K} (e : ↑A.toAlgCat ≃ₐ[K] ↑B.toAlgCat) : IsBrauerEquivalent A B

An isomorphism of algebras is a Brauer equivalence: take one-by-one matrices on both sides.

theorem TauCeti.isBrauerEquivalent_matrix (K : Type u) [Field K] (A : CSA K) (n : ℕ) [NeZero n] : IsBrauerEquivalent (CSA.matrix A n) A

Passing to matrices does not change the Brauer class. This is the move making Brauer equivalence strictly coarser than isomorphism -- Mₙ(A) and A are almost never isomorphic, their dimensions differing by a factor of n ^ 2 -- and it is why Mₙ(K) will be the identity class: it is Mₙ of the identity algebra.

The witness is the smallest one available, M₁(Mₙ(A)) ≃ₐ Mₙ(A), which is Matrix.compAlgEquiv followed by the reindexing Fin 1 × Fin n ≃ Fin n.

theorem TauCeti.isBrauerEquivalent_matrix_congr (K : Type u) [Field K] {A B : CSA K} (h : IsBrauerEquivalent A B) (m n : ℕ) [NeZero m] [NeZero n] : IsBrauerEquivalent (CSA.matrix A m) (CSA.matrix B n)

Matrix algebras over Brauer equivalent algebras are Brauer equivalent, in any two sizes.

Matrix absorption

def TauCeti.CSA.tensorProductMatrixAlgEquiv {K : Type u} [Field K] (A B : CSA K) (m n : ℕ) [NeZero m] [NeZero n] : ↑(tensorProduct (matrix A m) (matrix B n)).toAlgCat ≃ₐ[K] ↑(matrix (tensorProduct A B) (m * n)).toAlgCat

Matrix absorption for central simple algebras: Mₘ(A) ⊗[K] Mₙ(B) ≃ₐ[K] M_{mn}(A ⊗[K] B) as an isomorphism of terms of CSA K. This is Matrix.kroneckerTMulFinAlgEquiv, read through the constructors TauCeti.CSA.matrix and TauCeti.CSA.tensorProduct, whose underlying types are the expected ones by definition.

Equations

• TauCeti.CSA.tensorProductMatrixAlgEquiv A B m n = Matrix.kroneckerTMulFinAlgEquiv m n K ↑A.toAlgCat ↑B.toAlgCat

The tensor product of Brauer classes

theorem TauCeti.isBrauerEquivalent_tensorProduct_congr (K : Type u) [Field K] {A A' B B' : CSA K} (hA : IsBrauerEquivalent A A') (hB : IsBrauerEquivalent B B') : IsBrauerEquivalent (CSA.tensorProduct A B) (CSA.tensorProduct A' B')

The tensor product respects Brauer equivalence, so it descends to a binary operation on BrauerGroup K.

theorem TauCeti.isBrauerEquivalent_tensorProduct_comm (K : Type u) [Field K] (A B : CSA K) : IsBrauerEquivalent (CSA.tensorProduct A B) (CSA.tensorProduct B A)

The tensor product of central simple algebras is commutative up to Brauer equivalence -- indeed up to isomorphism, by Algebra.TensorProduct.comm.

theorem TauCeti.isBrauerEquivalent_tensorProduct_assoc (K : Type u) [Field K] (A B C : CSA K) : IsBrauerEquivalent (CSA.tensorProduct (CSA.tensorProduct A B) C) (CSA.tensorProduct A (CSA.tensorProduct B C))

The tensor product of central simple algebras is associative up to Brauer equivalence -- indeed up to isomorphism, by Algebra.TensorProduct.assoc.

theorem TauCeti.isBrauerEquivalent_tensorProduct_base (K : Type u) [Field K] (A : CSA K) : IsBrauerEquivalent (CSA.tensorProduct A (CSA.base K)) A

The base field is the identity for the tensor product, up to Brauer equivalence -- indeed up to isomorphism, by Algebra.TensorProduct.rid.