English
Let F: C ⥤ D be a functor between preadditive categories endowed with an R-linear structure. For any objects X and Y in C, there is an R-linear map mapLinearMap_{X,Y}: Hom_C(X,Y) → Hom_D(FX,FY) whose underlying function is F.map; in particular, mapLinearMap_{X,Y}(f) = F.map(f).
Русский
Пусть F: C ⥤ D — функтор между преддобавительными категориями, на который задан R-линейный структурный объект. Для любых объектов X,Y в C существует R-линейное отображение mapLinearMap_{X,Y}: Hom_C(X,Y) → Hom_D(FX,FY), чья обобщенная функция равна F.map; в частности, mapLinearMap_{X,Y}(f) = F.map(f).
LaTeX
$$$\\forall X,Y\\,\\forall f:\\,\\mathrm{Hom}_C(X,Y):\\ (F.mapLinearMap\\,R)\\,f = F.map\\,f\\\\[R\\text{-linearity}].$$$
Lean4
/-- `F.mapLinearMap` is an `R`-linear map whose underlying function is `F.map`. -/
@[simps]
def mapLinearMap {X Y : C} : (X ⟶ Y) →ₗ[R] F.obj X ⟶ F.obj Y :=
{ F.mapAddHom with map_smul' := fun r f => F.map_smul r f }
