Tensor products of Lie modules

Tensor products of Lie modules carry natural Lie module structures.

Tags

lie module, tensor product, universal property

noncomputable def TensorProduct.LieModule.hasBracketAux {R : Type u} [CommRing R] {L : Type v} {M : Type w} {N : Type w₁} [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] [AddCommGroup N] [Module R N] [LieRingModule L N] [LieModule R L N] (x : L) : Module.End R (TensorProduct 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 lieRingModule below.

Equations

• TensorProduct.LieModule.hasBracketAux x = LinearMap.rTensor N ((LieModule.toEnd R L M) x) + LinearMap.lTensor M ((LieModule.toEnd R L N) x)

noncomputable instance TensorProduct.LieModule.lieRingModule {R : Type u} [CommRing R] {L : Type v} {M : Type w} {N : Type w₁} [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] [AddCommGroup N] [Module R N] [LieRingModule L N] [LieModule R L N] : LieRingModule L (TensorProduct R M N)

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

Equations

• TensorProduct.LieModule.lieRingModule = LieRingModule.mk ⋯ ⋯ ⋯

noncomputable instance TensorProduct.LieModule.lieModule {R : Type u} [CommRing R] {L : Type v} {M : Type w} {N : Type w₁} [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] [AddCommGroup N] [Module R N] [LieRingModule L N] [LieModule R L N] : LieModule R L (TensorProduct R M N)

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

Equations

• ⋯ = ⋯

@[simp]

theorem TensorProduct.LieModule.lie_tmul_right {R : Type u} [CommRing R] {L : Type v} {M : Type w} {N : Type w₁} [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] [AddCommGroup N] [Module R N] [LieRingModule L N] [LieModule R L N] (x : L) (m : M) (n : N) : ⁅x, m ⊗ₜ[R] n⁆ = ⁅x, m⁆ ⊗ₜ[R] n + m ⊗ₜ[R] ⁅x, n⁆

noncomputable def TensorProduct.LieModule.lift (R : Type u) [CommRing R] (L : Type v) (M : Type w) (N : Type w₁) (P : Type w₂) [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] [AddCommGroup N] [Module R N] [LieRingModule L N] [LieModule R L N] [AddCommGroup P] [Module R P] [LieRingModule L P] [LieModule R L P] : (M →ₗ[R] N →ₗ[R] P) ≃ₗ⁅R,L⁆ TensorProduct R M N →ₗ[R] 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

• TensorProduct.LieModule.lift R L M N P = let __src := TensorProduct.lift.equiv R M N P; { toLinearMap := ↑__src, map_lie' := ⋯, invFun := __src.invFun, left_inv := ⋯, right_inv := ⋯ }

@[simp]

theorem TensorProduct.LieModule.lift_apply (R : Type u) [CommRing R] (L : Type v) (M : Type w) (N : Type w₁) (P : Type w₂) [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] [AddCommGroup N] [Module R N] [LieRingModule L N] [LieModule R L N] [AddCommGroup P] [Module R P] [LieRingModule L P] [LieModule R L P] (f : M →ₗ[R] N →ₗ[R] P) (m : M) (n : N) : ((TensorProduct.LieModule.lift R L M N P) f) (m ⊗ₜ[R] n) = (f m) n

noncomputable def TensorProduct.LieModule.liftLie (R : Type u) [CommRing R] (L : Type v) (M : Type w) (N : Type w₁) (P : Type w₂) [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] [AddCommGroup N] [Module R N] [LieRingModule L N] [LieModule R L N] [AddCommGroup P] [Module R P] [LieRingModule L P] [LieModule R L P] : (M →ₗ⁅R,L⁆ N →ₗ[R] P) ≃ₗ[R] TensorProduct R M N →ₗ⁅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₂).

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TensorProduct.LieModule.coe_liftLie_eq_lift_coe (R : Type u) [CommRing R] (L : Type v) (M : Type w) (N : Type w₁) (P : Type w₂) [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] [AddCommGroup N] [Module R N] [LieRingModule L N] [LieModule R L N] [AddCommGroup P] [Module R P] [LieRingModule L P] [LieModule R L P] (f : M →ₗ⁅R,L⁆ N →ₗ[R] P) : ⇑((TensorProduct.LieModule.liftLie R L M N P) f) = ⇑((TensorProduct.LieModule.lift R L M N P) ↑f)

theorem TensorProduct.LieModule.liftLie_apply (R : Type u) [CommRing R] (L : Type v) (M : Type w) (N : Type w₁) (P : Type w₂) [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] [AddCommGroup N] [Module R N] [LieRingModule L N] [LieModule R L N] [AddCommGroup P] [Module R P] [LieRingModule L P] [LieModule R L P] (f : M →ₗ⁅R,L⁆ N →ₗ[R] P) (m : M) (n : N) : ((TensorProduct.LieModule.liftLie R L M N P) f) (m ⊗ₜ[R] n) = (f m) n

noncomputable def TensorProduct.LieModule.map {R : Type u} [CommRing R] {L : Type v} {M : Type w} {N : Type w₁} {P : Type w₂} {Q : Type w₃} [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] [AddCommGroup N] [Module R N] [LieRingModule L N] [LieModule R L N] [AddCommGroup P] [Module R P] [LieRingModule L P] [LieModule R L P] [AddCommGroup Q] [Module R Q] [LieRingModule L Q] [LieModule R L Q] (f : M →ₗ⁅R,L⁆ P) (g : N →ₗ⁅R,L⁆ Q) : TensorProduct R M N →ₗ⁅R,L⁆ TensorProduct 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

• TensorProduct.LieModule.map f g = let __src := TensorProduct.map ↑f ↑g; { toLinearMap := __src, map_lie' := ⋯ }

@[simp]

theorem TensorProduct.LieModule.coe_linearMap_map {R : Type u} [CommRing R] {L : Type v} {M : Type w} {N : Type w₁} {P : Type w₂} {Q : Type w₃} [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] [AddCommGroup N] [Module R N] [LieRingModule L N] [LieModule R L N] [AddCommGroup P] [Module R P] [LieRingModule L P] [LieModule R L P] [AddCommGroup Q] [Module R Q] [LieRingModule L Q] [LieModule R L Q] (f : M →ₗ⁅R,L⁆ P) (g : N →ₗ⁅R,L⁆ Q) : ↑(TensorProduct.LieModule.map f g) = TensorProduct.map ↑f ↑g

@[simp]

theorem TensorProduct.LieModule.map_tmul {R : Type u} [CommRing R] {L : Type v} {M : Type w} {N : Type w₁} {P : Type w₂} {Q : Type w₃} [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] [AddCommGroup N] [Module R N] [LieRingModule L N] [LieModule R L N] [AddCommGroup P] [Module R P] [LieRingModule L P] [LieModule R L P] [AddCommGroup Q] [Module R Q] [LieRingModule L Q] [LieModule R L Q] (f : M →ₗ⁅R,L⁆ P) (g : N →ₗ⁅R,L⁆ Q) (m : M) (n : N) : (TensorProduct.LieModule.map f g) (m ⊗ₜ[R] n) = f m ⊗ₜ[R] g n

noncomputable def TensorProduct.LieModule.mapIncl {R : Type u} [CommRing R] {L : Type v} {M : Type w} {N : Type w₁} [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] [AddCommGroup N] [Module R N] [LieRingModule L N] [LieModule R L N] (M' : LieSubmodule R L M) (N' : LieSubmodule R L N) : TensorProduct R ↥↑M' ↥↑N' →ₗ⁅R,L⁆ TensorProduct R M N

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

Equations

• TensorProduct.LieModule.mapIncl M' N' = TensorProduct.LieModule.map M'.incl N'.incl

@[simp]

theorem TensorProduct.LieModule.mapIncl_def {R : Type u} [CommRing R] {L : Type v} {M : Type w} {N : Type w₁} [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] [AddCommGroup N] [Module R N] [LieRingModule L N] [LieModule R L N] (M' : LieSubmodule R L M) (N' : LieSubmodule R L N) : TensorProduct.LieModule.mapIncl M' N' = TensorProduct.LieModule.map M'.incl N'.incl

noncomputable def LieModule.toModuleHom (R : Type u) [CommRing R] (L : Type v) (M : Type w) [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] : TensorProduct 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

• LieModule.toModuleHom R L M = (TensorProduct.LieModule.liftLie R L L M M) (let __src := ↑(LieModule.toEnd R L M); { toLinearMap := __src, map_lie' := ⋯ })

@[simp]

theorem LieModule.toModuleHom_apply (R : Type u) [CommRing R] (L : Type v) (M : Type w) [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] (x : L) (m : M) : (LieModule.toModuleHom R L M) (x ⊗ₜ[R] m) = ⁅x, m⁆

theorem LieSubmodule.lieIdeal_oper_eq_tensor_map_range {R : Type u} [CommRing R] {L : Type v} {M : Type w} [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] (I : LieIdeal R L) (N : LieSubmodule R L M) : ⁅I, N⁆ = ((LieModule.toModuleHom R L M).comp (TensorProduct.LieModule.mapIncl 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.