smul_naturality — Mathlib

English

Morphisms preserve scalar multiplication, i.e., applying a morphism commutes with the scalar action on modules.

Русский

Гомоморфизмы сохраняют скалярное умножение: применение гомоморфизма commute с действием скаляра на модулях.

LaTeX

$$$(\mathrm{forget})\_map f \circ (N.\mathrm{smul} \; r) = (M.\mathrm{smul} \; r) \circ (\mathrm{forget})\_map f$$$

Lean4

theorem smul_naturality {M N : ModuleCat.{v} R} (f : M ⟶ N) (r : R) :
    (forget₂ (ModuleCat R) AddCommGrpCat).map f ≫ N.smul r = M.smul r ≫ (forget₂ (ModuleCat R) AddCommGrpCat).map f :=
  by
  ext x
  exact (f.hom.map_smul r x).symm

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