Limits in categories of sheaves of modules

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

TODO

• do the same for colimits (which requires constructing the associated sheaf of modules functor)

theorem PresheafOfModules.isSheaf_of_isLimit {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {R : CategoryTheory.Functor Cᵒᵖ RingCat} {F : CategoryTheory.Functor D (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} [CategoryTheory.Limits.HasLimitsOfShape D AddCommGrp] (hc : CategoryTheory.Limits.IsLimit c) (hF : ∀ (j : D), CategoryTheory.Presheaf.IsSheaf J (F.obj j).presheaf) : CategoryTheory.Presheaf.IsSheaf J c.pt.presheaf

instance SheafOfModules.instSmallElemForallObjCompModuleCatαRingOppositeRingCatValPresheafOfModulesForgetEvaluationForgetSections {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {R : CategoryTheory.Sheaf J RingCat} (F : CategoryTheory.Functor D (SheafOfModules R)) [∀ (X : Cᵒᵖ), Small.{v, max u₂ v} ↑((F.comp (SheafOfModules.evaluation R X)).comp (CategoryTheory.forget (ModuleCat ↑(R.val.obj X)))).sections] (X : Cᵒᵖ) : Small.{v, max u₂ v} ↑(((F.comp (SheafOfModules.forget R)).comp (PresheafOfModules.evaluation R.val X)).comp (CategoryTheory.forget (ModuleCat ↑(R.val.obj X)))).sections

Equations

• ⋯ = ⋯

noncomputable instance SheafOfModules.createsLimit {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {R : CategoryTheory.Sheaf J RingCat} (F : CategoryTheory.Functor D (SheafOfModules R)) [∀ (X : Cᵒᵖ), Small.{v, max u₂ v} ↑((F.comp (SheafOfModules.evaluation R X)).comp (CategoryTheory.forget (ModuleCat ↑(R.val.obj X)))).sections] [CategoryTheory.Limits.HasLimitsOfShape D AddCommGrp] : CategoryTheory.CreatesLimit F (SheafOfModules.forget R)

Equations

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

instance SheafOfModules.hasLimit {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {R : CategoryTheory.Sheaf J RingCat} (F : CategoryTheory.Functor D (SheafOfModules R)) [∀ (X : Cᵒᵖ), Small.{v, max u₂ v} ↑((F.comp (SheafOfModules.evaluation R X)).comp (CategoryTheory.forget (ModuleCat ↑(R.val.obj X)))).sections] [CategoryTheory.Limits.HasLimitsOfShape D AddCommGrp] : CategoryTheory.Limits.HasLimit F

Equations

• ⋯ = ⋯

noncomputable instance SheafOfModules.evaluationPreservesLimit {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {R : CategoryTheory.Sheaf J RingCat} (F : CategoryTheory.Functor D (SheafOfModules R)) [∀ (X : Cᵒᵖ), Small.{v, max u₂ v} ↑((F.comp (SheafOfModules.evaluation R X)).comp (CategoryTheory.forget (ModuleCat ↑(R.val.obj X)))).sections] [CategoryTheory.Limits.HasLimitsOfShape D AddCommGrp] (X : Cᵒᵖ) : CategoryTheory.Limits.PreservesLimit F (SheafOfModules.evaluation R X)

Equations

• SheafOfModules.evaluationPreservesLimit F X = id inferInstance

instance SheafOfModules.hasLimitsOfShape {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} (D : Type u₂) [CategoryTheory.Category.{v₂, u₂} D] (R : CategoryTheory.Sheaf J RingCat) [Small.{v, u₂} D] : CategoryTheory.Limits.HasLimitsOfShape D (SheafOfModules R)

Equations

• ⋯ = ⋯

noncomputable instance SheafOfModules.evaluationPreservesLimitsOfShape {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} (D : Type u₂) [CategoryTheory.Category.{v₂, u₂} D] (R : CategoryTheory.Sheaf J RingCat) [Small.{v, u₂} D] (X : Cᵒᵖ) : CategoryTheory.Limits.PreservesLimitsOfShape D (SheafOfModules.evaluation R X)

Equations

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

noncomputable instance SheafOfModules.forgetPreservesLimitsOfShape {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} (D : Type u₂) [CategoryTheory.Category.{v₂, u₂} D] (R : CategoryTheory.Sheaf J RingCat) [Small.{v, u₂} D] : CategoryTheory.Limits.PreservesLimitsOfShape D (SheafOfModules.forget R)

Equations

• SheafOfModules.forgetPreservesLimitsOfShape D R = { preservesLimit := fun {K : CategoryTheory.Functor D (SheafOfModules R)} => inferInstance }

instance SheafOfModules.Finite.hasFiniteLimits {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} (R : CategoryTheory.Sheaf J RingCat) : CategoryTheory.Limits.HasFiniteLimits (SheafOfModules R)

Equations

• ⋯ = ⋯

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

Equations

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

noncomputable instance SheafOfModules.Finite.forgetPreservesFiniteLimits {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} (R : CategoryTheory.Sheaf J RingCat) : CategoryTheory.Limits.PreservesFiniteLimits (SheafOfModules.forget R)

Equations

• SheafOfModules.Finite.forgetPreservesFiniteLimits R = { preservesFiniteLimits := inferInstance }

instance SheafOfModules.hasLimitsOfSize {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} (R : CategoryTheory.Sheaf J RingCat) : CategoryTheory.Limits.HasLimitsOfSize.{v₂, v, max u₁ v, max (max (max (v + 1) u) u₁) v₁} (SheafOfModules R)

Equations

• ⋯ = ⋯

noncomputable instance SheafOfModules.evaluationPreservesLimitsOfSize {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} (R : CategoryTheory.Sheaf J RingCat) (X : Cᵒᵖ) : CategoryTheory.Limits.PreservesLimitsOfSize.{v₂, v, max u₁ v, v, max (max (max u u₁) (v + 1)) v₁, max u (v + 1)} (SheafOfModules.evaluation R X)

Equations

• SheafOfModules.evaluationPreservesLimitsOfSize R X = { preservesLimitsOfShape := fun {J_1 : Type ?u.48} [CategoryTheory.Category.{?u.46, ?u.48} J_1] => inferInstance }

noncomputable instance SheafOfModules.forgetPreservesLimitsOfSize {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} (R : CategoryTheory.Sheaf J RingCat) : CategoryTheory.Limits.PreservesLimitsOfSize.{v₂, v, max u₁ v, max u₁ v, max (max (max u u₁) (v + 1)) v₁, max (max (max u u₁) (v + 1)) v₁} (SheafOfModules.forget R)

Equations

• SheafOfModules.forgetPreservesLimitsOfSize R = { preservesLimitsOfShape := fun {J_1 : Type ?u.42} [CategoryTheory.Category.{?u.40, ?u.42} J_1] => inferInstance }

noncomputable instance SheafOfModules.instPreservesFiniteLimitsFunctorOppositeAddCommGrpCompSheafToSheafSheafToPresheaf {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} (R : CategoryTheory.Sheaf J RingCat) : CategoryTheory.Limits.PreservesFiniteLimits ((SheafOfModules.toSheaf R).comp (CategoryTheory.sheafToPresheaf J AddCommGrp))

Equations

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

noncomputable instance SheafOfModules.instPreservesFiniteLimitsSheafAddCommGrpToSheaf {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} (R : CategoryTheory.Sheaf J RingCat) : CategoryTheory.Limits.PreservesFiniteLimits (SheafOfModules.toSheaf R)

Equations

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