# mathlibdocumentation

algebra.lie.tensor_product

# Tensor products of Lie modules #

Tensor products of Lie modules carry natural Lie module structures.

## Tags #

lie module, tensor product, universal property

def tensor_product.lie_module.has_bracket_aux {R : Type u} [comm_ring R] {L : Type v} {M : Type w} {N : Type w₁} [lie_ring L] [ L] [ M] [ M] [ L M] [ N] [ N] [ L N] (x : L) :
M N)

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

Equations
@[protected, instance]
def tensor_product.lie_module.lie_ring_module {R : Type u} [comm_ring R] {L : Type v} {M : Type w} {N : Type w₁} [lie_ring L] [ L] [ M] [ M] [ L M] [ N] [ N] [ L N] :
M N)

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

Equations
@[protected, instance]
def tensor_product.lie_module.lie_module {R : Type u} [comm_ring R] {L : Type v} {M : Type w} {N : Type w₁} [lie_ring L] [ L] [ M] [ M] [ L M] [ N] [ N] [ L N] :
L M N)

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

Equations
@[simp]
theorem tensor_product.lie_module.lie_tmul_right {R : Type u} [comm_ring R] {L : Type v} {M : Type w} {N : Type w₁} [lie_ring L] [ L] [ M] [ M] [ L M] [ N] [ N] [ L N] (x : L) (m : M) (n : N) :
def tensor_product.lie_module.lift (R : Type u) [comm_ring R] (L : Type v) (M : Type w) (N : Type w₁) (P : Type w₂) [lie_ring L] [ L] [ M] [ M] [ L M] [ N] [ N] [ L N] [ P] [ P] [ 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.

Equations
@[simp]
theorem tensor_product.lie_module.lift_apply (R : Type u) [comm_ring R] (L : Type v) (M : Type w) (N : Type w₁) (P : Type w₂) [lie_ring L] [ L] [ M] [ M] [ L M] [ N] [ N] [ L N] [ P] [ P] [ L P] (f : M →ₗ[R] N →ₗ[R] P) (m : M) (n : N) :
( N P) f) (m ⊗ₜ[R] n) = (f m) n
def tensor_product.lie_module.lift_lie (R : Type u) [comm_ring R] (L : Type v) (M : Type w) (N : Type w₁) (P : Type w₂) [lie_ring L] [ L] [ M] [ M] [ L M] [ N] [ N] [ L N] [ P] [ P] [ 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, lie_module_hom.map_lie₂).

Equations
@[simp]
theorem tensor_product.lie_module.coe_lift_lie_eq_lift_coe (R : Type u) [comm_ring R] (L : Type v) (M : Type w) (N : Type w₁) (P : Type w₂) [lie_ring L] [ L] [ M] [ M] [ L M] [ N] [ N] [ L N] [ P] [ P] [ L P] (f : M →ₗ⁅R,L N →ₗ[R] P) :
( P) f) = ( N P) f)
theorem tensor_product.lie_module.lift_lie_apply (R : Type u) [comm_ring R] (L : Type v) (M : Type w) (N : Type w₁) (P : Type w₂) [lie_ring L] [ L] [ M] [ M] [ L M] [ N] [ N] [ L N] [ P] [ P] [ L P] (f : M →ₗ⁅R,L N →ₗ[R] P) (m : M) (n : N) :
( P) f) (m ⊗ₜ[R] n) = (f m) n
def tensor_product.lie_module.map {R : Type u} [comm_ring R] {L : Type v} {M : Type w} {N : Type w₁} {P : Type w₂} {Q : Type w₃} [lie_ring L] [ L] [ M] [ M] [ L M] [ N] [ N] [ L N] [ P] [ P] [ L P] [ Q] [ Q] [ 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.

Equations
@[simp]
theorem tensor_product.lie_module.coe_linear_map_map {R : Type u} [comm_ring R] {L : Type v} {M : Type w} {N : Type w₁} {P : Type w₂} {Q : Type w₃} [lie_ring L] [ L] [ M] [ M] [ L M] [ N] [ N] [ L N] [ P] [ P] [ L P] [ Q] [ Q] [ L Q] (f : M →ₗ⁅R,L P) (g : N →ₗ⁅R,L Q) :
@[simp]
theorem tensor_product.lie_module.map_tmul {R : Type u} [comm_ring R] {L : Type v} {M : Type w} {N : Type w₁} {P : Type w₂} {Q : Type w₃} [lie_ring L] [ L] [ M] [ M] [ L M] [ N] [ N] [ L N] [ P] [ P] [ L P] [ Q] [ Q] [ 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 tensor_product.lie_module.map_incl {R : Type u} [comm_ring R] {L : Type v} {M : Type w} {N : Type w₁} [lie_ring L] [ L] [ M] [ M] [ L M] [ N] [ N] [ L N] (M' : M) (N' : N) :

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

Equations
@[simp]
theorem tensor_product.lie_module.map_incl_def {R : Type u} [comm_ring R] {L : Type v} {M : Type w} {N : Type w₁} [lie_ring L] [ L] [ M] [ M] [ L M] [ N] [ N] [ L N] (M' : M) (N' : N) :
def lie_module.to_module_hom (R : Type u) [comm_ring R] (L : Type v) (M : Type w) [lie_ring L] [ L] [ M] [ M] [ L M] :

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

Equations
@[simp]
theorem lie_module.to_module_hom_apply (R : Type u) [comm_ring R] (L : Type v) (M : Type w) [lie_ring L] [ L] [ M] [ M] [ L M] (x : L) (m : M) :
M) (x ⊗ₜ[R] m) = x,m
theorem lie_submodule.lie_ideal_oper_eq_tensor_map_range {R : Type u} [comm_ring R] {L : Type v} {M : Type w} [lie_ring L] [ L] [ M] [ M] [ L M] (I : L) (N : 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.