restrictScalars — Mathlib

English

The map sending a σ-linear map to its AddMonoidHom is injective.

Русский

Отображение, переводящее σ-линейное отображение к AddMonoidHom, инъективно.

LaTeX

$$$ \text{Injective } (\text{toAddMonoidHom} : (M \to_σ M_3) \to M \to_+ M_3) $$$

Lean4

/-- If `M` and `M₂` are both `R`-modules and `S`-modules and `R`-module structures
are defined by an action of `R` on `S` (formally, we have two scalar towers), then any `S`-linear
map from `M` to `M₂` is `R`-linear.

See also `LinearMap.map_smul_of_tower`. -/
@[coe]
def restrictScalars (fₗ : M →ₗ[S] M₂) : M →ₗ[R] M₂ where
  toFun := fₗ
  map_add' := fₗ.map_add
  map_smul' := fₗ.map_smul_of_tower

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