instIsFaithfulSubtypeMemLieSubalgebra

English

If M is a faithful Lie module over a Lie algebra L over a commutative ring R, then the restriction of the action to any Lie subalgebra L' of L is faithful on M as well.

Русский

Если M является верной модулем Ли над Ли-алгеброй L над R, тогда ограничение действия до любой подалгебры L' ⊆ L также верно на M.

LaTeX

$$$\forall x \in L',\; (\forall m \in M,[x,m]=0) \Rightarrow x=0,$ where $L'$ is a Lie subalgebra of $L$ and the action is given by $x\cdot m=[x,m]$.$$

Lean4

instance [IsFaithful R L M] {L' : LieSubalgebra R L} : IsFaithful R L' M :=
  by
  refine ⟨(?_ : Injective (toEnd R L M ∘ ((↑) : L' → L)))⟩
  exact IsFaithful.injective_toEnd.comp Subtype.val_injective

Похожие утверждения