English
Given a LieModuleHom f : M → M' and a LieSubmodule N of M, the forward image N.map f is a LieSubmodule of M' generated by {f(m) : m ∈ N}.
Русский
Пусть f: M → M' — гомоморфизм модулей Ли и N — LieSubmodule M. Тогда образ N по f является LieSubmodule M', порождаемым всеми изображениями элементов N через f.
LaTeX
$$N.map f = { m' ∈ M' : ∃ m ∈ N, m' = f(m) } as a LieSubmodule$$
Lean4
/-- A morphism of Lie modules `f : M → M'` pushes forward Lie submodules of `M` to Lie submodules
of `M'`. -/
def map : LieSubmodule R L M' :=
{ (N : Submodule R M).map (f : M →ₗ[R] M') with
lie_mem := fun {x m'} h ↦ by
rcases h with ⟨m, hm, hfm⟩; use ⁅x, m⁆; constructor
· apply N.lie_mem hm
· norm_cast at hfm; simp [hfm] }
