English
There is a correspondence between linear maps and Lie module homomorphisms that respect trivial action on the maximal trivial submodule; one obtains an equivalence between these structures.
Русский
Существует соответствие между линейными отображениями и гомоморфизмами модулей Ли, сохраняющими тривиальное действие на максимальном тривиальном подмодуле; получаем эквивалентность структур.
LaTeX
$$$\\text{maxTrivLinearMapEquivLieModuleHom} : \\maxTrivSubmodule R L (M \\to_{R} N) \\simeq_{\\text{Lie}} M \\to_{L} N$$$
Lean4
/-- `maxTrivSubmodule` is functorial. -/
def maxTrivHom (f : M →ₗ⁅R,L⁆ N) : maxTrivSubmodule R L M →ₗ⁅R,L⁆ maxTrivSubmodule R L N
where
toFun
m :=
⟨f m, fun x =>
(LieModuleHom.map_lie _ _ _).symm.trans <| (congr_arg f (m.property x)).trans (LieModuleHom.map_zero _)⟩
map_add' m n := by ext; simp
map_smul' t m := by ext; simp
map_lie' {x m} := by simp
