Colimits in categories of presheaves of modules

In this file, it is shown that under suitable assumptions, colimits exist in the category PresheafOfModules R.

def PresheafOfModules.evaluationJointlyReflectsColimits {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat} {J : Type u₂} [CategoryTheory.Category.{v₂, u₂} J] (F : CategoryTheory.Functor J (PresheafOfModules R)) (c : CategoryTheory.Limits.Cocone F) (hc : (X : Cᵒᵖ) → CategoryTheory.Limits.IsColimit ((evaluation R X).mapCocone c)) : CategoryTheory.Limits.IsColimit c

A cocone in the category PresheafOfModules R is colimit if it is so after the application of the functors evaluation R X for all X.

instance PresheafOfModules.instHasColimitModuleCatCarrierObjOppositeRingCatCompEvaluationRestrictScalarsHomMap {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat} {J : Type u₂} [CategoryTheory.Category.{v₂, u₂} J] (F : CategoryTheory.Functor J (PresheafOfModules R)) [∀ {X Y : Cᵒᵖ} (f : X ⟶ Y), CategoryTheory.Limits.PreservesColimit (F.comp (evaluation R Y)) (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f)))] [∀ (X : Cᵒᵖ), CategoryTheory.Limits.HasColimit (F.comp (evaluation R X))] {X Y : Cᵒᵖ} (f : X ⟶ Y) : CategoryTheory.Limits.HasColimit (F.comp ((evaluation R Y).comp (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f)))))

noncomputable def PresheafOfModules.colimitPresheafOfModules {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat} {J : Type u₂} [CategoryTheory.Category.{v₂, u₂} J] (F : CategoryTheory.Functor J (PresheafOfModules R)) [∀ {X Y : Cᵒᵖ} (f : X ⟶ Y), CategoryTheory.Limits.PreservesColimit (F.comp (evaluation R Y)) (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f)))] [∀ (X : Cᵒᵖ), CategoryTheory.Limits.HasColimit (F.comp (evaluation R X))] : PresheafOfModules R

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.

@[simp]

theorem PresheafOfModules.colimitPresheafOfModules_obj {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat} {J : Type u₂} [CategoryTheory.Category.{v₂, u₂} J] (F : CategoryTheory.Functor J (PresheafOfModules R)) [∀ {X Y : Cᵒᵖ} (f : X ⟶ Y), CategoryTheory.Limits.PreservesColimit (F.comp (evaluation R Y)) (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f)))] [∀ (X : Cᵒᵖ), CategoryTheory.Limits.HasColimit (F.comp (evaluation R X))] (X : Cᵒᵖ) : (colimitPresheafOfModules F).obj X = CategoryTheory.Limits.colimit (F.comp (evaluation R X))

@[simp]

theorem PresheafOfModules.colimitPresheafOfModules_map {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat} {J : Type u₂} [CategoryTheory.Category.{v₂, u₂} J] (F : CategoryTheory.Functor J (PresheafOfModules R)) [∀ {X Y : Cᵒᵖ} (f : X ⟶ Y), CategoryTheory.Limits.PreservesColimit (F.comp (evaluation R Y)) (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f)))] [∀ (X : Cᵒᵖ), CategoryTheory.Limits.HasColimit (F.comp (evaluation R X))] {x✝ Y : Cᵒᵖ} (f : x✝ ⟶ Y) : (colimitPresheafOfModules F).map f = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimMap (F.whiskerLeft (restriction R f))) (CategoryTheory.preservesColimitIso (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))) (F.comp (evaluation R Y))).inv

noncomputable def PresheafOfModules.colimitCocone {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat} {J : Type u₂} [CategoryTheory.Category.{v₂, u₂} J] (F : CategoryTheory.Functor J (PresheafOfModules R)) [∀ {X Y : Cᵒᵖ} (f : X ⟶ Y), CategoryTheory.Limits.PreservesColimit (F.comp (evaluation R Y)) (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f)))] [∀ (X : Cᵒᵖ), CategoryTheory.Limits.HasColimit (F.comp (evaluation R X))] : CategoryTheory.Limits.Cocone F

The (colimit) cocone for F : J ⥤ PresheafOfModules.{v} R that is constructed from the colimit of F ⋙ evaluation R X for all X.

@[simp]

theorem PresheafOfModules.colimitCocone_pt {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat} {J : Type u₂} [CategoryTheory.Category.{v₂, u₂} J] (F : CategoryTheory.Functor J (PresheafOfModules R)) [∀ {X Y : Cᵒᵖ} (f : X ⟶ Y), CategoryTheory.Limits.PreservesColimit (F.comp (evaluation R Y)) (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f)))] [∀ (X : Cᵒᵖ), CategoryTheory.Limits.HasColimit (F.comp (evaluation R X))] : (colimitCocone F).pt = colimitPresheafOfModules F

@[simp]

theorem PresheafOfModules.colimitCocone_ι_app_app {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat} {J : Type u₂} [CategoryTheory.Category.{v₂, u₂} J] (F : CategoryTheory.Functor J (PresheafOfModules R)) [∀ {X Y : Cᵒᵖ} (f : X ⟶ Y), CategoryTheory.Limits.PreservesColimit (F.comp (evaluation R Y)) (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f)))] [∀ (X : Cᵒᵖ), CategoryTheory.Limits.HasColimit (F.comp (evaluation R X))] (j : J) (X : Cᵒᵖ) : ((colimitCocone F).ι.app j).app X = CategoryTheory.Limits.colimit.ι (F.comp (evaluation R X)) j

noncomputable def PresheafOfModules.isColimitColimitCocone {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat} {J : Type u₂} [CategoryTheory.Category.{v₂, u₂} J] (F : CategoryTheory.Functor J (PresheafOfModules R)) [∀ {X Y : Cᵒᵖ} (f : X ⟶ Y), CategoryTheory.Limits.PreservesColimit (F.comp (evaluation R Y)) (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f)))] [∀ (X : Cᵒᵖ), CategoryTheory.Limits.HasColimit (F.comp (evaluation R X))] : CategoryTheory.Limits.IsColimit (colimitCocone F)

The cocone colimitCocone F is colimit for any F : J ⥤ PresheafOfModules.{v} R.

instance PresheafOfModules.hasColimit {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat} {J : Type u₂} [CategoryTheory.Category.{v₂, u₂} J] (F : CategoryTheory.Functor J (PresheafOfModules R)) [∀ {X Y : Cᵒᵖ} (f : X ⟶ Y), CategoryTheory.Limits.PreservesColimit (F.comp (evaluation R Y)) (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f)))] [∀ (X : Cᵒᵖ), CategoryTheory.Limits.HasColimit (F.comp (evaluation R X))] : CategoryTheory.Limits.HasColimit F

instance PresheafOfModules.evaluation_preservesColimit {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat} {J : Type u₂} [CategoryTheory.Category.{v₂, u₂} J] (F : CategoryTheory.Functor J (PresheafOfModules R)) [∀ {X Y : Cᵒᵖ} (f : X ⟶ Y), CategoryTheory.Limits.PreservesColimit (F.comp (evaluation R Y)) (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f)))] [∀ (X : Cᵒᵖ), CategoryTheory.Limits.HasColimit (F.comp (evaluation R X))] (X : Cᵒᵖ) : CategoryTheory.Limits.PreservesColimit F (evaluation R X)

instance PresheafOfModules.toPresheaf_preservesColimit {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat} {J : Type u₂} [CategoryTheory.Category.{v₂, u₂} J] (F : CategoryTheory.Functor J (PresheafOfModules R)) [∀ {X Y : Cᵒᵖ} (f : X ⟶ Y), CategoryTheory.Limits.PreservesColimit (F.comp (evaluation R Y)) (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f)))] [∀ (X : Cᵒᵖ), CategoryTheory.Limits.HasColimit (F.comp (evaluation R X))] [∀ (X : Cᵒᵖ), CategoryTheory.Limits.PreservesColimit F ((evaluation R X).comp (CategoryTheory.forget₂ (ModuleCat ↑(R.obj X)) AddCommGrpCat))] : CategoryTheory.Limits.PreservesColimit F (toPresheaf R)

instance PresheafOfModules.hasColimitsOfShape {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (R : CategoryTheory.Functor Cᵒᵖ RingCat) (J : Type u₂) [CategoryTheory.Category.{v₂, u₂} J] [CategoryTheory.Limits.HasColimitsOfShape J AddCommGrpCat] : CategoryTheory.Limits.HasColimitsOfShape J (PresheafOfModules R)

instance PresheafOfModules.evaluation_preservesColimitsOfShape {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (R : CategoryTheory.Functor Cᵒᵖ RingCat) (J : Type u₂) [CategoryTheory.Category.{v₂, u₂} J] [CategoryTheory.Limits.HasColimitsOfShape J AddCommGrpCat] (X : Cᵒᵖ) : CategoryTheory.Limits.PreservesColimitsOfShape J (evaluation R X)

instance PresheafOfModules.toPresheaf_preservesColimitsOfShape {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (R : CategoryTheory.Functor Cᵒᵖ RingCat) (J : Type u₂) [CategoryTheory.Category.{v₂, u₂} J] [CategoryTheory.Limits.HasColimitsOfShape J AddCommGrpCat] : CategoryTheory.Limits.PreservesColimitsOfShape J (toPresheaf R)

instance PresheafOfModules.Finite.hasFiniteColimits {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (R : CategoryTheory.Functor Cᵒᵖ RingCat) : CategoryTheory.Limits.HasFiniteColimits (PresheafOfModules R)

instance PresheafOfModules.Finite.evaluation_preservesFiniteColimits {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (R : CategoryTheory.Functor Cᵒᵖ RingCat) (X : Cᵒᵖ) : CategoryTheory.Limits.PreservesFiniteColimits (evaluation R X)

instance PresheafOfModules.Finite.toPresheaf_preservesFiniteColimits {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (R : CategoryTheory.Functor Cᵒᵖ RingCat) : CategoryTheory.Limits.PreservesFiniteColimits (toPresheaf R)

instance PresheafOfModules.hasColimitsOfSize {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (R : CategoryTheory.Functor Cᵒᵖ RingCat) [CategoryTheory.Limits.HasColimitsOfSize.{v₂, u₂, v, v + 1} AddCommGrpCat] : CategoryTheory.Limits.HasColimitsOfSize.{v₂, u₂, max u₁ v, max (max (max (v + 1) u) u₁) v₁} (PresheafOfModules R)

instance PresheafOfModules.evaluation_preservesColimitsOfSize {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (R : CategoryTheory.Functor Cᵒᵖ RingCat) [CategoryTheory.Limits.HasColimitsOfSize.{v₂, u₂, v, v + 1} AddCommGrpCat] (X : Cᵒᵖ) : CategoryTheory.Limits.PreservesColimitsOfSize.{v₂, u₂, max u₁ v, v, max (max (max u u₁) (v + 1)) v₁, max u (v + 1)} (evaluation R X)

instance PresheafOfModules.toPresheaf_preservesColimitsOfSize {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (R : CategoryTheory.Functor Cᵒᵖ RingCat) [CategoryTheory.Limits.HasColimitsOfSize.{v₂, u₂, v, v + 1} AddCommGrpCat] : CategoryTheory.Limits.PreservesColimitsOfSize.{v₂, u₂, max u₁ v, max u₁ v, max (max (max u u₁) (v + 1)) v₁, max (max u₁ (v + 1)) v₁} (toPresheaf R)