Lie homomorphisms from products to tensor products

Two Lie homomorphisms into associative algebras induce a Lie homomorphism from the product of their domains to the tensor product of their codomains. The two images commute because they lie in separate tensor factors.

Main definitions

• LieHom.prodToTensor: the induced Lie homomorphism from a product to a tensor product.

def LieHom.prodToTensor {R : Type u} {L : Type v} {M : Type w} {A : Type x} {B : Type y} [CommRing R] [LieRing L] [LieAlgebra R L] [LieRing M] [LieAlgebra R M] [Ring A] [Algebra R A] [Ring B] [Algebra R B] (f : L →ₗ⁅R⁆ A) (g : M →ₗ⁅R⁆ B) : L × M →ₗ⁅R⁆ TensorProduct R A B

Two Lie homomorphisms into associative algebras induce a Lie homomorphism from the product of their domains to the tensor product of their codomains, with each image placed in its corresponding tensor factor.

Equations

• f.prodToTensor g = { toLinearMap := (Algebra.TensorProduct.includeLeft.toLinearMap ∘ₗ ↑f).coprod (Algebra.TensorProduct.includeRight.toLinearMap ∘ₗ ↑g), map_lie' := ⋯ }

@[simp]

theorem LieHom.prodToTensor_apply {R : Type u} {L : Type v} {M : Type w} {A : Type x} {B : Type y} [CommRing R] [LieRing L] [LieAlgebra R L] [LieRing M] [LieAlgebra R M] [Ring A] [Algebra R A] [Ring B] [Algebra R B] (f : L →ₗ⁅R⁆ A) (g : M →ₗ⁅R⁆ B) (z : L × M) : (f.prodToTensor g) z = f z.1 ⊗ₜ[R] 1 + 1 ⊗ₜ[R] g z.2

Compute the product-to-tensor Lie homomorphism on a pair: prodToTensor f g (x, y) = f x ⊗ 1 + 1 ⊗ g y.