Base change preserves and detects centrality

Let A be a central algebra over a field K and let L / K be a field extension. This file proves that the scalar extension L ⊗[K] A is central over L, and conversely that centrality of L ⊗[K] A over L forces centrality of A over K.

This is a genuinely different statement from the centrality over K proved in TauCeti/Algebra/Central/TensorProduct.lean: that one asks both factors to be central over K, and for a nontrivial extension the factor L is not.

The proof is short once the centralizer computation is available. The centre of L ⊗[K] A is contained in the centralizer of 1 ⊗ A, which is L ⊗ 1 because A is central over K; and L ⊗ 1 is exactly the image of L.

Main results

• TauCeti.Algebra.IsCentral.baseChange: L ⊗[K] A is central over L when A is central over K and L is a commutative K-algebra free as a K-module. It is an instance, so together with TauCeti.IsSimpleRing.tensorProduct_of_isCentral_right instance search sees L ⊗[K] A as a central simple L-algebra with no glue.
• TauCeti.Algebra.IsCentral.of_baseChange: the converse over a field K, so centrality is not merely preserved by base change but detected by it.
• TauCeti.Algebra.isCentral_baseChange_iff: the two packaged as an equivalence.

Central simplicity of a scalar extension, its degree, and the compatibility of base change with ⊗ and ᵐᵒᵖ are assembled from these in TauCeti/Algebra/CentralSimple/BaseChange.lean.

Implementation notes

The forward direction is stated over a commutative semiring K and a commutative K-algebra L that is free as a K-module, the hypotheses the centralizer computation TauCeti.Algebra.TensorProduct.forall_commute_tmul_one_iff needs; a field extension is the case of interest and satisfies them. The converse genuinely needs K to be a field: it splits off a K-linear retraction L → K of the structure map, which is where the vector-space hypothesis enters, and L need only be a nontrivial commutative K-algebra.

Both directions are about the L-algebra structure on L ⊗[K] A coming from the left factor, which is Mathlib's Algebra.TensorProduct.leftAlgebra.

References

This is part of the Base change preserves central simplicity, then is a homomorphism bullet of Layer 6 of the semisimple algebras roadmap. See P. Gille, T. Szamuely, Central Simple Algebras and Galois Cohomology, Section 2.2, and R. S. Pierce, Associative Algebras, GTM 88, Chapter 12.

instance TauCeti.Algebra.IsCentral.baseChange (K : Type u_1) (L : Type u_2) (A : Type u_3) [CommSemiring K] [CommSemiring L] [Algebra K L] [Module.Free K L] [Semiring A] [Algebra K A] [Algebra.IsCentral K A] : Algebra.IsCentral L (TensorProduct K L A)

Base change preserves centrality. If A is a central K-algebra and L is a commutative K-algebra which is free as a K-module, then the scalar extension L ⊗[K] A is central over L.

Freeness of L and centrality of A are both used, through the centralizer computation TauCeti.Algebra.TensorProduct.forall_commute_tmul_one_iff: an element of L ⊗[K] A commuting with every 1 ⊗ₜ a is of the form l ⊗ₜ 1, that is, a scalar. Centrality of A cannot be dropped, and ℂ ⊗[ℝ] ℂ is the standard witness.

theorem TauCeti.Algebra.IsCentral.of_baseChange {K : Type u_1} {L : Type u_2} {A : Type u_3} [Field K] [CommSemiring L] [Nontrivial L] [Algebra K L] [Semiring A] [Algebra K A] [Algebra.IsCentral L (TensorProduct K L A)] : Algebra.IsCentral K A

Base change detects centrality. Over a field K, if the scalar extension L ⊗[K] A is central over a nontrivial commutative K-algebra L, then A was already central over K.

The centre of A lands in the centre of L ⊗[K] A under a ↦ 1 ⊗ₜ a, so a central a satisfies 1 ⊗ₜ a = l ⊗ₜ 1 for some l : L. Applying L ⊗[K] A → A built from a K-linear retraction of K → L turns that identity into a = g l • 1.

@[simp]

theorem TauCeti.Algebra.isCentral_baseChange_iff (K : Type u_1) (L : Type u_2) (A : Type u_3) [Field K] [CommSemiring L] [Nontrivial L] [Algebra K L] [Semiring A] [Algebra K A] : Algebra.IsCentral L (TensorProduct K L A) ↔ Algebra.IsCentral K A

Centrality passes both ways along a scalar extension. Over a field K, an algebra A is central exactly when its scalar extension along a nontrivial commutative K-algebra L is central over L. Freeness of L is automatic here, K being a field.