English
Given a Lie ring L2 acting on a module M, the pullback of this action along a Lie algebra homomorphism f: L1 → L2 makes M into a Lie module over L1.
Русский
Заданное действие Ли-кольца L2 на модуль M можно вытянуть по линейному гомоморфизму f: L1 → L2, чтобы M стало модулем Ли над L1.
LaTeX
$$$ M \text{ becomes a Lie } L_1\text{-module with action } x \cdot m = f(x) \cdot m, $$$
Lean4
/-- A Lie module may be pulled back along a morphism of Lie algebras. -/
theorem compLieHom [Module R M] [LieModule R L₂ M] : @LieModule R L₁ M _ _ _ _ _ (LieRingModule.compLieHom M f) :=
{ __ := LieRingModule.compLieHom M f
smul_lie := fun t x m => by simp only [LieRingModule.compLieHom_apply, smul_lie, LieHom.map_smul]
lie_smul := fun t x m => by simp only [LieRingModule.compLieHom_apply, lie_smul] }
