English
If f is surjective, the underlying submodule of I.map f equals the image of I under f as a submodule.
Русский
Если f сюръективен, подмодуль-образ I.map f совпадает с образом подмодуля I под действием f.
LaTeX
$$$\operatorname{toSubmodule}(I.map f) = \operatorname{toSubmodule}(I) \mapsto f$$$
Lean4
theorem coe_map_of_surjective (h : Function.Surjective f) :
LieSubmodule.toSubmodule (I.map f) = (LieSubmodule.toSubmodule I).map (f : L →ₗ[R] L') :=
by
let J : LieIdeal R L' :=
{ (I : Submodule R L).map (f : L →ₗ[R] L') with
lie_mem := fun {x y} hy ↦ by
have hy' : ∃ x : L, x ∈ I ∧ f x = y := by simpa [hy]
obtain ⟨z₂, hz₂, rfl⟩ := hy'
obtain ⟨z₁, rfl⟩ := h x
simp only [LieHom.coe_toLinearMap, SetLike.mem_coe, Set.mem_image, Submodule.mem_carrier, Submodule.map_coe]
use ⁅z₁, z₂⁆
exact ⟨I.lie_mem hz₂, f.map_lie z₁ z₂⟩ }
rw [map, toLieSubalgebra_toSubmodule, LieSubmodule.coe_lieSpan_submodule_eq_iff]
exact ⟨J, rfl⟩
