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.{u_4, u_1} A]
[Category.{u_6, u_2} C]
[Category.{u_5, 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.{u_4, u_1} A]
[Category.{u_5, 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.{u_4, u_1} A]
[Category.{u_6, u_2} C]
[Category.{u_5, 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.{u_4, u_1} A]
[Category.{u_5, u_2} C]
[FinitaryExtensive C]
[Preadditive A]
[Limits.HasFiniteColimits A]
: