Facts about algebras involving bilinear maps and tensor products #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
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.
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
- linear_map.mul R A = linear_map.mk₂ R has_mul.mul _ _ _ _
The multiplication map on a non-unital algebra, as an R
-linear map from A ⊗[R] A
to A
.
Equations
- linear_map.mul' R A = tensor_product.lift (linear_map.mul R A)
The multiplication on the left in a non-unital algebra is a linear map.
Equations
- linear_map.mul_left R a = ⇑(linear_map.mul R A) a
The multiplication on the right in an algebra is a linear map.
Equations
- linear_map.mul_right R a = ⇑((linear_map.mul R A).flip) a
Simultaneous multiplication on the left and right is a linear map.
Equations
- linear_map.mul_left_right R ab = (linear_map.mul_right R ab.snd).comp (linear_map.mul_left R ab.fst)
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
- non_unital_alg_hom.lmul R A = {to_fun := (linear_map.mul R A).to_fun, map_smul' := _, map_zero' := _, map_add' := _, map_mul' := _}
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
.