English
For a LieHom f: L → L' and a LieIdeal I ⊆ L, if the carrier of map f I is exactly f(I), then the corresponding LieSubmodule toSubmodule coincides with the image of I under f.
Русский
Пусть f: L → L' — гомоморфизм Ли и I ⊆ L — Ли-идеал. Если носитель (carrier) подмодуля map f I равен изображению f(I), то соответствующий подмодуль Lie совпадает с изображением I под действием f.
LaTeX
$$$ (\\uparrow (\\mathrm{map}\\ f I) = f '' I) \\Rightarrow \\mathrm{LieSubmodule}.toSubmodule(\\mathrm{map}\n f I) = (\\mathrm{LieSubmodule}.toSubmodule I).map(f) $$$
Lean4
@[simp]
theorem map_toSubmodule (h : ↑(map f I) = f '' I) :
LieSubmodule.toSubmodule (map f I) = (LieSubmodule.toSubmodule I).map (f : L →ₗ[R] L') := by
rw [SetLike.ext'_iff, LieSubmodule.coe_toSubmodule, h, Submodule.map_coe]; rfl
