AB axioms in sheaf categories #
This file proves that, when the relevant limits and colimits and sheafification exist, exactness of
limits and colimits carries over from A to categories of A-valued sheaves.
instance
CategoryTheory.instHasExactColimitsOfShapeSheafOfHasFiniteLimitsOfPreservesColimitsOfShapeFunctorOppositeSheafToPresheaf
{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]
(K : CategoryTheory.GrothendieckTopology C)
[CategoryTheory.HasWeakSheafify K A]
[CategoryTheory.Limits.HasFiniteLimits A]
[CategoryTheory.Limits.HasColimitsOfShape J A]
[CategoryTheory.HasExactColimitsOfShape J A]
[CategoryTheory.Limits.PreservesColimitsOfShape J (CategoryTheory.sheafToPresheaf K A)]
:
instance
CategoryTheory.instHasExactLimitsOfShapeSheafOfHasFiniteColimitsOfPreservesFiniteColimitsFunctorOppositeSheafToPresheaf
{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]
(K : CategoryTheory.GrothendieckTopology C)
[CategoryTheory.HasWeakSheafify K A]
[CategoryTheory.Limits.HasFiniteColimits A]
[CategoryTheory.Limits.HasLimitsOfShape J A]
[CategoryTheory.HasExactLimitsOfShape J A]
[CategoryTheory.Limits.PreservesFiniteColimits (CategoryTheory.sheafToPresheaf K A)]
: