Multiplying pure tensors in A ⊗[K] B

Two formulas for multiplication by a pure tensor a ⊗ₜ 1 in an algebra tensor product, one on each side, and two criteria for pure tensors to anticommute. All are general facts about A ⊗[K] B over a commutative semiring: none needs A or B to be central, simple, or even a ring.

Main results

• Algebra.TensorProduct.tmul_one_mul_eq_smul: multiplying on the left by a ⊗ₜ 1 is the left A-module action on A ⊗[K] B.
• Algebra.TensorProduct.basis_repr_mul_tmul_one: multiplying on the right by a ⊗ₜ 1 multiplies each coordinate against Algebra.TensorProduct.basis by a on the right.

All are declared into Mathlib's root Algebra.TensorProduct namespace, which houses the algebra tensor product's multiplicative API, rather than into a TauCeti.-prefixed copy of it. (The underlying type is the root TensorProduct; Algebra.TensorProduct is where its algebra structure and the lemmas about it live.)

@[simp]

theorem Algebra.TensorProduct.tmul_one_mul_eq_smul {K : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring K] [Semiring A] [Semiring B] [Algebra K A] [Algebra K B] (a : A) (x : TensorProduct K A B) : a ⊗ₜ[K] 1 * x = a • x

Left multiplication by a ⊗ₜ 1 on A ⊗[K] B is the left A-module action, the one that Algebra.TensorProduct.basis is a basis for.

This is Mathlib's smul_one_mul, available because Algebra.TensorProduct.isScalarTower_right makes A ⊗[K] B a scalar tower over A; all this adds is the identification of a • 1 with a ⊗ₜ 1. (Algebra.smul_def is not available here: A is not assumed commutative, so there is no Algebra A (A ⊗[K] B) instance.)

theorem Algebra.TensorProduct.tmul_anticommute_of_left {K : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring K] [Semiring A] [Semiring B] [Algebra K A] [Algebra K B] {x x' : A} {y y' : B} (hx : x * x' + x' * x = 0) (hy : Commute y y') : x ⊗ₜ[K] y * x' ⊗ₜ[K] y' + x' ⊗ₜ[K] y' * x ⊗ₜ[K] y = 0

Pure tensors anticommute when their left factors anticommute and right factors commute.

theorem Algebra.TensorProduct.tmul_anticommute_of_right {K : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring K] [Semiring A] [Semiring B] [Algebra K A] [Algebra K B] {x x' : A} {y y' : B} (hx : Commute x x') (hy : y * y' + y' * y = 0) : x ⊗ₜ[K] y * x' ⊗ₜ[K] y' + x' ⊗ₜ[K] y' * x ⊗ₜ[K] y = 0

Pure tensors anticommute when their left factors commute and right factors anticommute.

@[simp]

theorem Algebra.TensorProduct.basis_repr_mul_tmul_one {K : Type u_1} {A : Type u_2} {B : Type u_3} {ι : Type u_4} [CommSemiring K] [Semiring A] [Semiring B] [Algebra K A] [Algebra K B] (𝓑 : Module.Basis ι K B) (a : A) (x : TensorProduct K A B) (j : ι) : ((basis A 𝓑).repr (x * a ⊗ₜ[K] 1)) j = ((basis A 𝓑).repr x) j * a

Multiplying by a ⊗ₜ 1 on the right multiplies each coordinate of x by a on the right.

Unlike the left-handed Algebra.TensorProduct.tmul_one_mul_eq_smul this is not an instance of the generic scalar-action API, since right multiplication is not the module action Algebra.TensorProduct.basis is a basis for.