Colimits in categories of extensive sheaves #
This file proves that J-shaped colimits of A-valued sheaves for the extensive topology are
computed objectwise if colim : J ⥤ A ⥤ A preserves finite products.
This holds for all shapes J if A is a preadditive category.
This can also easily be applied to filtered J in the case when A is a category of sets, and
eventually to sifted J once that API is developed.
theorem CategoryTheory.isSheaf_pointwiseColimit {A : Type u_1} {C : Type u_2} {J : Type u_3} [Category.{v_1, u_1} A] [Category.{v_2, u_2} C] [Category.{v_3, u_3} J] [FinitaryExtensive C] [Limits.HasColimitsOfShape J A] [Limits.PreservesFiniteProducts Limits.colim] (G : Functor J (Sheaf (extensiveTopology C) A)) :
Presheaf.IsSheaf (extensiveTopology C) (Limits.pointwiseCocone (G.comp (sheafToPresheaf (extensiveTopology C) A))).pt
instance CategoryTheory.instPreservesFiniteProductsFunctorColimOfPreadditive {A : Type u_1} {J : Type u_3} [Category.{v_1, u_1} A] [Category.{v_3, u_3} J] [Limits.HasColimitsOfShape J A] [Preadditive A] :
instance CategoryTheory.instPreservesColimitsOfShapeSheafExtensiveTopologyFunctorOppositeSheafToPresheafOfPreservesFiniteProductsColim {A : Type u_1} {C : Type u_2} {J : Type u_3} [Category.{v_1, u_1} A] [Category.{v_2, u_2} C] [Category.{v_3, u_3} J] [FinitaryExtensive C] [Limits.HasColimitsOfShape J A] [Limits.PreservesFiniteProducts Limits.colim] :
instance CategoryTheory.instPreservesFiniteColimitsSheafExtensiveTopologyFunctorOppositeSheafToPresheafOfPreadditiveOfHasFiniteColimits {A : Type u_1} {C : Type u_2} [Category.{v_1, u_1} A] [Category.{v_2, u_2} C] [FinitaryExtensive C] [Preadditive A] [Limits.HasFiniteColimits A] :