# 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.

source
def LinearMap.mulLeft (R : Type u_1) {A : Type u_2} [Semiring R] [NonUnitalNonAssocSemiring A] [Module R A] [SMulCommClass R A A] (a : A) :
A →ₗ[R] A

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

Note that this only assumes `SMulCommClass R A A`, so that it also works for `R := Aᵐᵒᵖ`.

When `A` is unital and associative, this is the same as `DistribMulAction.toLinearMap R A a`

Equations

- LinearMap.mulLeft R a = { toFun := fun (x : A) => a * x, map_add' := ⋯, map_smul' := ⋯ }

Instances For

source
@[simp]
theorem LinearMap.mulLeft_apply (R : Type u_1) {A : Type u_2} [Semiring R] [NonUnitalNonAssocSemiring A] [Module R A] [SMulCommClass R A A] (a b : A) :
(mulLeft R a) b = a * b
source
@[simp]
theorem LinearMap.mulLeft_toAddMonoidHom (R : Type u_1) {A : Type u_2} [Semiring R] [NonUnitalNonAssocSemiring A] [Module R A] [SMulCommClass R A A] (a : A) :
↑(mulLeft R a) = AddMonoidHom.mulLeft a
source
@[simp]
theorem LinearMap.mulLeft_zero_eq_zero (R : Type u_1) (A : Type u_2) [Semiring R] [NonUnitalNonAssocSemiring A] [Module R A] [SMulCommClass R A A] :
mulLeft R 0 = 0
source
def LinearMap.mulRight (R : Type u_1) {A : Type u_2} [Semiring R] [NonUnitalNonAssocSemiring A] [Module R A] [IsScalarTower R A A] (b : A) :
A →ₗ[R] A

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

Note that this only assumes `IsScalarTower R A A`, so that it also works for `R := A`.

When `A` is unital and associative, this is the same as `DistribMulAction.toLinearMap R A (MulOpposite.op b)`.

Equations

- LinearMap.mulRight R b = { toFun := fun (x : A) => x * b, map_add' := ⋯, map_smul' := ⋯ }

Instances For

source
@[simp]
theorem LinearMap.mulRight_apply (R : Type u_1) {A : Type u_2} [Semiring R] [NonUnitalNonAssocSemiring A] [Module R A] [IsScalarTower R A A] (a b : A) :
(mulRight R a) b = b * a
source
@[simp]
theorem LinearMap.mulRight_toAddMonoidHom (R : Type u_1) {A : Type u_2} [Semiring R] [NonUnitalNonAssocSemiring A] [Module R A] [IsScalarTower R A A] (a : A) :
↑(mulRight R a) = AddMonoidHom.mulRight a
source
@[simp]
theorem LinearMap.mulRight_zero_eq_zero (R : Type u_1) (A : Type u_2) [Semiring R] [NonUnitalNonAssocSemiring A] [Module R A] [IsScalarTower R A A] :
mulRight R 0 = 0
source
def LinearMap.mul (R : Type u_1) (A : Type u_2) [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [SMulCommClass R A A] [IsScalarTower R A A] :
A →ₗ[R] A →ₗ[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

- LinearMap.mul R A = LinearMap.mk₂ R (fun (x1 x2 : A) => x1 * x2) ⋯ ⋯ ⋯ ⋯

Instances For

source
@[simp]
theorem LinearMap.mul_apply_apply (R : Type u_1) (A : Type u_2) [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [SMulCommClass R A A] [IsScalarTower R A A] (m x2✝ : A) :
((mul R A) m) x2✝ = m * x2✝
source
def LinearMap.mul' (R : Type u_1) (A : Type u_2) [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [SMulCommClass R A A] [IsScalarTower R A A] :
TensorProduct R A A →ₗ[R] A

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

Equations

- LinearMap.mul' R A = TensorProduct.lift (LinearMap.mul R A)

Instances For

source
def RingTheory.LinearMap.termμ :
Lean.ParserDescr

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

Equations

- RingTheory.LinearMap.termμ = Lean.ParserDescr.node `RingTheory.LinearMap.termμ 1024 (Lean.ParserDescr.symbol "μ")

Instances For

source
def RingTheory.LinearMap.«termμ[_]» :
Lean.ParserDescr

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

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
def LinearMap.mulLeftRight (R : Type u_1) {A : Type u_2} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [SMulCommClass R A A] [IsScalarTower R A A] (ab : A × A) :
A →ₗ[R] A

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

Equations

- LinearMap.mulLeftRight R ab = LinearMap.mulRight R ab.2 ∘ₗ LinearMap.mulLeft R ab.1

Instances For

source
@[simp]
theorem LinearMap.mul_apply' {R : Type u_1} {A : Type u_2} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [SMulCommClass R A A] [IsScalarTower R A A] (a b : A) :
((mul R A) a) b = a * b
source
@[simp]
theorem LinearMap.mulLeftRight_apply {R : Type u_1} {A : Type u_2} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [SMulCommClass R A A] [IsScalarTower R A A] (a b x : A) :
(mulLeftRight R (a, b)) x = a * x * b
source
@[simp]
theorem LinearMap.mul'_apply {R : Type u_1} {A : Type u_2} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [SMulCommClass R A A] [IsScalarTower R A A] {a b : A} :
(mul' R A) (a ⊗ₜ[R] b) = a * b
source
theorem LinearMap.lift_lsmul_mul_eq_lsmul_lift_lsmul {R : Type u_1} [CommSemiring R] {M : Type u_4} [AddCommMonoid M] [Module R M] {r : R} :
TensorProduct.lift (lsmul R M ∘ₗ (mul R R) r) = (lsmul R M) r ∘ₗ TensorProduct.lift (lsmul R M)
source
@[simp]
theorem LinearMap.mulLeft_mul (R : Type u_1) (A : Type u_2) [Semiring R] [NonUnitalSemiring A] [Module R A] [SMulCommClass R A A] (a b : A) :
mulLeft R (a * b) = mulLeft R a ∘ₗ mulLeft R b
source
@[simp]
theorem LinearMap.mulRight_mul (R : Type u_1) (A : Type u_2) [Semiring R] [NonUnitalSemiring A] [Module R A] [IsScalarTower R A A] (a b : A) :
mulRight R (a * b) = mulRight R b ∘ₗ mulRight R a
source
def NonUnitalAlgHom.lmul (R : Type u_1) (A : Type u_2) [CommSemiring R] [NonUnitalSemiring A] [Module R A] [SMulCommClass R A A] [IsScalarTower R A A] :
A →ₙₐ[R] Module.End 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

- NonUnitalAlgHom.lmul R A = { toFun := (LinearMap.mul R A).toFun, map_smul' := ⋯, map_zero' := ⋯, map_add' := ⋯, map_mul' := ⋯ }

Instances For

source
@[simp]
theorem NonUnitalAlgHom.coe_lmul_eq_mul {R : Type u_1} {A : Type u_2} [CommSemiring R] [NonUnitalSemiring A] [Module R A] [SMulCommClass R A A] [IsScalarTower R A A] :
⇑(lmul R A) = ⇑(LinearMap.mul R A)
source
theorem LinearMap.commute_mulLeft_right {R : Type u_1} {A : Type u_2} [CommSemiring R] [NonUnitalSemiring A] [Module R A] [SMulCommClass R A A] [IsScalarTower R A A] (a b : A) :
Commute (mulLeft R a) (mulRight R b)
source
theorem LinearMap.map_mul_iff {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [NonUnitalSemiring A] [NonUnitalSemiring B] [Module R B] [Module R A] [SMulCommClass R A A] [IsScalarTower R A A] [SMulCommClass R B B] [IsScalarTower R B B] (f : A →ₗ[R] B) :
(∀ (x y : A), f (x * y) = f x * f y) ↔ (mul R A).compr₂ f = (mul R B ∘ₗ 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 `LinearMap`s, this lemma allows various specialized `ext` lemmas about `→ₗ[R]` to then be applied.

This is the `LinearMap` version of `AddMonoidHom.map_mul_iff`.

source
@[simp]
theorem LinearMap.mulLeft_inj {R : Type u_4} {A : Type u_5} [Semiring R] [NonAssocSemiring A] [Module R A] [SMulCommClass R A A] {a b : A} :
mulLeft R a = mulLeft R b ↔ a = b
source
@[simp]
theorem LinearMap.mulRight_inj {R : Type u_4} {A : Type u_5} [Semiring R] [NonAssocSemiring A] [Module R A] [IsScalarTower R A A] {a b : A} :
mulRight R a = mulRight R b ↔ a = b
source
@[simp]
theorem LinearMap.mulLeft_one (R : Type u_1) (A : Type u_2) [Semiring R] [Semiring A] [Module R A] [SMulCommClass R A A] :
mulLeft R 1 = id
source
@[simp]
theorem LinearMap.mulLeft_eq_zero_iff (R : Type u_1) (A : Type u_2) [Semiring R] [Semiring A] [Module R A] [SMulCommClass R A A] (a : A) :
mulLeft R a = 0 ↔ a = 0
source
@[simp]
theorem LinearMap.pow_mulLeft (R : Type u_1) (A : Type u_2) [Semiring R] [Semiring A] [Module R A] [SMulCommClass R A A] (a : A) (n : ℕ) :
mulLeft R a ^ n = mulLeft R (a ^ n)
source
@[simp]
theorem LinearMap.mulRight_one (R : Type u_1) (A : Type u_2) [Semiring R] [Semiring A] [Module R A] [IsScalarTower R A A] :
mulRight R 1 = id
source
@[simp]
theorem LinearMap.mulRight_eq_zero_iff (R : Type u_1) (A : Type u_2) [Semiring R] [Semiring A] [Module R A] [IsScalarTower R A A] (a : A) :
mulRight R a = 0 ↔ a = 0
source
@[simp]
theorem LinearMap.pow_mulRight (R : Type u_1) (A : Type u_2) [Semiring R] [Semiring A] [Module R A] [IsScalarTower R A A] (a : A) (n : ℕ) :
mulRight R a ^ n = mulRight R (a ^ n)
source
def Algebra.lmul (R : Type u_1) (A : Type u_2) [CommSemiring R] [Semiring A] [Algebra R A] :
A →ₐ[R] Module.End 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.lmul`.

Equations

- Algebra.lmul R A = { toFun := (NonUnitalAlgHom.lmul R A).toFun, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯, commutes' := ⋯ }

Instances For

source
@[simp]
theorem Algebra.coe_lmul_eq_mul {R : Type u_1} {A : Type u_2} [CommSemiring R] [Semiring A] [Algebra R A] :
⇑(lmul R A) = ⇑(LinearMap.mul R A)
source
theorem Algebra.lmul_injective {R : Type u_1} {A : Type u_2} [CommSemiring R] [Semiring A] [Algebra R A] :
Function.Injective ⇑(lmul R A)
source
theorem Algebra.lmul_isUnit_iff {R : Type u_1} {A : Type u_2} [CommSemiring R] [Semiring A] [Algebra R A] {x : A} :
IsUnit ((lmul R A) x) ↔ IsUnit x
source
theorem LinearMap.toSpanSingleton_eq_algebra_linearMap {R : Type u_1} {A : Type u_2} [CommSemiring R] [Semiring A] [Algebra R A] :
toSpanSingleton R A 1 = Algebra.linearMap R A
source
@[simp]
theorem LinearMap.flip_mul {R : Type u_1} {A : Type u_2} [CommSemiring R] [NonUnitalCommSemiring A] [Module R A] [SMulCommClass R A A] [IsScalarTower R A A] :
(mul R A).flip = mul R A
source
theorem LinearMap.mul'_comp_comm {R : Type u_1} {A : Type u_2} [CommSemiring R] [NonUnitalCommSemiring A] [Module R A] [SMulCommClass R A A] [IsScalarTower R A A] :
mul' R A ∘ₗ ↑(TensorProduct.comm R A A) = mul' R A
source
theorem LinearMap.mul'_comm {R : Type u_1} {A : Type u_2} [CommSemiring R] [NonUnitalCommSemiring A] [Module R A] [SMulCommClass R A A] [IsScalarTower R A A] (x : TensorProduct R A A) :
(mul' R A) ((TensorProduct.comm R A A) x) = (mul' R A) x
source
theorem NonUnitalAlgHom.comp_mul' {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [NonUnitalSemiring A] [Module R A] [SMulCommClass R A A] [IsScalarTower R A A] [NonUnitalNonAssocSemiring B] [Module R B] [SMulCommClass R B B] [IsScalarTower R B B] (f : A →ₙₐ[R] B) :
↑f ∘ₗ LinearMap.mul' R A = LinearMap.mul' R B ∘ₗ TensorProduct.map ↑f ↑f
source
theorem AlgHom.comp_mul' {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] (f : A →ₐ[R] B) :
f.toLinearMap ∘ₗ LinearMap.mul' R A = LinearMap.mul' R B ∘ₗ TensorProduct.map f.toLinearMap f.toLinearMap