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 ((PresheafOfModules.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.

Equations

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

instance PresheafOfModules.instHasColimitModuleCatα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 Y : Cᵒᵖ} → (f : X ⟶ Y) → CategoryTheory.Limits.PreservesColimit (F.comp (PresheafOfModules.evaluation R Y)) (ModuleCat.restrictScalars (R.map f))] [∀ (X : Cᵒᵖ), CategoryTheory.Limits.HasColimit (F.comp (PresheafOfModules.evaluation R X))] {X : Cᵒᵖ} {Y : Cᵒᵖ} (f : X ⟶ Y) : CategoryTheory.Limits.HasColimit (F.comp ((PresheafOfModules.evaluation R Y).comp (ModuleCat.restrictScalars (R.map f))))

Equations

• ⋯ = ⋯

@[simp]

theorem PresheafOfModules.colimitBundledCore_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 (PresheafOfModules.evaluation R Y)) (ModuleCat.restrictScalars (R.map f))] [∀ (X : Cᵒᵖ), CategoryTheory.Limits.HasColimit (F.comp (PresheafOfModules.evaluation R X))] {X : Cᵒᵖ} {Y : Cᵒᵖ} (f : X ⟶ Y) : (PresheafOfModules.colimitBundledCore F).map f = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimMap (CategoryTheory.whiskerLeft F (PresheafOfModules.restriction R f))) (CategoryTheory.preservesColimitIso (ModuleCat.restrictScalars (R.map f)) (F.comp (PresheafOfModules.evaluation R Y))).inv

@[simp]

theorem PresheafOfModules.colimitBundledCore_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 (PresheafOfModules.evaluation R Y)) (ModuleCat.restrictScalars (R.map f))] [∀ (X : Cᵒᵖ), CategoryTheory.Limits.HasColimit (F.comp (PresheafOfModules.evaluation R X))] (X : Cᵒᵖ) : (PresheafOfModules.colimitBundledCore F).obj X = CategoryTheory.Limits.colimit (F.comp (PresheafOfModules.evaluation R X))

noncomputable def PresheafOfModules.colimitBundledCore {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 (PresheafOfModules.evaluation R Y)) (ModuleCat.restrictScalars (R.map f))] [∀ (X : Cᵒᵖ), CategoryTheory.Limits.HasColimit (F.comp (PresheafOfModules.evaluation R X))] : 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 colimit of F ⋙ evaluation R X.

Equations

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

noncomputable def PresheafOfModules.colimitCoconeι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 (PresheafOfModules.evaluation R Y)) (ModuleCat.restrictScalars (R.map f))] [∀ (X : Cᵒᵖ), CategoryTheory.Limits.HasColimit (F.comp (PresheafOfModules.evaluation R X))] (j : J) : F.obj j ⟶ (PresheafOfModules.colimitBundledCore F).toPresheafOfModules

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

Equations

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

@[simp]

theorem PresheafOfModules.colimitCoconeι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 Y : Cᵒᵖ} → (f : X ⟶ Y) → CategoryTheory.Limits.PreservesColimit (F.comp (PresheafOfModules.evaluation R Y)) (ModuleCat.restrictScalars (R.map f))] [∀ (X : Cᵒᵖ), CategoryTheory.Limits.HasColimit (F.comp (PresheafOfModules.evaluation R X))] {i : J} {j : J} (f : i ⟶ j) {Z : PresheafOfModules R} (h : (PresheafOfModules.colimitBundledCore F).toPresheafOfModules ⟶ Z) : CategoryTheory.CategoryStruct.comp (F.map f) (CategoryTheory.CategoryStruct.comp (PresheafOfModules.colimitCoconeιApp F j) h) = CategoryTheory.CategoryStruct.comp (PresheafOfModules.colimitCoconeιApp F i) h

@[simp]

theorem PresheafOfModules.colimitCoconeι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 Y : Cᵒᵖ} → (f : X ⟶ Y) → CategoryTheory.Limits.PreservesColimit (F.comp (PresheafOfModules.evaluation R Y)) (ModuleCat.restrictScalars (R.map f))] [∀ (X : Cᵒᵖ), CategoryTheory.Limits.HasColimit (F.comp (PresheafOfModules.evaluation R X))] {i : J} {j : J} (f : i ⟶ j) : CategoryTheory.CategoryStruct.comp (F.map f) (PresheafOfModules.colimitCoconeιApp F j) = PresheafOfModules.colimitCoconeιApp F i

@[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 (PresheafOfModules.evaluation R Y)) (ModuleCat.restrictScalars (R.map f))] [∀ (X : Cᵒᵖ), CategoryTheory.Limits.HasColimit (F.comp (PresheafOfModules.evaluation R X))] : (PresheafOfModules.colimitCocone F).pt = (PresheafOfModules.colimitBundledCore F).toPresheafOfModules

@[simp]

theorem PresheafOfModules.colimitCocone_ι_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 (PresheafOfModules.evaluation R Y)) (ModuleCat.restrictScalars (R.map f))] [∀ (X : Cᵒᵖ), CategoryTheory.Limits.HasColimit (F.comp (PresheafOfModules.evaluation R X))] (j : J) : (PresheafOfModules.colimitCocone F).ι.app j = PresheafOfModules.colimitCoconeιApp F j

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 (PresheafOfModules.evaluation R Y)) (ModuleCat.restrictScalars (R.map f))] [∀ (X : Cᵒᵖ), CategoryTheory.Limits.HasColimit (F.comp (PresheafOfModules.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.

Equations

• PresheafOfModules.colimitCocone F = { pt := (PresheafOfModules.colimitBundledCore F).toPresheafOfModules, ι := { app := PresheafOfModules.colimitCoconeιApp F, naturality := ⋯ } }

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 (PresheafOfModules.evaluation R Y)) (ModuleCat.restrictScalars (R.map f))] [∀ (X : Cᵒᵖ), CategoryTheory.Limits.HasColimit (F.comp (PresheafOfModules.evaluation R X))] : CategoryTheory.Limits.IsColimit (PresheafOfModules.colimitCocone F)

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

Equations

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

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 (PresheafOfModules.evaluation R Y)) (ModuleCat.restrictScalars (R.map f))] [∀ (X : Cᵒᵖ), CategoryTheory.Limits.HasColimit (F.comp (PresheafOfModules.evaluation R X))] : CategoryTheory.Limits.HasColimit F

Equations

• ⋯ = ⋯

noncomputable instance PresheafOfModules.evaluationPreservesColimit {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 (PresheafOfModules.evaluation R Y)) (ModuleCat.restrictScalars (R.map f))] [∀ (X : Cᵒᵖ), CategoryTheory.Limits.HasColimit (F.comp (PresheafOfModules.evaluation R X))] (X : Cᵒᵖ) : CategoryTheory.Limits.PreservesColimit F (PresheafOfModules.evaluation R X)

Equations

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

noncomputable instance PresheafOfModules.toPresheafPreservesColimit {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 (PresheafOfModules.evaluation R Y)) (ModuleCat.restrictScalars (R.map f))] [∀ (X : Cᵒᵖ), CategoryTheory.Limits.HasColimit (F.comp (PresheafOfModules.evaluation R X))] [(X : Cᵒᵖ) → CategoryTheory.Limits.PreservesColimit F ((PresheafOfModules.evaluation R X).comp (CategoryTheory.forget₂ (ModuleCat ↑(R.obj X)) AddCommGrp))] : CategoryTheory.Limits.PreservesColimit F (PresheafOfModules.toPresheaf R)

Equations

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

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 AddCommGrp] : CategoryTheory.Limits.HasColimitsOfShape J (PresheafOfModules R)

Equations

• ⋯ = ⋯

noncomputable instance PresheafOfModules.evaluationPreservesColimitsOfShape {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 AddCommGrp] (X : Cᵒᵖ) : CategoryTheory.Limits.PreservesColimitsOfShape J (PresheafOfModules.evaluation R X)

Equations

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

noncomputable instance PresheafOfModules.toPresheafPreservesColimitsOfShape {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 AddCommGrp] : CategoryTheory.Limits.PreservesColimitsOfShape J (PresheafOfModules.toPresheaf R)

Equations

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

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

Equations

• ⋯ = ⋯

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

Equations

• PresheafOfModules.Finite.evaluationPreservesFiniteColimits R X = { preservesFiniteColimits := inferInstance }

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

Equations

• PresheafOfModules.Finite.toPresheafPreservesFiniteColimits R = { preservesFiniteColimits := inferInstance }