English
Re-statement: mapIncl M' N' equals map M'.incl N'.incl, confirming the natural tensor inclusion construction.
Русский
Повторение: mapIncl M' N' = map M'.incl N'.incl, что подтверждает естественную конструцию включения тензора.
LaTeX
$$$$\mathrm{mapIncl}(M',N') = \mathrm{map}(M'.\mathrm{incl},N'.\mathrm{incl}).$$$$
Lean4
/-- 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`. -/
theorem lieIdeal_oper_eq_tensor_map_range :
⁅I, N⁆ = ((toModuleHom R L M).comp (mapIncl I N : I ⊗[R] N →ₗ⁅R,L⁆ L ⊗[R] M)).range :=
by
rw [← toSubmodule_inj, lieIdeal_oper_eq_linear_span, LieModuleHom.toSubmodule_range, LieModuleHom.toLinearMap_comp,
LinearMap.range_comp, mapIncl_def, toLinearMap_map, TensorProduct.range_map_eq_span_tmul, Submodule.map_span]
congr; ext m; constructor
· rintro ⟨⟨x, hx⟩, ⟨n, hn⟩, rfl⟩; use x ⊗ₜ n; constructor
· use ⟨x, hx⟩, ⟨n, hn⟩; rfl
· simp
· rintro ⟨t, ⟨⟨x, hx⟩, ⟨n, hn⟩, rfl⟩, h⟩; rw [← h]; use ⟨x, hx⟩, ⟨n, hn⟩; rfl
