Lean4
/-- Given `F : J ⥤ PresheafOfModules.{v} R`, this is the presheaf of modules obtained by
taking a colimit in the category of modules over `R.obj X` for all `X`. -/
@[simps]
noncomputable def colimitPresheafOfModules : PresheafOfModules R
where
obj X := colimit (F ⋙ evaluation R X)
map {_ Y}
f :=
colimMap (Functor.whiskerLeft F (restriction R f)) ≫
(preservesColimitIso (ModuleCat.restrictScalars (R.map f).hom) (F ⋙ evaluation R Y)).inv
map_id
X :=
colimit.hom_ext
(fun j => by
dsimp
rw [ι_colimMap_assoc, Functor.whiskerLeft_app, restriction_app]
-- Here we should rewrite using `Functor.assoc` but that gives a "motive is type-incorrect"
erw [ι_preservesColimitIso_inv (G := ModuleCat.restrictScalars (R.map (𝟙 X)).hom)]
rw [ModuleCat.restrictScalarsId'App_inv_naturality, map_id]
dsimp)
map_comp {X Y Z} f
g :=
colimit.hom_ext
(fun j => by
dsimp
rw [ι_colimMap_assoc, Functor.whiskerLeft_app, restriction_app, assoc, ι_colimMap_assoc]
-- Here we should rewrite using `Functor.assoc` but that gives a "motive is type-incorrect"
erw [ι_preservesColimitIso_inv (G := ModuleCat.restrictScalars (R.map (f ≫ g)).hom),
ι_preservesColimitIso_inv_assoc (G := ModuleCat.restrictScalars (R.map f).hom)]
rw [← Functor.map_comp_assoc, ι_colimMap_assoc]
erw [ι_preservesColimitIso_inv (G := ModuleCat.restrictScalars (R.map g).hom)]
rw [map_comp, ModuleCat.restrictScalarsComp'_inv_app, assoc, assoc, Functor.whiskerLeft_app,
Functor.whiskerLeft_app, restriction_app, restriction_app]
simp only [Functor.map_comp, assoc]
rfl)
