feat: port Topology.Sheaves.Functors (#4392)

Mathlib.lean

@@ -2470,6 +2470,7 @@ import Mathlib.Topology.Sets.Compacts
 import Mathlib.Topology.Sets.Opens
 import Mathlib.Topology.Sets.Order
 import Mathlib.Topology.Sheaves.Abelian
+import Mathlib.Topology.Sheaves.Functors
 import Mathlib.Topology.Sheaves.Init
 import Mathlib.Topology.Sheaves.Limits
 import Mathlib.Topology.Sheaves.PUnit

Mathlib/Topology/Sheaves/Functors.lean

@@ -0,0 +1,101 @@
+/-
+Copyright (c) 2021 Junyan Xu. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Junyan Xu
+
+! This file was ported from Lean 3 source module topology.sheaves.functors
+! leanprover-community/mathlib commit 85d6221d32c37e68f05b2e42cde6cee658dae5e9
+! Please do not edit these lines, except to modify the commit id
+! if you have ported upstream changes.
+-/
+import Mathlib.Topology.Sheaves.SheafCondition.PairwiseIntersections
+
+/-!
+# functors between categories of sheaves
+
+Show that the pushforward of a sheaf is a sheaf, and define
+the pushforward functor from the category of C-valued sheaves
+on X to that of sheaves on Y, given a continuous map between
+topological spaces X and Y.
+
+TODO: pullback for presheaves and sheaves
+-/
+
+
+noncomputable section
+
+universe w v u
+
+open CategoryTheory
+
+open CategoryTheory.Limits
+
+open TopologicalSpace
+
+variable {C : Type u} [Category.{v} C]
+
+variable {X Y : TopCat.{w}} (f : X ⟶ Y)
+
+variable ⦃ι : Type w⦄ {U : ι → Opens Y}
+
+namespace TopCat
+
+namespace Presheaf.SheafConditionPairwiseIntersections
+
+theorem map_diagram :
+    Pairwise.diagram U ⋙ Opens.map f = Pairwise.diagram ((Opens.map f).obj ∘ U) := by
+  have obj_eq : ∀ (j : Pairwise ι), (Pairwise.diagram U ⋙ Opens.map f).obj j =
+    (Pairwise.diagram ((Opens.map f).toPrefunctor.obj ∘ U)).obj j
+  . rintro ⟨i⟩ <;> rfl
+  refine Functor.hext obj_eq ?_
+  intro i j g; apply Subsingleton.helim
+  rw [obj_eq, obj_eq]
+set_option linter.uppercaseLean3 false in
+#align Top.presheaf.sheaf_condition_pairwise_intersections.map_diagram TopCat.Presheaf.SheafConditionPairwiseIntersections.map_diagram
+
+theorem mapCocone :
+    HEq ((Opens.map f).mapCocone (Pairwise.cocone U)) 
+      (Pairwise.cocone ((Opens.map f).obj ∘ U)) := by
+  unfold Functor.mapCocone Cocones.functoriality; dsimp; congr
+  iterate 2 rw [map_diagram]; rw [Opens.map_iSup]
+  apply Subsingleton.helim; rw [map_diagram, Opens.map_iSup]
+  apply proof_irrel_heq
+set_option linter.uppercaseLean3 false in
+#align Top.presheaf.sheaf_condition_pairwise_intersections.map_cocone TopCat.Presheaf.SheafConditionPairwiseIntersections.mapCocone
+
+theorem pushforward_sheaf_of_sheaf {F : Presheaf C X} (h : F.IsSheafPairwiseIntersections) :
+    (f _* F).IsSheafPairwiseIntersections := fun ι U => by
+  convert h ((Opens.map f).obj ∘ U) using 2
+  rw [← map_diagram]; rfl
+  change HEq (Functor.mapCone F ((Opens.map f).mapCocone (Pairwise.cocone U)).op) _
+  congr
+  iterate 2 rw [map_diagram]
+  apply mapCocone
+set_option linter.uppercaseLean3 false in
+#align Top.presheaf.sheaf_condition_pairwise_intersections.pushforward_sheaf_of_sheaf TopCat.Presheaf.SheafConditionPairwiseIntersections.pushforward_sheaf_of_sheaf
+
+end Presheaf.SheafConditionPairwiseIntersections
+
+namespace Sheaf
+
+open Presheaf
+
+/-- The pushforward of a sheaf (by a continuous map) is a sheaf.
+-/
+theorem pushforward_sheaf_of_sheaf {F : X.Presheaf C} (h : F.IsSheaf) : (f _* F).IsSheaf := by
+  rw [isSheaf_iff_isSheafPairwiseIntersections] at h ⊢ ;
+  exact SheafConditionPairwiseIntersections.pushforward_sheaf_of_sheaf f h
+set_option linter.uppercaseLean3 false in
+#align Top.sheaf.pushforward_sheaf_of_sheaf TopCat.Sheaf.pushforward_sheaf_of_sheaf
+
+/-- The pushforward functor.
+-/
+def pushforward (f : X ⟶ Y) : X.Sheaf C ⥤ Y.Sheaf C where
+  obj ℱ := ⟨f _* ℱ.1, pushforward_sheaf_of_sheaf f ℱ.2⟩
+  map {_ _} g := ⟨pushforwardMap f g.1⟩
+set_option linter.uppercaseLean3 false in
+#align Top.sheaf.pushforward TopCat.Sheaf.pushforward
+
+end Sheaf
+
+end TopCat