Lemmas about tensor products of central algebras

In this file we prove for algebras B and C over a field K that if B ⊗[K] C is a central algebra and B, C nontrivial, then both B and C are central algebras.

Main Results

• Algebra.IsCentral.left_of_tensor_of_field: If B C are K-algebras where K is a field, C is nontrivial and B ⊗[K] C is a central algebra over K, then B is a central algebra over K.
• Algebra.IsCentral.right_of_tensor_of_field: If B C are K-algebras where K is a field, B is nontrivial and B ⊗[K] C is a central algebra over K, then C is a central algebra over K.

Tags

Central Algebras, Central Simple Algebras, Noncommutative Algebra

theorem Algebra.TensorProduct.includeLeft_map_center_le (K : Type u_1) (B : Type u_2) (C : Type u_3) [CommSemiring K] [Semiring B] [Semiring C] [Algebra K B] [Algebra K C] : Subalgebra.map includeLeft (Subalgebra.center K B) ≤ Subalgebra.center K (TensorProduct K B C)

theorem Algebra.TensorProduct.includeRight_map_center_le (K : Type u_1) (B : Type u_2) (C : Type u_3) [CommSemiring K] [Semiring B] [Semiring C] [Algebra K B] [Algebra K C] : Subalgebra.map includeRight (Subalgebra.center K C) ≤ Subalgebra.center K (TensorProduct K B C)

theorem Algebra.IsCentral.left_of_tensor (K : Type u_1) (B : Type u_2) (C : Type u_3) [CommSemiring K] [Semiring B] [Semiring C] [Algebra K B] [Algebra K C] (inj : Function.Injective ⇑(algebraMap K C)) [Module.Flat K B] [hbc : IsCentral K (TensorProduct K B C)] : IsCentral K B

theorem Algebra.IsCentral.right_of_tensor (K : Type u_1) (B : Type u_2) (C : Type u_3) [CommSemiring K] [Semiring B] [Semiring C] [Algebra K B] [Algebra K C] (inj : Function.Injective ⇑(algebraMap K B)) [Module.Flat K C] [IsCentral K (TensorProduct K B C)] : IsCentral K C

theorem Algebra.IsCentral.left_of_tensor_of_field (K : Type u_4) (B : Type u_5) (C : Type u_6) [Field K] [Ring B] [Ring C] [Nontrivial C] [Algebra K B] [Algebra K C] [IsCentral K (TensorProduct K B C)] : IsCentral K B

Let B and C be two algebras over a field K, if B ⊗[K] C is central and C is non-trivial, then B is central.

theorem Algebra.IsCentral.right_of_tensor_of_field (K : Type u_4) (B : Type u_5) (C : Type u_6) [Field K] [Ring B] [Ring C] [Nontrivial B] [Algebra K B] [Algebra K C] [IsCentral K (TensorProduct K B C)] : IsCentral K C

Let B and C be two algebras over a field K, if B ⊗[K] C is central and B is non-trivial, then C is central.