LieSubmodule.lieIdeal_oper_eq_tensor_map_range

theorem LieSubmodule.lieIdeal_oper_eq_tensor_map_range : ∀ {R : Type u} [inst : CommRing R] {L : Type v} {M : Type w} [inst_1 : LieRing L] [inst_2 : LieAlgebra R L] [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : LieRingModule L M] [inst_6 : 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

This theorem provides an alternative way to characterize the operations of Lie ideals on Lie submodules in the context of Lie algebras. Suppose we have a Lie ideal `I` which is a subset of `L` and a Lie submodule `N` which is a subset of `M`. By tensoring the inclusion maps and then applying the action of `L` on `M`, we obtain a morphism of Lie modules `f` from `I ⊗ N` to `L ⊗ M` to `M`. This theorem states that the Lie bracket operation `⁅I, N⁆` results in the range of the morphism `f`. In more mathematical terms, we have `⁅I, N⁆ = range f`. Here, `f` is constructed by composing the `LieModule.toModuleHom` function (which converts a given Lie module to a module homomorphism) with the `TensorProduct.LieModule.mapIncl` function that maps inclusions into the respective tensor product of the Lie modules.

More concisely: The theorem asserts that the Lie bracket of a Lie ideal and a Lie submodule equals the image of the morphism obtained by tensoring and applying the Lie module action to their inclusion maps.