English
Let R be a commutative ring. If D is a preadditive category and F: C → D is a functor, then the lifted functor lift_R(F) is additive; equivalently, it preserves addition of morphisms: for all morphisms f,g, (lift_R(F))(f+g) = (lift_R(F))(f) + (lift_R(F))(g).
Русский
Пусть R — коммутативное кольцо. Если D — предадитивная категория и F: C → D — функтор, то полученный подъем lift_R(F) является аддитивным; то есть он сохраняет сумму морфизмов: для любых f,g имеем (lift_R(F))(f+g) = (lift_R(F))(f) + (lift_R(F))(g).
LaTeX
$$$ \\forall f,g:\\; \\text{Hom}(X,Y) ,\\; (\\mathrm{Lift}_R(F))(f+g) = (\\mathrm{Lift}_R(F))(f) + (\\mathrm{Lift}_R(F))(g).$$$
Lean4
instance lift_additive (F : C ⥤ D) : (lift R F).Additive where
map_add {X Y} f
g := by
dsimp
rw [Finsupp.sum_add_index'] <;> simp [add_smul]
