English
An injective Lie-module hom f yields a LieModuleEquiv between a submodule N and its image N.map f.
Русский
Инъективный гомоморфизм Ли-модулей f задаёт эквивалентность Ли-модуля между N и его образом N.map f.
LaTeX
$$$ N \simeq_{R,L} N.map f $$$
Lean4
/-- For an injective morphism of Lie modules, any Lie submodule is equivalent to its image. -/
noncomputable def equivMapOfInjective (hf : Function.Injective f) : N ≃ₗ⁅R,L⁆ N.map f :=
{ Submodule.equivMapOfInjective (f : M →ₗ[R] M') hf N with
-- Note: https://github.com/leanprover-community/mathlib4/pull/8386 had to specify `invFun` explicitly this way, otherwise we'd get a type mismatch
invFun := by exact DFunLike.coe (Submodule.equivMapOfInjective (f : M →ₗ[R] M') hf N).symm
map_lie' := by rintro x ⟨m, hm : m ∈ N⟩; ext; exact f.map_lie x m }
