English
There is a natural distributive action of the group of algebra automorphisms on the units of the algebra: for f ∈ Aut_R(A1) and u ∈ A1^×, the action is given by f • u = Units.map f(u). This endows Units(A1) with a MulDistribMulAction by AlgEquiv R A1 A1.
Русский
Существует естественное распределяемое действие группы алгебраических автоморфизмов на юнитах алгебры: для f ∈ Aut_R(A1) и u ∈ A1^× действие задано f • u = Units.map f(u). Это наделяет группу единиц Units(A1) структурой MulDistribMulAction над AlgEquiv R A1 A1.
LaTeX
$$$ (f\\cdot u) = \\mathrm{Units.map}(f)(u), \\; f\\in \\mathrm{Aut}_R(A_1), \\; u\\in A_1^{\\times},$ and these satisfy the laws of a distributive action: $1\\cdot u = u$, $(uv)\\cdot w = u\\cdot(v\\cdot w)$, and $f\\cdot(u v)=(f\\cdot u)(f\\cdot v)$.$$
Lean4
instance : MulDistribMulAction (A₁ ≃ₐ[R] A₁) A₁ˣ
where
smul := fun f => Units.map f
one_smul := fun x => by ext; rfl
mul_smul := fun x y z => by ext; rfl
smul_mul := fun x y z => by ext; exact map_mul x _ _
smul_one := fun x => by ext; exact map_one x
