Presheaves in C have limits and colimits when C does.

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

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

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

theorem TopCat.instHasColimitsOfSizePresheafOfHasColimits {C : Type u} [CategoryTheory.Category C] [CategoryTheory.Limits.HasColimits C] (X : TopCat) : CategoryTheory.Limits.HasColimitsOfSize (Presheaf C X)

def TopCat.instCreatesLimitsOfShapeSheafPresheafForgetOfHasLimitsOfShape {C : Type u} [CategoryTheory.Category C] {J : Type w} [CategoryTheory.Category J] [CategoryTheory.Limits.HasLimitsOfShape J C] (X : TopCat) : CategoryTheory.CreatesLimitsOfShape J (Sheaf.forget C X)

Equations

• Eq X.instCreatesLimitsOfShapeSheafPresheafForgetOfHasLimitsOfShape CategoryTheory.Sheaf.createsLimitsOfShape

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

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

Equations

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

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

theorem TopCat.isSheaf_of_isLimit {C : Type u} [CategoryTheory.Category C] {J : Type w} [CategoryTheory.Category 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 C] {J : Type w} [CategoryTheory.Category 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