English
Let R' act on A and on B, and suppose this action is compatible with the R-structure (a tower of scalars). Then any bialgebra homomorphism φ: A →ₐc[R] B is R'-linear; that is, φ(r · x) = r · φ(x) for all r in R' and x in A.
Русский
Пусть R' действует на A и на B и это действие совместимо со структурой над R (существует каскад скаляров). Тогда любой гомоморфизм биалгебр φ: A →ₐc[R] B линейен по R': φ(r · x) = r · φ(x) при любом r ∈ R' и x ∈ A.
LaTeX
$$$\forall r \in R',\ \forall x \in A:\ \varphi(r \cdot x) = r \cdot \varphi(x).$$$
Lean4
theorem map_smul_of_tower {R'} [SMul R' A] [SMul R' B] [LinearMap.CompatibleSMul A B R' R] (r : R') (x : A) :
φ (r • x) = r • φ x :=
φ.toLinearMap.map_smul_of_tower r x
