Presheaves in C
have limits and colimits when C
does. #
instance
TopCat.instHasLimitsPresheafInstCategoryPresheaf
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasLimits C]
(X : TopCat)
:
theorem
TopCat.isSheaf_of_isLimit
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{J : Type v}
[CategoryTheory.SmallCategory J]
[CategoryTheory.Limits.HasLimits C]
{X : TopCat}
(F : CategoryTheory.Functor J (TopCat.Presheaf C X))
(H : ∀ (j : J), TopCat.Presheaf.IsSheaf (F.obj j))
{c : CategoryTheory.Limits.Cone F}
(hc : CategoryTheory.Limits.IsLimit c)
:
theorem
TopCat.limit_isSheaf
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{J : Type v}
[CategoryTheory.SmallCategory J]
[CategoryTheory.Limits.HasLimits C]
{X : TopCat}
(F : CategoryTheory.Functor J (TopCat.Presheaf C X))
(H : ∀ (j : J), TopCat.Presheaf.IsSheaf (F.obj j))
: