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 (PresheafOfModules.evaluation R X)).comp (CategoryTheory.forget (ModuleCat ↑(R.obj X)))).sections] (c : CategoryTheory.Limits.Cone F) (hc : (X : Cᵒᵖ) → CategoryTheory.Limits.IsLimit ((PresheafOfModules.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.

Equations

• One or more equations did not get rendered due to their size.

instance PresheafOfModules.instHasLimitModuleCatαRingObjOppositeRingCatCompEvaluationRestrictScalarsMap {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 (PresheafOfModules.evaluation R X)).comp (CategoryTheory.forget (ModuleCat ↑(R.obj X)))).sections] {X : Cᵒᵖ} {Y : Cᵒᵖ} (f : X ⟶ Y) : CategoryTheory.Limits.HasLimit (F.comp ((PresheafOfModules.evaluation R Y).comp (ModuleCat.restrictScalars (R.map f))))

Equations

• ⋯ = ⋯

@[simp]

theorem PresheafOfModules.limitBundledCore_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 (PresheafOfModules.evaluation R X)).comp (CategoryTheory.forget (ModuleCat ↑(R.obj X)))).sections] {X : Cᵒᵖ} {Y : Cᵒᵖ} (f : X ⟶ Y) : (PresheafOfModules.limitBundledCore F).map f = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limMap (CategoryTheory.whiskerLeft F (PresheafOfModules.restriction R f))) (CategoryTheory.preservesLimitIso (ModuleCat.restrictScalars (R.map f)) (F.comp (PresheafOfModules.evaluation R Y))).inv

@[simp]

theorem PresheafOfModules.limitBundledCore_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 (PresheafOfModules.evaluation R X)).comp (CategoryTheory.forget (ModuleCat ↑(R.obj X)))).sections] (X : Cᵒᵖ) : (PresheafOfModules.limitBundledCore F).obj X = CategoryTheory.Limits.limit (F.comp (PresheafOfModules.evaluation R X))

noncomputable def PresheafOfModules.limitBundledCore {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 (PresheafOfModules.evaluation R X)).comp (CategoryTheory.forget (ModuleCat ↑(R.obj X)))).sections] : BundledCorePresheafOfModules R

Given F : J ⥤ PresheafOfModules.{v} R, this is the BundledCorePresheafOfModules R which corresponds to the presheaf of modules which sends X to the limit of F ⋙ evaluation R X.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def PresheafOfModules.limitConeπ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 (PresheafOfModules.evaluation R X)).comp (CategoryTheory.forget (ModuleCat ↑(R.obj X)))).sections] (j : J) : (PresheafOfModules.limitBundledCore F).toPresheafOfModules ⟶ F.obj j

Given F : J ⥤ PresheafOfModules.{v} R, this is the canonical map (limitBundledCore F).toPresheafOfModules ⟶ F.obj j for all j : J.

Equations

• PresheafOfModules.limitConeπApp F j = PresheafOfModules.Hom.mk'' (fun (X : Cᵒᵖ) => CategoryTheory.Limits.limit.π (F.comp (PresheafOfModules.evaluation R X)) j) ⋯

@[simp]

theorem PresheafOfModules.limitConeπApp_naturality_assoc {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 (PresheafOfModules.evaluation R X)).comp (CategoryTheory.forget (ModuleCat ↑(R.obj X)))).sections] {i : J} {j : J} (f : i ⟶ j) {Z : PresheafOfModules R} (h : F.obj j ⟶ Z) : CategoryTheory.CategoryStruct.comp (PresheafOfModules.limitConeπApp F i) (CategoryTheory.CategoryStruct.comp (F.map f) h) = CategoryTheory.CategoryStruct.comp (PresheafOfModules.limitConeπApp F j) h

@[simp]

theorem PresheafOfModules.limitConeπApp_naturality {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 (PresheafOfModules.evaluation R X)).comp (CategoryTheory.forget (ModuleCat ↑(R.obj X)))).sections] {i : J} {j : J} (f : i ⟶ j) : CategoryTheory.CategoryStruct.comp (PresheafOfModules.limitConeπApp F i) (F.map f) = PresheafOfModules.limitConeπApp F j

@[simp]

theorem PresheafOfModules.limitCone_π_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 (PresheafOfModules.evaluation R X)).comp (CategoryTheory.forget (ModuleCat ↑(R.obj X)))).sections] (j : J) : (PresheafOfModules.limitCone F).π.app j = PresheafOfModules.limitConeπApp F j

@[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 (PresheafOfModules.evaluation R X)).comp (CategoryTheory.forget (ModuleCat ↑(R.obj X)))).sections] : (PresheafOfModules.limitCone F).pt = (PresheafOfModules.limitBundledCore F).toPresheafOfModules

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 (PresheafOfModules.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 for the limit of F ⋙ evaluation R X for all X.

Equations

• PresheafOfModules.limitCone F = { pt := (PresheafOfModules.limitBundledCore F).toPresheafOfModules, π := { app := PresheafOfModules.limitConeπApp F, naturality := ⋯ } }

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 (PresheafOfModules.evaluation R X)).comp (CategoryTheory.forget (ModuleCat ↑(R.obj X)))).sections] : CategoryTheory.Limits.IsLimit (PresheafOfModules.limitCone F)

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

Equations

• One or more equations did not get rendered due to their size.

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 (PresheafOfModules.evaluation R X)).comp (CategoryTheory.forget (ModuleCat ↑(R.obj X)))).sections] : CategoryTheory.Limits.HasLimit F

Equations

• ⋯ = ⋯

noncomputable instance PresheafOfModules.evaluationPreservesLimit {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 (PresheafOfModules.evaluation R X)).comp (CategoryTheory.forget (ModuleCat ↑(R.obj X)))).sections] (X : Cᵒᵖ) : CategoryTheory.Limits.PreservesLimit F (PresheafOfModules.evaluation R X)

Equations

• One or more equations did not get rendered due to their size.

noncomputable instance PresheafOfModules.toPresheafPreservesLimit {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 (PresheafOfModules.evaluation R X)).comp (CategoryTheory.forget (ModuleCat ↑(R.obj X)))).sections] : CategoryTheory.Limits.PreservesLimit F (PresheafOfModules.toPresheaf R)

Equations

• One or more equations did not get rendered due to their size.

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)

Equations

• ⋯ = ⋯

noncomputable instance PresheafOfModules.evaluationPreservesLimitsOfShape {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 (PresheafOfModules.evaluation R X)

Equations

• PresheafOfModules.evaluationPreservesLimitsOfShape R J X = { preservesLimit := fun {K : CategoryTheory.Functor J (PresheafOfModules R)} => inferInstance }

noncomputable instance PresheafOfModules.toPresheafPreservesLimitsOfShape {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 (PresheafOfModules.toPresheaf R)

Equations

• PresheafOfModules.toPresheafPreservesLimitsOfShape R J = { preservesLimit := fun {K : CategoryTheory.Functor J (PresheafOfModules R)} => inferInstance }

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

Equations

• ⋯ = ⋯

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

Equations

• PresheafOfModules.Finite.evaluationPreservesFiniteLimits R X = { preservesFiniteLimits := inferInstance }

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

Equations

• PresheafOfModules.Finite.toPresheafPreservesFiniteLimits R = { preservesFiniteLimits := inferInstance }