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}
[CategoryTheory.Category.{u_4, u_1} A]
[CategoryTheory.Category.{u_6, u_2} C]
[CategoryTheory.Category.{u_5, u_3} J]
[CategoryTheory.FinitaryExtensive C]
[CategoryTheory.Limits.HasColimitsOfShape J A]
[CategoryTheory.Limits.PreservesFiniteProducts CategoryTheory.Limits.colim]
(G : CategoryTheory.Functor J (CategoryTheory.Sheaf (CategoryTheory.extensiveTopology C) A))
:
instance
CategoryTheory.instPreservesFiniteProductsFunctorColimOfPreadditive
{A : Type u_1}
{J : Type u_3}
[CategoryTheory.Category.{u_4, u_1} A]
[CategoryTheory.Category.{u_5, u_3} J]
[CategoryTheory.Limits.HasColimitsOfShape J A]
[CategoryTheory.Preadditive A]
:
CategoryTheory.Limits.PreservesFiniteProducts CategoryTheory.Limits.colim
instance
CategoryTheory.instPreservesColimitsOfShapeSheafExtensiveTopologyFunctorOppositeSheafToPresheafOfPreservesFiniteProductsColim
{A : Type u_1}
{C : Type u_2}
{J : Type u_3}
[CategoryTheory.Category.{u_4, u_1} A]
[CategoryTheory.Category.{u_6, u_2} C]
[CategoryTheory.Category.{u_5, u_3} J]
[CategoryTheory.FinitaryExtensive C]
[CategoryTheory.Limits.HasColimitsOfShape J A]
[CategoryTheory.Limits.PreservesFiniteProducts CategoryTheory.Limits.colim]
:
instance
CategoryTheory.instPreservesFiniteColimitsSheafExtensiveTopologyFunctorOppositeSheafToPresheafOfPreadditiveOfHasFiniteColimits
{A : Type u_1}
{C : Type u_2}
[CategoryTheory.Category.{u_4, u_1} A]
[CategoryTheory.Category.{u_5, u_2} C]
[CategoryTheory.FinitaryExtensive C]
[CategoryTheory.Preadditive A]
[CategoryTheory.Limits.HasFiniteColimits A]
: