The tensor product of two central algebras is central

Mathlib's Mathlib/Algebra/Central/TensorProduct.lean has the two converse statements (Algebra.IsCentral.left_of_tensor_of_field and Algebra.IsCentral.right_of_tensor_of_field), but not the forward one. This file supplies it, over a field, together with the elementwise centralizer computation it rests on.

Main results

• TauCeti.Algebra.TensorProduct.forall_commute_tmul_one_iff: for A central over K, the centralizer of A ⊗ 1 in A ⊗[K] B is exactly 1 ⊗ B. This is Mathlib's Subalgebra.centralizer_coe_range_includeLeft_eq_center_tensorProduct specialized to Z(A) = K and phrased elementwise. It is stated over a commutative base ring with B free, the hypotheses that theorem needs; the case of a field is picked up by typeclass inference.
• TauCeti.Algebra.IsCentral.tensorProduct: A ⊗[K] B is central when both factors are.

The companion simplicity statement, TauCeti.IsSimpleRing.tensorProduct, is in TauCeti/Algebra/CentralSimple/TensorProduct.lean; together the two say that central simple K-algebras are closed under ⊗[K]. That closure is what lets the tensor product descend to a multiplication on Brauer classes. Note that the centrality proved here is centrality over the base field K: for a scalar extension L ⊗[K] A along a field extension L / K the statement wanted is centrality over L, which is a different statement, proved as TauCeti.Algebra.IsCentral.baseChange in TauCeti/Algebra/Central/BaseChange.lean.

References

This is part of the Tensor product of central simple is central simple bullet of Layer 4 of the semisimple algebras roadmap. See R. S. Pierce, Associative Algebras, GTM 88, Chapter 12, and P. Gille, T. Szamuely, Central Simple Algebras and Galois Cohomology, Chapter 2.

theorem TauCeti.Algebra.TensorProduct.forall_commute_tmul_one_iff {K : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring K] [Semiring A] [Semiring B] [Algebra K A] [Algebra K B] [Module.Free K B] [Algebra.IsCentral K A] {x : TensorProduct K A B} : (∀ (a : A), Commute (a ⊗ₜ[K] 1) x) ↔ ∃ (b : B), x = 1 ⊗ₜ[K] b

The centralizer of A ⊗ 1 in A ⊗[K] B is 1 ⊗ B, for A a central K-algebra and B free: an element of A ⊗[K] B commutes with every a ⊗ₜ 1 exactly when it is of the form 1 ⊗ₜ b.

This is Mathlib's Subalgebra.centralizer_coe_range_includeLeft_eq_center_tensorProduct, which computes that centralizer as Z(A) ⊗ B, specialized to Z(A) = K and repackaged as a statement about elements. Centrality of A is what shrinks the centralizer to 1 ⊗ B; without it Z(A) ⊗ B can be strictly larger.

instance TauCeti.Algebra.IsCentral.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] [Algebra.IsCentral K B] : Algebra.IsCentral K (TensorProduct K A B)

The tensor product of two central K-algebras is central. Mathlib has the two converses (Algebra.IsCentral.left_of_tensor_of_field and Algebra.IsCentral.right_of_tensor_of_field); this is the forward implication.