mathlib documentation

algebra.algebra.bilinear

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 linear_algebra.bilinear_map and linear_algebra.tensor_product unnecessarily.

def linear_map.mul (R : Type u_1) (A : Type u_2) [comm_semiring R] [non_unital_non_assoc_semiring A] [module R A] [smul_comm_class R A A] [is_scalar_tower R A A] :

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

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

Equations
def linear_map.mul' (R : Type u_1) (A : Type u_2) [comm_semiring R] [non_unital_non_assoc_semiring A] [module R A] [smul_comm_class R A A] [is_scalar_tower R A A] :

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

Equations
def linear_map.mul_left (R : Type u_1) {A : Type u_2} [comm_semiring R] [non_unital_non_assoc_semiring A] [module R A] [smul_comm_class R A A] [is_scalar_tower R A A] (a : A) :

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

Equations
def linear_map.mul_right (R : Type u_1) {A : Type u_2} [comm_semiring R] [non_unital_non_assoc_semiring A] [module R A] [smul_comm_class R A A] [is_scalar_tower R A A] (a : A) :

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

Equations
def linear_map.mul_left_right (R : Type u_1) {A : Type u_2} [comm_semiring R] [non_unital_non_assoc_semiring A] [module R A] [smul_comm_class R A A] [is_scalar_tower R A A] (ab : A × A) :

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

Equations
@[simp]
theorem linear_map.mul_apply' {R : Type u_1} {A : Type u_2} [comm_semiring R] [non_unital_non_assoc_semiring A] [module R A] [smul_comm_class R A A] [is_scalar_tower R A A] (a b : A) :
((linear_map.mul R A) a) b = a * b
@[simp]
theorem linear_map.mul_left_apply {R : Type u_1} {A : Type u_2} [comm_semiring R] [non_unital_non_assoc_semiring A] [module R A] [smul_comm_class R A A] [is_scalar_tower R A A] (a b : A) :
@[simp]
theorem linear_map.mul_right_apply {R : Type u_1} {A : Type u_2} [comm_semiring R] [non_unital_non_assoc_semiring A] [module R A] [smul_comm_class R A A] [is_scalar_tower R A A] (a b : A) :
@[simp]
theorem linear_map.mul_left_right_apply {R : Type u_1} {A : Type u_2} [comm_semiring R] [non_unital_non_assoc_semiring A] [module R A] [smul_comm_class R A A] [is_scalar_tower R A A] (a b x : A) :
(linear_map.mul_left_right R (a, b)) x = a * x * b
@[simp]
theorem linear_map.mul'_apply {R : Type u_1} {A : Type u_2} [comm_semiring R] [non_unital_non_assoc_semiring A] [module R A] [smul_comm_class R A A] [is_scalar_tower R A A] {a b : A} :
(linear_map.mul' R A) (a ⊗ₜ[R] b) = a * b
@[simp]
@[simp]
def non_unital_alg_hom.lmul (R : Type u_1) (A : Type u_2) [comm_semiring R] [non_unital_semiring A] [module R A] [smul_comm_class R A A] [is_scalar_tower R A 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 linear_map.mul.

Equations
@[simp]
theorem linear_map.commute_mul_left_right {R : Type u_1} {A : Type u_2} [comm_semiring R] [non_unital_semiring A] [module R A] [smul_comm_class R A A] [is_scalar_tower R A A] (a b : A) :
@[simp]
theorem linear_map.mul_left_mul {R : Type u_1} {A : Type u_2} [comm_semiring R] [non_unital_semiring A] [module R A] [smul_comm_class R A A] [is_scalar_tower R A A] (a b : A) :
@[simp]
theorem linear_map.mul_right_mul {R : Type u_1} {A : Type u_2} [comm_semiring R] [non_unital_semiring A] [module R A] [smul_comm_class R A A] [is_scalar_tower R A A] (a b : A) :
def algebra.lmul (R : Type u_1) (A : Type u_2) [comm_semiring R] [semiring A] [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 non_unital_alg_hom.mul.

Equations
@[simp]
theorem algebra.coe_lmul_eq_mul {R : Type u_1} {A : Type u_2} [comm_semiring R] [semiring A] [algebra R A] :
@[simp]
theorem linear_map.mul_left_eq_zero_iff {R : Type u_1} {A : Type u_2} [comm_semiring R] [semiring A] [algebra R A] (a : A) :
@[simp]
theorem linear_map.mul_right_eq_zero_iff {R : Type u_1} {A : Type u_2} [comm_semiring R] [semiring A] [algebra R A] (a : A) :
@[simp]
theorem linear_map.mul_left_one {R : Type u_1} {A : Type u_2} [comm_semiring R] [semiring A] [algebra R A] :
@[simp]
theorem linear_map.mul_right_one {R : Type u_1} {A : Type u_2} [comm_semiring R] [semiring A] [algebra R A] :
@[simp]
theorem linear_map.pow_mul_left {R : Type u_1} {A : Type u_2} [comm_semiring R] [semiring A] [algebra R A] (a : A) (n : ) :
@[simp]
theorem linear_map.pow_mul_right {R : Type u_1} {A : Type u_2} [comm_semiring R] [semiring A] [algebra R A] (a : A) (n : ) :
theorem linear_map.mul_left_injective {R : Type u_1} {A : Type u_2} [comm_semiring R] [ring A] [algebra R A] [no_zero_divisors A] {x : A} (hx : x 0) :
theorem linear_map.mul_right_injective {R : Type u_1} {A : Type u_2} [comm_semiring R] [ring A] [algebra R A] [no_zero_divisors A] {x : A} (hx : x 0) :
theorem linear_map.mul_injective {R : Type u_1} {A : Type u_2} [comm_semiring R] [ring A] [algebra R A] [no_zero_divisors A] {x : A} (hx : x 0) :