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

@[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✝

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.

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.

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.

@[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

@[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

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)

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.

@[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)

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)

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 LinearMaps, this lemma allows various specialized ext lemmas about →ₗ[R] to then be applied.

This is the LinearMap version of AddMonoidHom.map_mul_iff.

@[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)

@[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)

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.

@[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)

theorem Algebra.lmul_injective {R : Type u_1} {A : Type u_2} [CommSemiring R] [Semiring A] [Algebra R A] : Function.Injective ⇑(lmul R A)

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

theorem LinearMap.toSpanSingleton_one_eq_algebraLinearMap {R : Type u_1} {A : Type u_2} [CommSemiring R] [Semiring A] [Algebra R A] : toSpanSingleton R A 1 = Algebra.linearMap R A

@[deprecated LinearMap.toSpanSingleton_one_eq_algebraLinearMap (since := "2025-12-30")]

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

Alias of LinearMap.toSpanSingleton_one_eq_algebraLinearMap.

def LinearMap.mul'' (R : Type u_1) (A : Type u_2) [CommSemiring R] [Semiring A] [Algebra R A] : TensorProduct R A A →ₗ[A] A

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

@[simp]

theorem LinearMap.mul''_apply (R : Type u_1) (A : Type u_2) [CommSemiring R] [Semiring A] [Algebra R A] (a✝ : TensorProduct R A A) : (mul'' R A) a✝ = (TensorProduct.liftAux (mul R A)) a✝

@[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

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

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

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

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