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) : CategoryTheory.Limits.HasLimits (TopCat.Presheaf C X)

Equations

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

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

Equations

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

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

Equations

• TopCat.instCreatesLimitsSheafSheafCatPresheafInstCategoryPresheafForget X = CategoryTheory.Sheaf.createsLimits

instance TopCat.instHasLimitsOfSizeSheafSheafCat {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

• (_ : CategoryTheory.Limits.HasLimitsOfSize.{v, v, v, max v u} (TopCat.Sheaf C X)) = (_ : CategoryTheory.Limits.HasLimitsOfSize.{v, v, v, max u v} (TopCat.Sheaf C X))

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

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