# Documentation

Mathlib.Algebra.Lie.TensorProduct

# Tensor products of Lie modules #

Tensor products of Lie modules carry natural Lie module structures.

## Tags #

lie module, tensor product, universal property

def TensorProduct.LieModule.hasBracketAux {R : Type u} [] {L : Type v} {M : Type w} {N : Type w₁} [] [] [] [Module R M] [] [LieModule R L M] [] [Module R N] [] [LieModule R L N] (x : L) :

It is useful to define the bracket via this auxiliary function so that we have a type-theoretic expression of the fact that L acts by linear endomorphisms. It simplifies the proofs in lieRingModule below.

Instances For
instance TensorProduct.LieModule.lieRingModule {R : Type u} [] {L : Type v} {M : Type w} {N : Type w₁} [] [] [] [Module R M] [] [LieModule R L M] [] [Module R N] [] [LieModule R L N] :

The tensor product of two Lie modules is a Lie ring module.

instance TensorProduct.LieModule.lieModule {R : Type u} [] {L : Type v} {M : Type w} {N : Type w₁} [] [] [] [Module R M] [] [LieModule R L M] [] [Module R N] [] [LieModule R L N] :
LieModule R L ()

The tensor product of two Lie modules is a Lie module.

@[simp]
theorem TensorProduct.LieModule.lie_tmul_right {R : Type u} [] {L : Type v} {M : Type w} {N : Type w₁} [] [] [] [Module R M] [] [LieModule R L M] [] [Module R N] [] [LieModule R L N] (x : L) (m : M) (n : N) :
def TensorProduct.LieModule.lift (R : Type u) [] (L : Type v) (M : Type w) (N : Type w₁) (P : Type w₂) [] [] [] [Module R M] [] [LieModule R L M] [] [Module R N] [] [LieModule R L N] [] [Module R P] [] [LieModule R L P] :

The universal property for tensor product of modules of a Lie algebra: the R-linear tensor-hom adjunction is equivariant with respect to the L action.

Instances For
@[simp]
theorem TensorProduct.LieModule.lift_apply (R : Type u) [] (L : Type v) (M : Type w) (N : Type w₁) (P : Type w₂) [] [] [] [Module R M] [] [LieModule R L M] [] [Module R N] [] [LieModule R L N] [] [Module R P] [] [LieModule R L P] (f : M →ₗ[R] N →ₗ[R] P) (m : M) (n : N) :
↑(↑() f) (m ⊗ₜ[R] n) = ↑(f m) n
def TensorProduct.LieModule.liftLie (R : Type u) [] (L : Type v) (M : Type w) (N : Type w₁) (P : Type w₂) [] [] [] [Module R M] [] [LieModule R L M] [] [Module R N] [] [LieModule R L N] [] [Module R P] [] [LieModule R L P] :

A weaker form of the universal property for tensor product of modules of a Lie algebra.

Note that maps f of type M →ₗ⁅R,L⁆ N →ₗ[R] P are exactly those R-bilinear maps satisfying ⁅x, f m n⁆ = f ⁅x, m⁆ n + f m ⁅x, n⁆ for all x, m, n (see e.g, LieModuleHom.map_lie₂).

Instances For
@[simp]
theorem TensorProduct.LieModule.coe_liftLie_eq_lift_coe (R : Type u) [] (L : Type v) (M : Type w) (N : Type w₁) (P : Type w₂) [] [] [] [Module R M] [] [LieModule R L M] [] [Module R N] [] [LieModule R L N] [] [Module R P] [] [LieModule R L P] (f : M →ₗ⁅R,L N →ₗ[R] P) :
↑(↑() f) = ↑(↑() f)
theorem TensorProduct.LieModule.liftLie_apply (R : Type u) [] (L : Type v) (M : Type w) (N : Type w₁) (P : Type w₂) [] [] [] [Module R M] [] [LieModule R L M] [] [Module R N] [] [LieModule R L N] [] [Module R P] [] [LieModule R L P] (f : M →ₗ⁅R,L N →ₗ[R] P) (m : M) (n : N) :
↑(↑() f) (m ⊗ₜ[R] n) = ↑(f m) n
def TensorProduct.LieModule.map {R : Type u} [] {L : Type v} {M : Type w} {N : Type w₁} {P : Type w₂} {Q : Type w₃} [] [] [] [Module R M] [] [LieModule R L M] [] [Module R N] [] [LieModule R L N] [] [Module R P] [] [LieModule R L P] [] [Module R Q] [] [LieModule R L Q] (f : M →ₗ⁅R,L P) (g : N →ₗ⁅R,L Q) :

A pair of Lie module morphisms f : M → P and g : N → Q, induce a Lie module morphism: M ⊗ N → P ⊗ Q.

Instances For
@[simp]
theorem TensorProduct.LieModule.coe_linearMap_map {R : Type u} [] {L : Type v} {M : Type w} {N : Type w₁} {P : Type w₂} {Q : Type w₃} [] [] [] [Module R M] [] [LieModule R L M] [] [Module R N] [] [LieModule R L N] [] [Module R P] [] [LieModule R L P] [] [Module R Q] [] [LieModule R L Q] (f : M →ₗ⁅R,L P) (g : N →ₗ⁅R,L Q) :
↑() =
@[simp]
theorem TensorProduct.LieModule.map_tmul {R : Type u} [] {L : Type v} {M : Type w} {N : Type w₁} {P : Type w₂} {Q : Type w₃} [] [] [] [Module R M] [] [LieModule R L M] [] [Module R N] [] [LieModule R L N] [] [Module R P] [] [LieModule R L P] [] [Module R Q] [] [LieModule R L Q] (f : M →ₗ⁅R,L P) (g : N →ₗ⁅R,L Q) (m : M) (n : N) :
↑() (m ⊗ₜ[R] n) = f m ⊗ₜ[R] g n
def TensorProduct.LieModule.mapIncl {R : Type u} [] {L : Type v} {M : Type w} {N : Type w₁} [] [] [] [Module R M] [] [LieModule R L M] [] [Module R N] [] [LieModule R L N] (M' : LieSubmodule R L M) (N' : LieSubmodule R L N) :
TensorProduct R { x // x M' } { x // x N' } →ₗ⁅R,L

Given Lie submodules M' ⊆ M and N' ⊆ N, this is the natural map: M' ⊗ N' → M ⊗ N.

Instances For
@[simp]
theorem TensorProduct.LieModule.mapIncl_def {R : Type u} [] {L : Type v} {M : Type w} {N : Type w₁} [] [] [] [Module R M] [] [LieModule R L M] [] [Module R N] [] [LieModule R L N] (M' : LieSubmodule R L M) (N' : LieSubmodule R L N) :
def LieModule.toModuleHom (R : Type u) [] (L : Type v) (M : Type w) [] [] [] [Module R M] [] [LieModule R L M] :

The action of the Lie algebra on one of its modules, regarded as a morphism of Lie modules.

Instances For
@[simp]
theorem LieModule.toModuleHom_apply (R : Type u) [] (L : Type v) (M : Type w) [] [] [] [Module R M] [] [LieModule R L M] (x : L) (m : M) :
↑() (x ⊗ₜ[R] m) = x, m
theorem LieSubmodule.lieIdeal_oper_eq_tensor_map_range {R : Type u} [] {L : Type v} {M : Type w} [] [] [] [Module R M] [] [LieModule R L M] (I : LieIdeal R L) (N : LieSubmodule R L M) :

A useful alternative characterisation of Lie ideal operations on Lie submodules.

Given a Lie ideal I ⊆ L and a Lie submodule N ⊆ M, by tensoring the inclusion maps and then applying the action of L on M, we obtain morphism of Lie modules f : I ⊗ N → L ⊗ M → M.

This lemma states that ⁅I, N⁆ = range f.