English
For a map f: A →ₐ[S] B, restrictScalars(R) sends f to an R-algebra map A → B by forgetting the S-structure,
while preserving the underlying ring map.
Русский
Для отображения f: A →ₐ[S] B ограничение по R отправляет f в R-гомоморфизм A → B, забывая структуру S.
LaTeX
$$$ restrictScalars\ R: (A \to_{{S}} B) \to (A \to_{{R}} B)$$$
Lean4
/-- R ⟶ S induces S-Alg ⥤ R-Alg -/
def restrictScalars (f : A →ₐ[S] B) : A →ₐ[R] B :=
{ (f : A →+* B) with
commutes' := fun r => by
rw [algebraMap_apply R S A, algebraMap_apply R S B]
exact f.commutes (algebraMap R S r) }