Lean4
/-- A morphism of Lie algebras `f : L → L'` pulls back Lie ideals of `L'` to Lie ideals of `L`.
Note that `f` makes `L'` into a Lie module over `L` (turning `f` into a morphism of Lie modules)
and so this is a special case of `LieSubmodule.comap` but we do not exploit this fact. -/
def comap : LieIdeal R L :=
{ (J : Submodule R L').comap (f : L →ₗ[R] L') with
lie_mem := fun {x y} h ↦
by
suffices ⁅f x, f y⁆ ∈ J
by
simp only [AddSubsemigroup.mem_carrier, AddSubmonoid.mem_toSubsemigroup, Submodule.mem_toAddSubmonoid,
Submodule.mem_comap, LieHom.coe_toLinearMap, LieHom.map_lie, LieSubalgebra.mem_toSubmodule]
exact this
apply J.lie_mem h }
