Presheaves in C have limits and colimits when C does.

instance TopCat.instHasLimitsPresheaf {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasLimits C] (X : TopCat) : CategoryTheory.Limits.HasLimits (TopCat.Presheaf C X)

Equations

• ⋯ = ⋯

instance TopCat.instHasColimitsOfSizePresheafOfHasColimits {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasColimits C] (X : TopCat) : CategoryTheory.Limits.HasColimitsOfSize.{v, v, max v w, max (max u v) w} (TopCat.Presheaf C X)

Equations

• ⋯ = ⋯

instance TopCat.instCreatesLimitsSheafPresheafForgetOfHasLimits {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasLimits C] (X : TopCat) : CategoryTheory.CreatesLimits (TopCat.Sheaf.forget C X)

Equations

• X.instCreatesLimitsSheafPresheafForgetOfHasLimits = CategoryTheory.Sheaf.createsLimits

instance TopCat.instHasLimitsOfSizeSheafOfHasLimits {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasLimits C] (X : TopCat) : CategoryTheory.Limits.HasLimitsOfSize.{v, v, v, max v u} (TopCat.Sheaf C X)

Equations

• ⋯ = ⋯

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), (F.obj j).IsSheaf) {c : CategoryTheory.Limits.Cone F} (hc : CategoryTheory.Limits.IsLimit c) : c.pt.IsSheaf

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), (F.obj j).IsSheaf) : (CategoryTheory.Limits.limit F).IsSheaf