# Facts about algebras involving bilinear maps and tensor products #

We move a few basic statements about algebras out of Algebra.Algebra.Basic, in order to avoid importing LinearAlgebra.BilinearMap and LinearAlgebra.TensorProduct unnecessarily.

def LinearMap.mul (R : Type u_1) (A : Type u_2) [] [Module R A] [] [] :

The multiplication in a non-unital non-associative algebra is a bilinear map.

A weaker version of this for semirings exists as AddMonoidHom.mul.

Equations
Instances For
noncomputable def LinearMap.mul' (R : Type u_1) (A : Type u_2) [] [Module R A] [] [] :

The multiplication map on a non-unital algebra, as an R-linear map from A ⊗[R] A to A.

Equations
Instances For
def LinearMap.mulLeft (R : Type u_1) {A : Type u_2} [] [Module R A] [] [] (a : A) :

The multiplication on the left in a non-unital algebra is a linear map.

Equations
Instances For
def LinearMap.mulRight (R : Type u_1) {A : Type u_2} [] [Module R A] [] [] (a : A) :

The multiplication on the right in an algebra is a linear map.

Equations
Instances For
def LinearMap.mulLeftRight (R : Type u_1) {A : Type u_2} [] [Module R A] [] [] (ab : A × A) :

Simultaneous multiplication on the left and right is a linear map.

Equations
Instances For
@[simp]
theorem LinearMap.mulLeft_toAddMonoidHom (R : Type u_1) {A : Type u_2} [] [Module R A] [] [] (a : A) :
@[simp]
theorem LinearMap.mulRight_toAddMonoidHom (R : Type u_1) {A : Type u_2} [] [Module R A] [] [] (a : A) :
@[simp]
theorem LinearMap.mul_apply' {R : Type u_1} {A : Type u_2} [] [Module R A] [] [] (a : A) (b : A) :
((LinearMap.mul R A) a) b = a * b
@[simp]
theorem LinearMap.mulLeft_apply {R : Type u_1} {A : Type u_2} [] [Module R A] [] [] (a : A) (b : A) :
b = a * b
@[simp]
theorem LinearMap.mulRight_apply {R : Type u_1} {A : Type u_2} [] [Module R A] [] [] (a : A) (b : A) :
b = b * a
@[simp]
theorem LinearMap.mulLeftRight_apply {R : Type u_1} {A : Type u_2} [] [Module R A] [] [] (a : A) (b : A) (x : A) :
(LinearMap.mulLeftRight R (a, b)) x = a * x * b
@[simp]
theorem LinearMap.mul'_apply {R : Type u_1} {A : Type u_2} [] [Module R A] [] [] {a : A} {b : A} :
(LinearMap.mul' R A) (a ⊗ₜ[R] b) = a * b
@[simp]
theorem LinearMap.mulLeft_zero_eq_zero {R : Type u_1} {A : Type u_2} [] [Module R A] [] [] :
= 0
@[simp]
theorem LinearMap.mulRight_zero_eq_zero {R : Type u_1} {A : Type u_2} [] [Module R A] [] [] :
= 0
def NonUnitalAlgHom.lmul (R : Type u_1) (A : Type u_2) [] [Module R A] [] [] :

The multiplication in a non-unital algebra is a bilinear map.

A weaker version of this for non-unital non-associative algebras exists as LinearMap.mul.

Equations
• = { toFun := (LinearMap.mul R A).toFun, map_smul' := , map_zero' := , map_add' := , map_mul' := }
Instances For
@[simp]
theorem NonUnitalAlgHom.coe_lmul_eq_mul {R : Type u_1} {A : Type u_2} [] [Module R A] [] [] :
= (LinearMap.mul R A)
theorem LinearMap.commute_mulLeft_right {R : Type u_1} {A : Type u_2} [] [Module R A] [] [] (a : A) (b : A) :
@[simp]
theorem LinearMap.mulLeft_mul {R : Type u_1} {A : Type u_2} [] [Module R A] [] [] (a : A) (b : A) :
LinearMap.mulLeft R (a * b) = ∘ₗ
@[simp]
theorem LinearMap.mulRight_mul {R : Type u_1} {A : Type u_2} [] [Module R A] [] [] (a : A) (b : A) :
LinearMap.mulRight R (a * b) = ∘ₗ
theorem LinearMap.map_mul_iff {R : Type u_1} {A : Type u_2} {B : Type u_3} [] [] [] [Algebra R A] [Algebra R B] (f : A →ₗ[R] B) :
(∀ (x y : A), f (x * y) = f x * f y) (LinearMap.mul R A).compr₂ f = ( ∘ₗ f).compl₂ f

A LinearMap preserves multiplication if pre- and post- composition with LinearMap.mul are equivalent. By converting the statement into an equality of LinearMaps, this lemma allows various specialized ext lemmas about →ₗ[R] to then be applied.

This is the LinearMap version of AddMonoidHom.map_mul_iff.

def Algebra.lmul (R : Type u_1) (A : Type u_2) [] [] [Algebra R A] :

The multiplication in an algebra is an algebra homomorphism into the endomorphisms on the algebra.

A weaker version of this for non-unital algebras exists as NonUnitalAlgHom.mul.

Equations
• = { toFun := (LinearMap.mul R A).toFun, map_one' := , map_mul' := , map_zero' := , map_add' := , commutes' := }
Instances For
@[simp]
theorem Algebra.coe_lmul_eq_mul {R : Type u_1} {A : Type u_2} [] [] [Algebra R A] :
(Algebra.lmul R A) = (LinearMap.mul R A)
theorem Algebra.lmul_injective {R : Type u_1} {A : Type u_2} [] [] [Algebra R A] :
theorem Algebra.lmul_isUnit_iff {R : Type u_1} {A : Type u_2} [] [] [Algebra R A] {x : A} :
@[simp]
theorem LinearMap.mulLeft_eq_zero_iff {R : Type u_1} {A : Type u_2} [] [] [Algebra R A] (a : A) :
= 0 a = 0
@[simp]
theorem LinearMap.mulRight_eq_zero_iff {R : Type u_1} {A : Type u_2} [] [] [Algebra R A] (a : A) :
= 0 a = 0
@[simp]
theorem LinearMap.mulLeft_one {R : Type u_1} {A : Type u_2} [] [] [Algebra R A] :
= LinearMap.id
@[simp]
theorem LinearMap.mulRight_one {R : Type u_1} {A : Type u_2} [] [] [Algebra R A] :
= LinearMap.id
@[simp]
theorem LinearMap.pow_mulLeft {R : Type u_1} {A : Type u_2} [] [] [Algebra R A] (a : A) (n : ) :
^ n = LinearMap.mulLeft R (a ^ n)
@[simp]
theorem LinearMap.pow_mulRight {R : Type u_1} {A : Type u_2} [] [] [Algebra R A] (a : A) (n : ) :
^ n = LinearMap.mulRight R (a ^ n)
theorem LinearMap.mulLeft_injective {R : Type u_1} {A : Type u_2} [] [Ring A] [Algebra R A] [] {x : A} (hx : x 0) :
theorem LinearMap.mulRight_injective {R : Type u_1} {A : Type u_2} [] [Ring A] [Algebra R A] [] {x : A} (hx : x 0) :
theorem LinearMap.mul_injective {R : Type u_1} {A : Type u_2} [] [Ring A] [Algebra R A] [] {x : A} (hx : x 0) :