Limits in categories of presheaves of modules

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

def PresheafOfModules.evaluationJointlyReflectsLimits {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 : Cᵒᵖ), Small.{v, max u₂ v} ↑((F.comp (evaluation R X)).comp (CategoryTheory.forget (ModuleCat ↑(R.obj X)))).sections] (c : CategoryTheory.Limits.Cone F) (hc : (X : Cᵒᵖ) → CategoryTheory.Limits.IsLimit ((evaluation R X).mapCone c)) : CategoryTheory.Limits.IsLimit c

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

instance PresheafOfModules.instHasLimitModuleCatCarrierObjOppositeRingCatCompEvaluationRestrictScalarsHomMap {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 : Cᵒᵖ), Small.{v, max u₂ v} ↑((F.comp (evaluation R X)).comp (CategoryTheory.forget (ModuleCat ↑(R.obj X)))).sections] {X Y : Cᵒᵖ} (f : X ⟶ Y) : CategoryTheory.Limits.HasLimit (F.comp ((evaluation R Y).comp (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f)))))

noncomputable def PresheafOfModules.limitPresheafOfModules {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 : Cᵒᵖ), Small.{v, max u₂ v} ↑((F.comp (evaluation R X)).comp (CategoryTheory.forget (ModuleCat ↑(R.obj X)))).sections] : PresheafOfModules R

Given F : J ⥤ PresheafOfModules.{v} R, this is the presheaf of modules obtained by taking a limit in the category of modules over R.obj X for all X.

@[simp]

theorem PresheafOfModules.limitPresheafOfModules_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 : Cᵒᵖ), Small.{v, max u₂ v} ↑((F.comp (evaluation R X)).comp (CategoryTheory.forget (ModuleCat ↑(R.obj X)))).sections] {x✝ Y : Cᵒᵖ} (f : x✝ ⟶ Y) : (limitPresheafOfModules F).map f = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limMap (F.whiskerLeft (restriction R f))) (CategoryTheory.preservesLimitIso (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))) (F.comp (evaluation R Y))).inv

@[simp]

theorem PresheafOfModules.limitPresheafOfModules_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 : Cᵒᵖ), Small.{v, max u₂ v} ↑((F.comp (evaluation R X)).comp (CategoryTheory.forget (ModuleCat ↑(R.obj X)))).sections] (X : Cᵒᵖ) : (limitPresheafOfModules F).obj X = CategoryTheory.Limits.limit (F.comp (evaluation R X))

noncomputable def PresheafOfModules.limitCone {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 : Cᵒᵖ), Small.{v, max u₂ v} ↑((F.comp (evaluation R X)).comp (CategoryTheory.forget (ModuleCat ↑(R.obj X)))).sections] : CategoryTheory.Limits.Cone F

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

@[simp]

theorem PresheafOfModules.limitCone_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 : Cᵒᵖ), Small.{v, max u₂ v} ↑((F.comp (evaluation R X)).comp (CategoryTheory.forget (ModuleCat ↑(R.obj X)))).sections] : (limitCone F).pt = limitPresheafOfModules F

@[simp]

theorem PresheafOfModules.limitCone_π_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 : Cᵒᵖ), Small.{v, max u₂ v} ↑((F.comp (evaluation R X)).comp (CategoryTheory.forget (ModuleCat ↑(R.obj X)))).sections] (j : J) (X : Cᵒᵖ) : ((limitCone F).π.app j).app X = CategoryTheory.Limits.limit.π (F.comp (evaluation R X)) j

noncomputable def PresheafOfModules.isLimitLimitCone {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 : Cᵒᵖ), Small.{v, max u₂ v} ↑((F.comp (evaluation R X)).comp (CategoryTheory.forget (ModuleCat ↑(R.obj X)))).sections] : CategoryTheory.Limits.IsLimit (limitCone F)

The cone limitCone F is limit for any F : J ⥤ PresheafOfModules.{v} R.

instance PresheafOfModules.hasLimit {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 : Cᵒᵖ), Small.{v, max u₂ v} ↑((F.comp (evaluation R X)).comp (CategoryTheory.forget (ModuleCat ↑(R.obj X)))).sections] : CategoryTheory.Limits.HasLimit F

instance PresheafOfModules.evaluation_preservesLimit {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 : Cᵒᵖ), Small.{v, max u₂ v} ↑((F.comp (evaluation R X)).comp (CategoryTheory.forget (ModuleCat ↑(R.obj X)))).sections] (X : Cᵒᵖ) : CategoryTheory.Limits.PreservesLimit F (evaluation R X)

instance PresheafOfModules.toPresheaf_preservesLimit {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 : Cᵒᵖ), Small.{v, max u₂ v} ↑((F.comp (evaluation R X)).comp (CategoryTheory.forget (ModuleCat ↑(R.obj X)))).sections] : CategoryTheory.Limits.PreservesLimit F (toPresheaf R)

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

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

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

instance PresheafOfModules.toPresheaf_preservesLimitsOfShape {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (R : CategoryTheory.Functor Cᵒᵖ RingCat) (J : Type u₂) [CategoryTheory.Category.{v₂, u₂} J] [Small.{v, u₂} J] : CategoryTheory.Limits.PreservesLimitsOfShape J (toPresheaf R)

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

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

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