English
The restriction of scalars construction is equipped with an R-algebra structure, i.e., there is an R-algebra on RestrictScalars R S A built from the R-algebra maps via composition with the S-algebra map to A.
Русский
У конструкции ограничение скаляров имеется структура R-алгебры: на RestrictScalars R S A задана алгебраическая структура над R, получаемая путем композиции алгебраических отображений.
LaTeX
$$$\text{Algebra}_R(\mathrm{RestrictScalars}(R,S,A))$$$
Lean4
/-- `R ⟶ S` induces `S-Alg ⥤ R-Alg` -/
instance algebra : Algebra R (RestrictScalars R S A)
where
algebraMap := (algebraMap S A).comp (algebraMap R S)
smul := (· • ·)
commutes' := fun _ _ ↦ Algebra.commutes' (A := A) _ _
smul_def' := fun _ _ ↦ Algebra.smul_def' (A := A) _ _
