Presheaves in C have limits and colimits when C does.

instance TopCat.instHasLimitsOfShapePresheaf {C : Type u} [CategoryTheory.Category.{v, u} C] {J : Type w} [CategoryTheory.Category.{v_1, w} J] [CategoryTheory.Limits.HasLimitsOfShape J C] (X : TopCat) : CategoryTheory.Limits.HasLimitsOfShape J (Presheaf C X)

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

instance TopCat.instHasColimitsOfShapePresheaf {C : Type u} [CategoryTheory.Category.{v, u} C] {J : Type w} [CategoryTheory.Category.{v_1, w} J] [CategoryTheory.Limits.HasColimitsOfShape J C] (X : TopCat) : CategoryTheory.Limits.HasColimitsOfShape J (Presheaf C X)

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

@[instance_reducible]

noncomputable instance TopCat.instCreatesLimitsOfShapeSheafPresheafForgetOfHasLimitsOfShape {C : Type u} [CategoryTheory.Category.{v, u} C] {J : Type w} [CategoryTheory.Category.{v_1, w} J] [CategoryTheory.Limits.HasLimitsOfShape J C] (X : TopCat) : CategoryTheory.CreatesLimitsOfShape J (Sheaf.forget C X)

Equations

• One or more equations did not get rendered due to their size.

instance TopCat.instHasLimitsOfShapeSheaf {C : Type u} [CategoryTheory.Category.{v, u} C] {J : Type w} [CategoryTheory.Category.{v_1, w} J] [CategoryTheory.Limits.HasLimitsOfShape J C] (X : TopCat) : CategoryTheory.Limits.HasLimitsOfShape J (Sheaf C X)

@[instance_reducible]

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

Equations

• X.instCreatesLimitsSheafPresheafForgetOfHasLimits = { CreatesLimitsOfShape := fun {J : Type ?u.2} [CategoryTheory.Category.{?u.2, ?u.2} J] => inferInstance }

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} (Sheaf C X)

theorem TopCat.isSheaf_of_isLimit {C : Type u} [CategoryTheory.Category.{v, u} C] {J : Type w} [CategoryTheory.Category.{v_1, w} J] [CategoryTheory.Limits.HasLimitsOfShape J C] {X : TopCat} (F : CategoryTheory.Functor J (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 w} [CategoryTheory.Category.{v_1, w} J] [CategoryTheory.Limits.HasLimitsOfShape J C] {X : TopCat} (F : CategoryTheory.Functor J (Presheaf C X)) (H : ∀ (j : J), (F.obj j).IsSheaf) : (CategoryTheory.Limits.limit F).IsSheaf