restrictScalars_map — Mathlib

English

Restricting scalars commutes with mapping: (M'.map f).restrictScalars R = (M'.restrictScalars R).map (f.restrictScalars R).

Русский

Ограничение скалярных действий коммутирует с отображением: (M'.map f).restrictScalars R = (M'.restrictScalars R).map (f.restrictScalars R).

LaTeX

$$$$ (M'.map f).\mathrm{restrictScalars} R = (M'.\mathrm{restrictScalars} R).map (f.\mathrm{restrictScalars} R) $$$$

Lean4

theorem restrictScalars_map [SMul R R₂] [Module R₂ M] [Module R M₂] [IsScalarTower R R₂ M] [IsScalarTower R R₂ M₂]
    (f : M →ₗ[R₂] M₂) (M' : Submodule R₂ M) :
    (M'.map f).restrictScalars R = (M'.restrictScalars R).map (f.restrictScalars R) :=
  rfl

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