Tensor products of Lie modules #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
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) :
module.End R (tensor_product R 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
- tensor_product.lie_module.has_bracket_aux x = linear_map.rtensor N (⇑(lie_module.to_endomorphism R L M) x) + linear_map.ltensor M (⇑(lie_module.to_endomorphism R L N) x)
@[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] :
lie_ring_module L (tensor_product R M N)
The tensor product of two Lie modules is a Lie ring module.
Equations
- tensor_product.lie_module.lie_ring_module = {to_has_bracket := {bracket := λ (x : L), ⇑(tensor_product.lie_module.has_bracket_aux x)}, add_lie := _, lie_add := _, leibniz_lie := _}
@[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] :
lie_module R L (tensor_product R M N)
The tensor product of two Lie modules is a Lie module.
Equations
- tensor_product.lie_module.lie_module = {smul_lie := _, lie_smul := _}
@[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
- tensor_product.lie_module.lift R L M N P = {to_lie_module_hom := {to_linear_map := {to_fun := (tensor_product.lift.equiv R M N P).to_fun, map_add' := _, map_smul' := _}, map_lie' := _}, inv_fun := (tensor_product.lift.equiv R M N P).inv_fun, left_inv := _, right_inv := _}
@[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₂).
@[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) :
⇑(⇑(tensor_product.lie_module.lift_lie R L M N P) f) = ⇑(⇑(tensor_product.lie_module.lift R L M 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]
[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) :
tensor_product R M N →ₗ⁅R,L⁆ tensor_product R P Q
A pair of Lie module morphisms f : M → P and g : N → Q, induce a Lie module morphism:
M ⊗ N → P ⊗ Q.
Equations
- tensor_product.lie_module.map f g = {to_linear_map := {to_fun := (tensor_product.map ↑f ↑g).to_fun, map_add' := _, map_smul' := _}, map_lie' := _}
@[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) :
tensor_product R ↥M' ↥N' →ₗ⁅R,L⁆ tensor_product R M 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] :
tensor_product R L M →ₗ⁅R,L⁆ M
The action of the Lie algebra on one of its modules, regarded as a morphism of Lie modules.
Equations
- lie_module.to_module_hom R L M = ⇑(tensor_product.lie_module.lift_lie R L L M M) {to_linear_map := {to_fun := ↑(lie_module.to_endomorphism R L M).to_fun, map_add' := _, map_smul' := _}, map_lie' := _}
@[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) :
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]
[lie_algebra R L]
[add_comm_group M]
[module R M]
[lie_ring_module L M]
[lie_module R L M]
(I : lie_ideal R L)
(N : lie_submodule R L M) :
⁅I, N⁆ = ((lie_module.to_module_hom R L M).comp (tensor_product.lie_module.map_incl I N)).range
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.