English
Let P be a LieSubmodule of N and f: M →ₗ⁅R,L⁆ N a LieModuleHom. If every f(m) lies in P, then there is a LieModuleHom M →ₗ⁅R,L⁆ P whose underlying map agrees with f on M.
Русский
Пусть P — подмодуля N, и f: M →ₗ⁅R,L⁆ N — гомоморфизм Ли. Если все значения f(m) лежат в P, то существует гомоморфизм M →ₗ⁅R,L⁆ P, чья функция-образ совпадает с f на M.
LaTeX
$$Есть ограничение по коду: существует гомоморфизм в P, если f(m) ∈ P для всех m$$
Lean4
/-- A morphism of Lie modules `f : M → N` whose values lie in a Lie submodule `P ⊆ N` can be
restricted to a morphism of Lie modules `M → P`. -/
def codRestrict (P : LieSubmodule R L N) (f : M →ₗ⁅R,L⁆ N) (h : ∀ m, f m ∈ P) : M →ₗ⁅R,L⁆ P
where
toFun := f.toLinearMap.codRestrict P h
__ := f.toLinearMap.codRestrict P h
map_lie' {x m} := by ext; simp
