English
If M acts on N and N acts on α with a scalar tower structure, and all components have continuous SMul, then M acts continuously on α.
Русский
Если M действует на N, N на α и есть структура IsScalarTower, и все смулы непрерывны, то M действует непрерывно на α.
LaTeX
$$$\\text{IsScalarTower } M N α\\;\\Rightarrow\\; \\text{ContinuousSMul } M α$$$
Lean4
/-- If a scalar action is central, then its right action is continuous when its left action is. -/
@[to_additive /-- If an additive action is central, then its right action is continuous when its
left action is. -/
]
instance op [SMul Mᵐᵒᵖ X] [IsCentralScalar M X] : ContinuousSMul Mᵐᵒᵖ X :=
⟨by
suffices Continuous fun p : M × X => MulOpposite.op p.fst • p.snd from
this.comp (MulOpposite.continuous_unop.prodMap continuous_id)
simpa only [op_smul_eq_smul] using (continuous_smul : Continuous fun p : M × X => _)⟩
