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

Instances For

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.

Instances For

source

def LinearMap.mulLeft (R : Type u_1) {A : Type u_2} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [SMulCommClass R A A] [IsScalarTower R A A] (a : A) :

A →ₗ[R] A

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

Instances For

source

def LinearMap.mulRight (R : Type u_1) {A : Type u_2} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [SMulCommClass R A A] [IsScalarTower R A A] (a : A) :

A →ₗ[R] A

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

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.

Instances For

source

@[simp]

theorem LinearMap.mulLeft_toAddMonoidHom (R : Type u_1) {A : Type u_2} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [SMulCommClass R A A] [IsScalarTower R A A] (a : A) :

↑(LinearMap.mulLeft R a) = AddMonoidHom.mulLeft a

source

@[simp]

theorem LinearMap.mulRight_toAddMonoidHom (R : Type u_1) {A : Type u_2} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [SMulCommClass R A A] [IsScalarTower R A A] (a : A) :

↑(LinearMap.mulRight R a) = AddMonoidHom.mulRight a

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 : A) (b : A) :

↑(↑(LinearMap.mul R A) a) b = a * b

source

@[simp]

theorem LinearMap.mulLeft_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 : A) (b : A) :

↑(LinearMap.mulLeft R a) b = a * b

source

@[simp]

theorem LinearMap.mulRight_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 : A) (b : A) :

↑(LinearMap.mulRight R a) b = b * a

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 : A) (b : A) (x : A) :

↑(LinearMap.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 : A} {b : A} :

↑(LinearMap.mul' R A) (a ⊗ₜ[R] b) = a * b

source

@[simp]

theorem LinearMap.mulLeft_zero_eq_zero {R : Type u_1} {A : Type u_2} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [SMulCommClass R A A] [IsScalarTower R A A] :

LinearMap.mulLeft R 0 = 0

source

@[simp]

theorem LinearMap.mulRight_zero_eq_zero {R : Type u_1} {A : Type u_2} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [SMulCommClass R A A] [IsScalarTower R A A] :

LinearMap.mulRight R 0 = 0

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.

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] :

↑(NonUnitalAlgHom.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 : A) (b : A) :

Commute (LinearMap.mulLeft R a) (LinearMap.mulRight R b)

source

@[simp]

theorem LinearMap.mulLeft_mul {R : Type u_1} {A : Type u_2} [CommSemiring R] [NonUnitalSemiring A] [Module R A] [SMulCommClass R A A] [IsScalarTower R A A] (a : A) (b : A) :

LinearMap.mulLeft R (a * b) = LinearMap.comp (LinearMap.mulLeft R a) (LinearMap.mulLeft R b)

source

@[simp]

theorem LinearMap.mulRight_mul {R : Type u_1} {A : Type u_2} [CommSemiring R] [NonUnitalSemiring A] [Module R A] [SMulCommClass R A A] [IsScalarTower R A A] (a : A) (b : A) :

LinearMap.mulRight R (a * b) = LinearMap.comp (LinearMap.mulRight R b) (LinearMap.mulRight R a)

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

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] :

↑(Algebra.lmul R A) = ↑(LinearMap.mul R A)

source

@[simp]

theorem LinearMap.mulLeft_eq_zero_iff {R : Type u_1} {A : Type u_2} [CommSemiring R] [Semiring A] [Algebra R A] (a : A) :

LinearMap.mulLeft R a = 0 ↔ a = 0

source

@[simp]

theorem LinearMap.mulRight_eq_zero_iff {R : Type u_1} {A : Type u_2} [CommSemiring R] [Semiring A] [Algebra R A] (a : A) :

LinearMap.mulRight R a = 0 ↔ a = 0

source

@[simp]

theorem LinearMap.mulLeft_one {R : Type u_1} {A : Type u_2} [CommSemiring R] [Semiring A] [Algebra R A] :

LinearMap.mulLeft R 1 = LinearMap.id

source

@[simp]

theorem LinearMap.mulRight_one {R : Type u_1} {A : Type u_2} [CommSemiring R] [Semiring A] [Algebra R A] :

LinearMap.mulRight R 1 = LinearMap.id

source

@[simp]

theorem LinearMap.pow_mulLeft {R : Type u_1} {A : Type u_2} [CommSemiring R] [Semiring A] [Algebra R A] (a : A) (n : ℕ) :

LinearMap.mulLeft R a ^ n = LinearMap.mulLeft R (a ^ n)

source

@[simp]

theorem LinearMap.pow_mulRight {R : Type u_1} {A : Type u_2} [CommSemiring R] [Semiring A] [Algebra R A] (a : A) (n : ℕ) :

LinearMap.mulRight R a ^ n = LinearMap.mulRight R (a ^ n)

source

theorem LinearMap.mulLeft_injective {R : Type u_1} {A : Type u_2} [CommSemiring R] [Ring A] [Algebra R A] [NoZeroDivisors A] {x : A} (hx : x ≠ 0) :

Function.Injective ↑(LinearMap.mulLeft R x)

source

theorem LinearMap.mulRight_injective {R : Type u_1} {A : Type u_2} [CommSemiring R] [Ring A] [Algebra R A] [NoZeroDivisors A] {x : A} (hx : x ≠ 0) :

Function.Injective ↑(LinearMap.mulRight R x)

source

theorem LinearMap.mul_injective {R : Type u_1} {A : Type u_2} [CommSemiring R] [Ring A] [Algebra R A] [NoZeroDivisors A] {x : A} (hx : x ≠ 0) :

Function.Injective ↑(↑(LinearMap.mul R A) x)