English
Let R be a commutative semiring, A1 an R-algebra, and suppose S acts on R and on A1 in a way compatible with R (IsScalarTower). Then the action of S on the group of R-algebra automorphisms of A1 commutes with the evaluation on elements of A1. In particular, for all s in S, φ in Aut_R(A1), and a in A1, one has s · φ(a) = φ(s · a).
Русский
Пусть R — коммутативное полукольцо, A1 — R-алгебра, и S действует на R и на A1 совместимо с R через IsScalarTower. Тогда действие S на группу R-алгебраических автоморфизмов A1 коммутирует с действиями на элементы A1: для любых s∈S, φ∈Aut_R(A1), a∈A1 выполняется s·φ(a)=φ(s·a).
LaTeX
$$$\\forall s\\in S,\\; \\forall \\phi \\in \\mathrm{Aut}_R(A_1),\\; \\forall a \\in A_1:\\ s \\cdot \\phi(a)=\\phi(s\\cdot a).$$$
Lean4
instance apply_smulCommClass {S} [SMul S R] [SMul S A₁] [IsScalarTower S R A₁] : SMulCommClass S (A₁ ≃ₐ[R] A₁) A₁ where
smul_comm r e a := (e.toLinearEquiv.map_smul_of_tower r a).symm
