English
Let Y be acted upon by X and X be acted upon by M′ in a compatible way (a scalar tower). Then any map f: X → Y that preserves the X-action is automatically M′-equivariant as well.
Русский
Пусть Y есть действие со стороны X, а X — со стороны M′, совместимо (скалярная башня). Тогда любая функция f: X → Y, сохраняющая действие X, автоматически сохраняет и действие M′.
LaTeX
$$$\forall f:\,X\to Y,\; (\forall x\in X, f(x_0\cdot x)=x_0\cdot f(x)\text{ для всех } x_0\in X) \Rightarrow (\forall m\in M', \forall x\in X, f(m\cdot x)=m\cdot f(x)).$$$
Lean4
/-- If Y/X/M forms a scalar tower, any map X → Y preserving X-action also preserves M-action. -/
@[to_additive]
theorem _root_.IsScalarTower.smulHomClass [MulOneClass X] [SMul X Y] [IsScalarTower M' X Y]
[MulActionHomClass F X X Y] : MulActionHomClass F M' X Y where
map_smulₛₗ f m
x := by rw [← mul_one (m • x), ← smul_eq_mul, map_smul, smul_assoc, ← map_smul, smul_eq_mul, mul_one, id_eq]
