restrictScalars — Mathlib

English

Restriction of scalars commutes with the algebra hom structure: the map restricting scalars equals the corresponding restricted map on algebras.

Русский

Ограничение скаляров сохраняет структуру гомоморфизма алгебр: отображение ограничения скаляров равно ограниченному гомоморфизму алгебр.

LaTeX

$$$\text{coe\_restrictScalars} = \text{coe\_restrictScalars}'$$$

Lean4

/-- If `A` is an `R`-algebra, then a continuous `A`-algebra morphism can be interpreted as a
continuous `R`-algebra morphism. -/
def restrictScalars (f : B →A[S] C) : B →A[R] C :=
  ⟨(f : B →ₐ[S] C).restrictScalars R, f.continuous⟩

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