English
Under suitable compatibility hypotheses, one can endow a subtype S (of some ambient object) with a module structure, using scalar action restricted from the ambient setting.
Русский
При заданных совместимостию условиях можно на подтипе S ввести структуру модуля, используя ограниченное от окружения скалярное действие.
LaTeX
$$$ \\text{If } (S,R,A,\\dots) \\text{ satisfy a compatible scalar tower},\\ \\text{then } (S, R, A) \\text{ carries a module structure }$$
Lean4
/-- This can't be an instance because Lean wouldn't know how to find `R`, but we can still use
this to manually derive `Module` on specific types. -/
def toModule' (S R' R A : Type*) [Semiring R] [NonUnitalNonAssocSemiring A] [Module R A] [Semiring R'] [SMul R' R]
[Module R' A] [IsScalarTower R' R A] [SetLike S A] [AddSubmonoidClass S A] [SMulMemClass S R A] (s : S) :
Module R' s :=
haveI : SMulMemClass S R' A := SMulMemClass.ofIsScalarTower S R' R A
SMulMemClass.toModule s
