mathlib documentation

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] [lie_algebra R L] [add_comm_group M] [module R M] [lie_ring_module L M] [lie_module R L M] [add_comm_group N] [module R N] [lie_ring_module L N] [lie_module 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 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] [lie_algebra R L] [add_comm_group M] [module R M] [lie_ring_module L M] [lie_module R L M] [add_comm_group N] [module R N] [lie_ring_module L N] [lie_module R L 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] [lie_algebra R L] [add_comm_group M] [module R M] [lie_ring_module L M] [lie_module R L M] [add_comm_group N] [module R N] [lie_ring_module L N] [lie_module R L 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] [lie_algebra R L] [add_comm_group M] [module R M] [lie_ring_module L M] [lie_module R L M] [add_comm_group N] [module R N] [lie_ring_module L N] [lie_module R 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] [lie_algebra R L] [add_comm_group M] [module R M] [lie_ring_module L M] [lie_module R L M] [add_comm_group N] [module R N] [lie_ring_module L N] [lie_module R L N] [add_comm_group P] [module R P] [lie_ring_module L P] [lie_module 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.

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] [lie_algebra R L] [add_comm_group M] [module R M] [lie_ring_module L M] [lie_module R L M] [add_comm_group N] [module R N] [lie_ring_module L N] [lie_module R L N] [add_comm_group P] [module R P] [lie_ring_module L P] [lie_module R L P] (f : M →ₗ[R] N →ₗ[R] P) (m : M) (n : 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] [lie_algebra R L] [add_comm_group M] [module R M] [lie_ring_module L M] [lie_module R L M] [add_comm_group N] [module R N] [lie_ring_module L N] [lie_module R L N] [add_comm_group P] [module R P] [lie_ring_module L P] [lie_module 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, 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] [lie_algebra R L] [add_comm_group M] [module R M] [lie_ring_module L M] [lie_module R L M] [add_comm_group N] [module R N] [lie_ring_module L N] [lie_module R L N] [add_comm_group P] [module R P] [lie_ring_module L P] [lie_module R L P] (f : M →ₗ⁅R,L N →ₗ[R] P) :
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] [lie_algebra R L] [add_comm_group M] [module R M] [lie_ring_module L M] [lie_module R L M] [add_comm_group N] [module R N] [lie_ring_module L N] [lie_module R L N] [add_comm_group P] [module R P] [lie_ring_module L P] [lie_module R L P] (f : M →ₗ⁅R,L N →ₗ[R] P) (m : M) (n : 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] [lie_algebra R L] [add_comm_group M] [module R M] [lie_ring_module L M] [lie_module R L M] [add_comm_group N] [module R N] [lie_ring_module L N] [lie_module R L N] [add_comm_group P] [module R P] [lie_ring_module L P] [lie_module R L P] [add_comm_group Q] [module R Q] [lie_ring_module L Q] [lie_module 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.

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] [lie_algebra R L] [add_comm_group M] [module R M] [lie_ring_module L M] [lie_module R L M] [add_comm_group N] [module R N] [lie_ring_module L N] [lie_module R L N] [add_comm_group P] [module R P] [lie_ring_module L P] [lie_module R L P] [add_comm_group Q] [module R Q] [lie_ring_module L Q] [lie_module R 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] [lie_algebra R L] [add_comm_group M] [module R M] [lie_ring_module L M] [lie_module R L M] [add_comm_group N] [module R N] [lie_ring_module L N] [lie_module R L N] [add_comm_group P] [module R P] [lie_ring_module L P] [lie_module R L P] [add_comm_group Q] [module R Q] [lie_ring_module L Q] [lie_module R L Q] (f : M →ₗ⁅R,L P) (g : N →ₗ⁅R,L Q) (m : M) (n : 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] [lie_algebra R L] [add_comm_group M] [module R M] [lie_ring_module L M] [lie_module R L M] [add_comm_group N] [module R N] [lie_ring_module L N] [lie_module R L N] (M' : lie_submodule R L M) (N' : lie_submodule R L 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] [lie_algebra R L] [add_comm_group M] [module R M] [lie_ring_module L M] [lie_module R L M] [add_comm_group N] [module R N] [lie_ring_module L N] [lie_module R L N] (M' : lie_submodule R L M) (N' : lie_submodule R L N) :
def lie_module.to_module_hom (R : Type u) [comm_ring R] (L : Type v) (M : Type w) [lie_ring L] [lie_algebra R L] [add_comm_group M] [module R M] [lie_ring_module L M] [lie_module R 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] [lie_algebra R L] [add_comm_group M] [module R M] [lie_ring_module L M] [lie_module R L M] (x : L) (m : 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.