instSMulHom — Mathlib

English

For any chain complexes X, Y over a semiring R, the morphisms X ⟶ Y form an R-module with scalar action defined componentwise by (r • f).f_n = r • f.f_n.

Русский

Для комплексов Х, Y над полем/кольцом R множество гомоморфизмов X → Y образует модуль над R, где скалярное умножение задано по компонентам: (r • f).f_n = r • f_n.

LaTeX

$$$\\forall r\\in R\\, \\forall f\\colon X \\to Y\\, \\forall n, \\ (r\\cdot f).f_n = r\\cdot f.f_n$$$

Lean4

instance : SMul R (X ⟶ Y) where smul r f := { f := fun n => r • f.f n }

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