English
A LieModuleHom f: M → L N induces a LieModuleHom between maxTrivSubmodule R L M and maxTrivSubmodule R L N, sending each element to its image under f while preserving the Lie-module structure.
Русский
Ли-гомоморфизм f: M → N индуцирует гомоморфизм между maxTrivSubmodule R L M и maxTrivSubmodule R L N, переводя каждый элемент в образ через f и сохраняя структуру модуля Ли.
LaTeX
$$$\\text{maxTrivHom } f : \\maxTrivSubmodule R L M \\to_{\\text{Lie}} \\maxTrivSubmodule R L N$$$
Lean4
/-- The maximal trivial submodules of Lie-equivalent Lie modules are Lie-equivalent. -/
def maxTrivEquiv (e : M ≃ₗ⁅R,L⁆ N) : maxTrivSubmodule R L M ≃ₗ⁅R,L⁆ maxTrivSubmodule R L N :=
{ maxTrivHom (e : M →ₗ⁅R,L⁆ N) with
toFun := maxTrivHom (e : M →ₗ⁅R,L⁆ N)
invFun := maxTrivHom (e.symm : N →ₗ⁅R,L⁆ M)
left_inv := fun m => by ext; simp
right_inv := fun n => by ext; simp }
