Central simple algebras are closed under tensor product

Let K be a field, let A be a central simple K-algebra and let B be a simple K-algebra. This file proves that A ⊗[K] B is again simple, in both orientations. Together with TauCeti.Algebra.IsCentral.tensorProduct of TauCeti/Algebra/Central/TensorProduct.lean, which says that A ⊗[K] B is again central as soon as B is, this is the statement that central simple K-algebras are closed under ⊗[K]. That closure is what lets the tensor product descend to a multiplication on Brauer classes.

Simplicity needs no finite-dimensionality. The argument is the classical minimal-length one, and it uses only that A is simple with centre K and that B is simple.

Simplicity is a statement about A ⊗[K] B as a ring, so it applies unchanged to a scalar extension L ⊗[K] A along a field extension L / K, with L merely simple and A central simple: that is the orientation supplied by TauCeti.IsSimpleRing.tensorProduct_of_isCentral_right. It is only the simplicity half of "L ⊗[K] A is central simple over L". The centrality there is a statement about L ⊗[K] A as an L-algebra, over L and not over K, and is not proved here: TauCeti.Algebra.IsCentral.tensorProduct gives centrality over K and asks both factors to be central over K, which for a nontrivial extension L / K the factor L is not. The other half is TauCeti.Algebra.IsCentral.baseChange in TauCeti/Algebra/Central/BaseChange.lean, which asks only that A be central and L be free as a K-module, and so combines with the simplicity instance below rather than resting on it.

Main results

• TauCeti.IsSimpleRing.tensorProduct: A ⊗[K] B is simple when A is central simple and B is simple. Only one of the two factors has to be central.
• TauCeti.IsSimpleRing.tensorProduct_of_isCentral_right: the mirror-image statement, with B central simple and A merely simple, obtained by transporting the previous one along Algebra.TensorProduct.comm. This is the orientation of a scalar extension L ⊗[K] A.

Both are instances, and TauCeti.Algebra.IsCentral.tensorProduct is re-exported by this module, so importing this file alone lets typeclass inference recognize A ⊗[K] B as a central simple K-algebra whenever A and B are. With Mathlib's matrix instances that reads Mₘ(K) ⊗[K] Mₙ(K) off with no glue; that is the worked example checked at the end of the file.

Implementation notes

The minimal-length argument for simplicity is run in the coordinates of Algebra.TensorProduct.basis A 𝓑, the A-basis of A ⊗[K] B attached to a K-basis 𝓑 of B. Reading an element in these coordinates is exactly the classical step "write x = ∑ aᵢ ⊗ bᵢ with the bᵢ linearly independent over K", with the Finsupp support playing the role of the length of that expression. Multiplying by a ⊗ₜ 1 on one side multiplies every coordinate on that same side, which is what makes the coordinatewise bookkeeping of that argument -- the two-sided ideal of i₀-th coordinates, and the support of an additive commutator -- available. On the left this is just the generic scalar-action API: (a ⊗ₜ 1) * x is the module action a • x by Mathlib's smul_one_mul (packaged as Algebra.TensorProduct.tmul_one_mul_eq_smul), and (Algebra.TensorProduct.basis A 𝓑).repr is A-linear. The right-hand version is a statement in its own right, Algebra.TensorProduct.basis_repr_mul_tmul_one, and it is where it matters that the coordinates are taken with respect to a basis of B over the base field: that is what lets the scalars pass through a. Both are general facts about A ⊗[K] B and live in TauCeti/Algebra/TensorProduct/Mul.lean.

Simplicity is then the classical minimal-length argument: given a nonzero two-sided ideal I, pick a nonzero y ∈ I with as few nonzero coordinates as possible; after rescaling one coordinate to 1 (which is where simplicity of A is used), minimality forces every additive commutator (a ⊗ₜ 1) * y - y * (a ⊗ₜ 1) to vanish, so y = 1 ⊗ₜ b by TauCeti.Algebra.TensorProduct.forall_commute_tmul_one_iff; simplicity of B then pushes 1 into I.

Both appeals to simplicity in TauCeti.IsSimpleRing.tensorProduct are made by exhibiting a two-sided ideal that is nonzero, hence everything: on the A side the i₀-th coordinates of the elements of a two-sided ideal I supported in a fixed finite set, built as a TwoSidedIdeal.mk', and on the B side the c : B with 1 ⊗ₜ c ∈ I, which is I.comap along Algebra.TensorProduct.includeRight. That is how 1 enters I; phrasing the argument this way avoids ever expanding 1 as an explicit sum ∑ uⱼ a vⱼ.

References

R. S. Pierce, Associative Algebras, GTM 88, Chapter 12, and P. Gille, T. Szamuely, Central Simple Algebras and Galois Cohomology, Chapter 2.

instance TauCeti.IsSimpleRing.tensorProduct (K : Type u_1) (A : Type u_2) (B : Type u_3) [Field K] [Ring A] [Ring B] [Algebra K A] [Algebra K B] [Algebra.IsCentral K A] [IsSimpleRing A] [IsSimpleRing B] : IsSimpleRing (TensorProduct K A B)

The tensor product of a central simple K-algebra with a simple K-algebra is simple. Together with TauCeti.Algebra.IsCentral.tensorProduct this says that central simple K-algebras are closed under ⊗[K].

No finite-dimensionality is needed on either side.

instance TauCeti.IsSimpleRing.tensorProduct_of_isCentral_right (K : Type u_1) (A : Type u_2) (B : Type u_3) [Field K] [Ring A] [Ring B] [Algebra K A] [Algebra K B] [IsSimpleRing A] [Algebra.IsCentral K B] [IsSimpleRing B] : IsSimpleRing (TensorProduct K A B)

The tensor product of a simple K-algebra with a central simple K-algebra is simple. This is TauCeti.IsSimpleRing.tensorProduct with the roles of the two factors exchanged, so that it is the right factor that is central; it is the orientation of a scalar extension L ⊗[K] A, where L / K is a field extension and A is the central simple algebra.