English
For any subalgebra S of A, and any α with a compatible A-action (MulActionWithZero structure), α carries a natural S-action obtained by restricting the A-action along the inclusion S → A. Concretely, for s in S and x in α, the S-action is given by s • x = (s in A) • x.
Русский
Для любой подалгебры S внутри A и любого модуля α с действием A (структура MulActionWithZero), α естественным образом становится модулем над S, получаемым ограничением действия A по вложению S → A. То есть для s ∈ S и x ∈ α имеем s • x = (s в A) • x.
LaTeX
$$$\forall (S : \text{Subalgebra } R A) (\alpha) [Zero \alpha] [MulActionWithZero A \alpha] (s : S) (x : \alpha), s \cdot x = ((s : A) \cdot x)$$$
Lean4
/-- The action by a subalgebra is the action by the underlying algebra. -/
instance [Zero α] [MulActionWithZero A α] (S : Subalgebra R A) : MulActionWithZero S α :=
inferInstanceAs (MulActionWithZero S.toSubsemiring α)
