English
If f: L → L2 is surjective and L is Engelian, then L2 is Engelian.
Русский
Если отображение f слугущее и L является Engelian, то L2 тоже Engelian.
LaTeX
$$isEngelian {f : L →ₗ⁅R⁆ L2} (hf : Function.Surjective f) (h : LieAlgebra.IsEngelian R L) : LieAlgebra.IsEngelian R L2$$
Lean4
theorem isEngelian {f : L →ₗ⁅R⁆ L₂} (hf : Function.Surjective f) (h : LieAlgebra.IsEngelian.{u₁, u₂, u₄} R L) :
LieAlgebra.IsEngelian.{u₁, u₃, u₄} R L₂ :=
by
intro M _i1 _i2 _i3 _i4 h'
letI : LieRingModule L M := LieRingModule.compLieHom M f
letI : LieModule R L M := compLieHom M f
have hnp : ∀ x, IsNilpotent (toEnd R L M x) := fun x => h' (f x)
have surj_id : Function.Surjective (LinearMap.id : M →ₗ[R] M) := Function.surjective_id
haveI : LieModule.IsNilpotent L M := h M hnp
apply hf.lieModuleIsNilpotent _ surj_id
aesop
