restrictScalarsₗ — Mathlib

English

There is a canonical linear map RestrictScalars_R sending an S-linear map f: M →ₗ[S] N to its R-restriction f|_R: M →ₗ[R] N; this map preserves addition and R-scalar multiplication.

Русский

Существует каноническое линейное отображение RestrictScalars_R, отправляющее S-линейное отображение f: M →ₗ[S] N в его ограничение f|_R: M →ₗ[R] N; это отображение линейно по R.

LaTeX

$$$ \text{restrictScalars}_R: \mathrm{Hom}_S(M,N) \to \mathrm{Hom}_R(M,N), \quad f \mapsto f|_R $$$

Lean4

/-- `LinearMap.restrictScalars` as a `LinearMap`. -/
@[simps apply]
def restrictScalarsₗ : (M →ₗ[S] N) →ₗ[R₁] M →ₗ[R] N
    where
  toFun := restrictScalars R
  map_add' := restrictScalars_add
  map_smul' := restrictScalars_smul

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