English
If g is injective, and the Lie module on L₂,M₂ is nilpotent, then the preimage module (L,M) is nilpotent.
Русский
Если g инъективно, и модуля на L₂,M₂ нильпотентны, то предобразный модуль (L,M) нильпотентен.
LaTeX
$$theorem lieModuleIsNilpotent (with injective g) : IsNilpotent L M$$
Lean4
theorem lieModule_isNilpotent_iff (f : L ≃ₗ⁅R⁆ L₂) (g : M ≃ₗ[R] M₂) (hfg : ∀ x m, ⁅f x, g m⁆ = g ⁅x, m⁆) :
IsNilpotent L M ↔ IsNilpotent L₂ M₂ := by
constructor <;> intro h
· have hg : Surjective (g : M →ₗ[R] M₂) := g.surjective
exact f.surjective.lieModuleIsNilpotent hfg hg
· have hg : Surjective (g.symm : M₂ →ₗ[R] M) := g.symm.surjective
refine f.symm.surjective.lieModuleIsNilpotent (fun x m => ?_) hg
rw [LinearEquiv.coe_coe, LieEquiv.coe_toLieHom, ← g.symm_apply_apply ⁅f.symm x, g.symm m⁆, ← hfg,
f.apply_symm_apply, g.apply_symm_apply]
