English
For a diagram F: J → PresheafOfModules(R) and for any morphism f: X → Y, the colimit of the diagram obtained by evaluating at Y and restricting scalars along R.map f exists; this computes the colimit objectwise after restriction.
Русский
Для диаграммы F: J → PresheafOfModules(R) и для любого morphism f: X → Y существует предел по colimit диаграмме, полученной после вычисления в Y и ограничения по скалярам через R.map f; предел вычисляется по точкам отдельно после ограничения.
LaTeX
$$$HasColimit\\left(F \\;\\circ\\; (\\mathrm{evaluation}\\; R\\; Y) \\;\\circ\\; (\\mathrm{ModuleCat}.restrictScalars(\\mathrm{RingCat}.Hom.hom (R.map f)))\\right)$$$
Lean4
instance {X Y : Cᵒᵖ} (f : X ⟶ Y) : HasColimit (F ⋙ evaluation R Y ⋙ (ModuleCat.restrictScalars (R.map f).hom)) :=
⟨_, isColimitOfPreserves (ModuleCat.restrictScalars (R.map f).hom) (colimit.isColimit (F ⋙ evaluation R Y))⟩
