feat: port Topology.Sheaves.Limits (#4096)

Author: Parcly-Taxel

Mathlib.lean

@@ -2225,6 +2225,7 @@ import Mathlib.Topology.Sets.Opens
 import Mathlib.Topology.Sets.Order
 import Mathlib.Topology.Sheaves.Abelian
 import Mathlib.Topology.Sheaves.Init
+import Mathlib.Topology.Sheaves.Limits
 import Mathlib.Topology.Sheaves.Presheaf
 import Mathlib.Topology.Sheaves.PresheafOfFunctions
 import Mathlib.Topology.Sheaves.Sheaf

Mathlib/CategoryTheory/Sites/Limits.lean

@@ -171,7 +171,7 @@ instance : HasLimitsOfShape K (Sheaf J D) :=
 
 end
 
-instance [HasLimits D] : CreatesLimits (sheafToPresheaf J D) :=
+instance createsLimits [HasLimits D] : CreatesLimits (sheafToPresheaf J D) :=
   ⟨createsLimitsOfShape⟩
 
 instance [HasLimits D] : HasLimits (Sheaf J D) :=

Mathlib/Topology/Sheaves/Limits.lean

@@ -0,0 +1,62 @@
+/-
+Copyright (c) 2020 Scott Morrison. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Scott Morrison
+
+! This file was ported from Lean 3 source module topology.sheaves.limits
+! leanprover-community/mathlib commit 70fd9563a21e7b963887c9360bd29b2393e6225a
+! Please do not edit these lines, except to modify the commit id
+! if you have ported upstream changes.
+-/
+import Mathlib.Topology.Sheaves.Sheaf
+import Mathlib.CategoryTheory.Sites.Limits
+import Mathlib.CategoryTheory.Limits.FunctorCategory
+
+/-!
+# Presheaves in `C` have limits and colimits when `C` does.
+-/
+
+
+noncomputable section
+
+universe v u
+
+open CategoryTheory
+
+open CategoryTheory.Limits
+
+variable {C : Type u} [Category.{v} C] {J : Type v} [SmallCategory J]
+
+namespace TopCat
+
+instance [HasLimits C] (X : TopCat) : HasLimits (Presheaf C X) :=
+  Limits.functorCategoryHasLimitsOfSize.{v, v}
+
+instance [HasColimits C] (X : TopCat) : HasColimitsOfSize.{v} (Presheaf C X) :=
+  Limits.functorCategoryHasColimitsOfSize
+
+instance [HasLimits C] (X : TopCat) : CreatesLimits (Sheaf.forget C X) :=
+  Sheaf.createsLimits.{u, v, v}
+
+instance [HasLimits C] (X : TopCat) : HasLimitsOfSize.{v} (Sheaf.{v} C X) :=
+  has_limits_of_has_limits_creates_limits (Sheaf.forget C X)
+
+theorem isSheaf_of_isLimit [HasLimits C] {X : TopCat} (F : J ⥤ Presheaf.{v} C X)
+    (H : ∀ j, (F.obj j).IsSheaf) {c : Cone F} (hc : IsLimit c) : c.pt.IsSheaf := by
+  let F' : J ⥤ Sheaf C X :=
+    { obj := fun j => ⟨F.obj j, H j⟩
+      map := fun f => ⟨F.map f⟩ }
+  let e : F' ⋙ Sheaf.forget C X ≅ F := NatIso.ofComponents (fun _ => Iso.refl _) (by aesop_cat)
+  exact Presheaf.isSheaf_of_iso
+    ((isLimitOfPreserves (Sheaf.forget C X) (limit.isLimit F')).conePointsIsoOfNatIso hc e)
+    (limit F').2
+set_option linter.uppercaseLean3 false in
+#align Top.is_sheaf_of_is_limit TopCat.isSheaf_of_isLimit
+
+theorem limit_isSheaf [HasLimits C] {X : TopCat} (F : J ⥤ Presheaf.{v} C X)
+    (H : ∀ j, (F.obj j).IsSheaf) : (limit F).IsSheaf :=
+  isSheaf_of_isLimit F H (limit.isLimit F)
+set_option linter.uppercaseLean3 false in
+#align Top.limit_is_sheaf TopCat.limit_isSheaf
+
+end TopCat