restrictScalars — Mathlib

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) }

Похожие утверждения