refactor(topology/sheaves): Redefine sheaves in terms of Grothendieck…

… topology. (#15384)

We change the "official definition" of sheaves over topological spaces from the equalizer diagram condition to the condition in terms of the Grothendieck topology on `Opens(X)`. The benefit is that 
1. The `X.Sheaf C` category is now defeq to `(opens.grothendieck_topology X).Sheaf C`, so that functors between categories of sheaves over sites could be specialized onto topological spaces without the abundant equivalences.
2. It allows sheaves over spaces to value in arbitrary categories that doesn't have all products.

The original sheaf condition is now called `presheaf.is_sheaf_equalizer_products`, and `presheaf.is_sheaf_iff_is_sheaf_equalizer_products` (in `topology.sheaves.sheaf_condition.sites`) shows that the two are equivalent.



Co-authored-by: Andrew Yang <36414270+erdOne@users.noreply.github.com>

src/algebraic_geometry/AffineScheme.lean

@@ -491,9 +491,10 @@ begin
   erw [← X.presheaf.map_comp, Spec_Γ_naturality_assoc],
   congr' 1,
   simp only [← category.assoc],
-  transitivity _ ≫ (structure_sheaf (X.presheaf.obj $ op U)).1.germ ⟨_, _⟩,
+  transitivity _ ≫ (structure_sheaf (X.presheaf.obj $ op U)).presheaf.germ ⟨_, _⟩,
   { refl },
-  convert ((structure_sheaf (X.presheaf.obj $ op U)).1.germ_res (hom_of_le le_top) ⟨_, _⟩) using 2,
+  convert ((structure_sheaf (X.presheaf.obj $ op U)).presheaf.germ_res (hom_of_le le_top) ⟨_, _⟩)
+    using 2,
   rw category.assoc,
   erw nat_trans.naturality,
   rw [← LocallyRingedSpace.Γ_map_op, ← LocallyRingedSpace.Γ.map_comp_assoc, ← op_comp],

src/algebraic_geometry/Gamma_Spec_adjunction.lean

@@ -191,7 +191,7 @@ def to_Γ_Spec : X ⟶ Spec.LocallyRingedSpace_obj (Γ.obj (op X)) :=
     intro x,
     let p : prime_spectrum (Γ.obj (op X)) := X.to_Γ_Spec_fun x,
     constructor, /- show stalk map is local hom ↓ -/
-    let S := (structure_sheaf _).val.stalk p,
+    let S := (structure_sheaf _).presheaf.stalk p,
     rintros (t : S) ht,
     obtain ⟨⟨r, s⟩, he⟩ := is_localization.surj p.as_ideal.prime_compl t,
     dsimp at he,
@@ -272,7 +272,7 @@ begin
   apply LocallyRingedSpace.comp_ring_hom_ext,
   { ext (p : prime_spectrum R) x,
     erw ← is_localization.at_prime.to_map_mem_maximal_iff
-      ((structure_sheaf R).val.stalk p) p.as_ideal x,
+      ((structure_sheaf R).presheaf.stalk p) p.as_ideal x,
     refl },
   { intro r, apply to_open_res },
 end

src/algebraic_geometry/open_immersion.lean

@@ -772,7 +772,7 @@ lemma of_stalk_iso {X Y : SheafedSpace C} (f : X ⟶ Y)
 { base_open := hf,
   c_iso := λ U, begin
     apply_with (Top.presheaf.app_is_iso_of_stalk_functor_map_iso
-      (show Y.sheaf ⟶ (Top.sheaf.pushforward f.base).obj X.sheaf, from f.c)) { instances := ff },
+      (show Y.sheaf ⟶ (Top.sheaf.pushforward f.base).obj X.sheaf, from ⟨f.c⟩)) { instances := ff },
     rintros ⟨_, y, hy, rfl⟩,
     specialize H y,
     delta PresheafedSpace.stalk_map at H,

src/algebraic_geometry/projective_spectrum/structure_sheaf.lean

@@ -212,7 +212,7 @@ def Proj.structure_sheaf : sheaf CommRing (projective_spectrum.Top 𝒜) :=
   -- We check the sheaf condition under `forget CommRing`.
   (is_sheaf_iff_is_sheaf_comp _ _).mpr
     (is_sheaf_of_iso (structure_presheaf_comp_forget 𝒜).symm
-      (structure_sheaf_in_Type 𝒜).property)⟩
+      (structure_sheaf_in_Type 𝒜).cond)⟩
 
 end projective_spectrum
 
@@ -247,25 +247,26 @@ def open_to_localization (U : opens (projective_spectrum.Top 𝒜)) (x : project
 to a homogeneous prime ideal `x` to the *homogeneous localization* at `x`,
 formed by gluing the `open_to_localization` maps. -/
 def stalk_to_fiber_ring_hom (x : projective_spectrum.Top 𝒜) :
-  (Proj.structure_sheaf 𝒜).1.stalk x ⟶ CommRing.of (at x) :=
+  (Proj.structure_sheaf 𝒜).presheaf.stalk x ⟶ CommRing.of (at x) :=
 limits.colimit.desc (((open_nhds.inclusion x).op) ⋙ (Proj.structure_sheaf 𝒜).1)
   { X := _,
     ι :=
     { app := λ U, open_to_localization 𝒜 ((open_nhds.inclusion _).obj (unop U)) x (unop U).2, } }
 
 @[simp] lemma germ_comp_stalk_to_fiber_ring_hom (U : opens (projective_spectrum.Top 𝒜)) (x : U) :
-  (Proj.structure_sheaf 𝒜).1.germ x ≫ stalk_to_fiber_ring_hom 𝒜 x =
+  (Proj.structure_sheaf 𝒜).presheaf.germ x ≫ stalk_to_fiber_ring_hom 𝒜 x =
   open_to_localization 𝒜 U x x.2 :=
 limits.colimit.ι_desc _ _
 
 @[simp] lemma stalk_to_fiber_ring_hom_germ' (U : opens (projective_spectrum.Top 𝒜))
   (x : projective_spectrum.Top 𝒜) (hx : x ∈ U) (s : (Proj.structure_sheaf 𝒜).1.obj (op U)) :
-  stalk_to_fiber_ring_hom 𝒜 x ((Proj.structure_sheaf 𝒜).1.germ ⟨x, hx⟩ s) = (s.1 ⟨x, hx⟩ : _) :=
+  stalk_to_fiber_ring_hom 𝒜 x
+    ((Proj.structure_sheaf 𝒜).presheaf.germ ⟨x, hx⟩ s) = (s.1 ⟨x, hx⟩ : _) :=
 ring_hom.ext_iff.1 (germ_comp_stalk_to_fiber_ring_hom 𝒜 U ⟨x, hx⟩ : _) s
 
 @[simp] lemma stalk_to_fiber_ring_hom_germ (U : opens (projective_spectrum.Top 𝒜)) (x : U)
   (s : (Proj.structure_sheaf 𝒜).1.obj (op U)) :
-  stalk_to_fiber_ring_hom 𝒜 x ((Proj.structure_sheaf 𝒜).1.germ x s) = s.1 x :=
+  stalk_to_fiber_ring_hom 𝒜 x ((Proj.structure_sheaf 𝒜).presheaf.germ x s) = s.1 x :=
 by { cases x, exact stalk_to_fiber_ring_hom_germ' 𝒜 U _ _ _ }
 
 lemma homogeneous_localization.mem_basic_open (x : projective_spectrum.Top 𝒜) (f : at x) :
@@ -292,19 +293,19 @@ def section_in_basic_open (x : projective_spectrum.Top 𝒜) :
 stalk at `x` obtained by `section_in_basic_open`. This is the inverse of `stalk_to_fiber_ring_hom`.
 -/
 def homogeneous_localization_to_stalk (x : projective_spectrum.Top 𝒜) :
-  (at x) → (Proj.structure_sheaf 𝒜).1.stalk x :=
-λ f, (Proj.structure_sheaf 𝒜).1.germ
+  (at x) → (Proj.structure_sheaf 𝒜).presheaf.stalk x :=
+λ f, (Proj.structure_sheaf 𝒜).presheaf.germ
   (⟨x, homogeneous_localization.mem_basic_open _ x f⟩ : projective_spectrum.basic_open _ f.denom)
   (section_in_basic_open _ x f)
 
 /--Using `homogeneous_localization_to_stalk`, we construct a ring isomorphism between stalk at `x`
 and homogeneous localization at `x` for any point `x` in `Proj`.-/
 def Proj.stalk_iso' (x : projective_spectrum.Top 𝒜) :
-  (Proj.structure_sheaf 𝒜).1.stalk x ≃+* CommRing.of (at x)  :=
+  (Proj.structure_sheaf 𝒜).presheaf.stalk x ≃+* CommRing.of (at x)  :=
 ring_equiv.of_bijective (stalk_to_fiber_ring_hom _ x)
 ⟨λ z1 z2 eq1, begin
-  obtain ⟨u1, memu1, s1, rfl⟩ := (Proj.structure_sheaf 𝒜).1.germ_exist x z1,
-  obtain ⟨u2, memu2, s2, rfl⟩ := (Proj.structure_sheaf 𝒜).1.germ_exist x z2,
+  obtain ⟨u1, memu1, s1, rfl⟩ := (Proj.structure_sheaf 𝒜).presheaf.germ_exist x z1,
+  obtain ⟨u2, memu2, s2, rfl⟩ := (Proj.structure_sheaf 𝒜).presheaf.germ_exist x z2,
   obtain ⟨v1, memv1, i1, ⟨j1, ⟨a1, a1_mem⟩, ⟨b1, b1_mem⟩, hs1⟩⟩ := s1.2 ⟨x, memu1⟩,
   obtain ⟨v2, memv2, i2, ⟨j2, ⟨a2, a2_mem⟩, ⟨b2, b2_mem⟩, hs2⟩⟩ := s2.2 ⟨x, memu2⟩,
   obtain ⟨b1_nin_x, eq2⟩ := hs1 ⟨x, memv1⟩,

src/algebraic_geometry/sheafed_space.lean

@@ -119,8 +119,9 @@ The restriction of a sheafed space along an open embedding into the space.
 -/
 def restrict {U : Top} (X : SheafedSpace C)
   {f : U ⟶ (X : Top.{v})} (h : open_embedding f) : SheafedSpace C :=
-{ is_sheaf := λ ι 𝒰, ⟨is_limit.of_iso_limit
-    ((is_limit.postcompose_inv_equiv _ _).inv_fun (X.is_sheaf _).some)
+{ is_sheaf := (is_sheaf_iff_is_sheaf_equalizer_products _).mpr $ λ ι 𝒰, ⟨is_limit.of_iso_limit
+    ((is_limit.postcompose_inv_equiv _ _).inv_fun
+    ((is_sheaf_iff_is_sheaf_equalizer_products _).mp X.is_sheaf _).some)
     (sheaf_condition_equalizer_products.fork.iso_of_open_embedding h 𝒰).symm⟩,
   ..X.to_PresheafedSpace.restrict h }
 

src/algebraic_geometry/structure_sheaf.lean

@@ -262,7 +262,7 @@ def Spec.structure_sheaf : sheaf CommRing (prime_spectrum.Top R) :=
   -- We check the sheaf condition under `forget CommRing`.
   (is_sheaf_iff_is_sheaf_comp _ _).mpr
     (is_sheaf_of_iso (structure_presheaf_comp_forget R).symm
-      (structure_sheaf_in_Type R).property)⟩
+      (structure_sheaf_in_Type R).cond)⟩
 
 open Spec (structure_sheaf)
 
@@ -402,20 +402,20 @@ subtype.eq $ funext $ λ x, eq.symm $ is_localization.mk'_one _ f
 
 /-- The canonical ring homomorphism interpreting an element of `R` as an element of
 the stalk of `structure_sheaf R` at `x`. -/
-def to_stalk (x : prime_spectrum.Top R) : CommRing.of R ⟶ (structure_sheaf R).1.stalk x :=
-(to_open R ⊤ ≫ (structure_sheaf R).1.germ ⟨x, ⟨⟩⟩ : _)
+def to_stalk (x : prime_spectrum.Top R) : CommRing.of R ⟶ (structure_sheaf R).presheaf.stalk x :=
+(to_open R ⊤ ≫ (structure_sheaf R).presheaf.germ ⟨x, ⟨⟩⟩ : _)
 
 @[simp] lemma to_open_germ (U : opens (prime_spectrum.Top R)) (x : U) :
-  to_open R U ≫ (structure_sheaf R).1.germ x =
+  to_open R U ≫ (structure_sheaf R).presheaf.germ x =
   to_stalk R x :=
 by { rw [← to_open_res R ⊤ U (hom_of_le le_top : U ⟶ ⊤), category.assoc, presheaf.germ_res], refl }
 
 @[simp] lemma germ_to_open (U : opens (prime_spectrum.Top R)) (x : U) (f : R) :
-  (structure_sheaf R).1.germ x (to_open R U f) = to_stalk R x f :=
+  (structure_sheaf R).presheaf.germ x (to_open R U f) = to_stalk R x f :=
 by { rw ← to_open_germ, refl }
 
 lemma germ_to_top (x : prime_spectrum.Top R) (f : R) :
-  (structure_sheaf R).1.germ (⟨x, trivial⟩ : (⊤ : opens (prime_spectrum.Top R)))
+  (structure_sheaf R).presheaf.germ (⟨x, trivial⟩ : (⊤ : opens (prime_spectrum.Top R)))
     (to_open R ⊤ f) =
     to_stalk R x f :=
 rfl
@@ -432,7 +432,7 @@ by { erw ← germ_to_open R (basic_open (f : R)) ⟨x, f.2⟩ (f : R),
 /-- The canonical ring homomorphism from the localization of `R` at `p` to the stalk
 of the structure sheaf at the point `p`. -/
 def localization_to_stalk (x : prime_spectrum.Top R) :
-  CommRing.of (localization.at_prime x.as_ideal) ⟶ (structure_sheaf R).1.stalk x :=
+  CommRing.of (localization.at_prime x.as_ideal) ⟶ (structure_sheaf R).presheaf.stalk x :=
 show localization.at_prime x.as_ideal →+* _, from
 is_localization.lift (is_unit_to_stalk R x)
 
@@ -443,7 +443,7 @@ is_localization.lift_eq _ f
 @[simp] lemma localization_to_stalk_mk' (x : prime_spectrum.Top R) (f : R)
   (s : (as_ideal x).prime_compl) :
   localization_to_stalk R x (is_localization.mk' _ f s : localization _) =
-  (structure_sheaf R).1.germ (⟨x, s.2⟩ : basic_open (s : R))
+  (structure_sheaf R).presheaf.germ (⟨x, s.2⟩ : basic_open (s : R))
     (const R f s (basic_open s) (λ _, id)) :=
 (is_localization.lift_mk'_spec _ _ _ _).2 $
 by erw [← germ_to_open R (basic_open s) ⟨x, s.2⟩, ← germ_to_open R (basic_open s) ⟨x, s.2⟩,
@@ -478,25 +478,25 @@ rfl
 a prime ideal `p` to the localization of `R` at `p`,
 formed by gluing the `open_to_localization` maps. -/
 def stalk_to_fiber_ring_hom (x : prime_spectrum.Top R) :
-  (structure_sheaf R).1.stalk x ⟶ CommRing.of (localization.at_prime x.as_ideal) :=
+  (structure_sheaf R).presheaf.stalk x ⟶ CommRing.of (localization.at_prime x.as_ideal) :=
 limits.colimit.desc (((open_nhds.inclusion x).op) ⋙ (structure_sheaf R).1)
   { X := _,
     ι :=
     { app := λ U, open_to_localization R ((open_nhds.inclusion _).obj (unop U)) x (unop U).2, } }
 
 @[simp] lemma germ_comp_stalk_to_fiber_ring_hom (U : opens (prime_spectrum.Top R)) (x : U) :
-  (structure_sheaf R).1.germ x ≫ stalk_to_fiber_ring_hom R x =
+  (structure_sheaf R).presheaf.germ x ≫ stalk_to_fiber_ring_hom R x =
   open_to_localization R U x x.2 :=
 limits.colimit.ι_desc _ _
 
 @[simp] lemma stalk_to_fiber_ring_hom_germ' (U : opens (prime_spectrum.Top R))
   (x : prime_spectrum.Top R) (hx : x ∈ U) (s : (structure_sheaf R).1.obj (op U)) :
-  stalk_to_fiber_ring_hom R x ((structure_sheaf R).1.germ ⟨x, hx⟩ s) = (s.1 ⟨x, hx⟩ : _) :=
+  stalk_to_fiber_ring_hom R x ((structure_sheaf R).presheaf.germ ⟨x, hx⟩ s) = (s.1 ⟨x, hx⟩ : _) :=
 ring_hom.ext_iff.1 (germ_comp_stalk_to_fiber_ring_hom R U ⟨x, hx⟩ : _) s
 
 @[simp] lemma stalk_to_fiber_ring_hom_germ (U : opens (prime_spectrum.Top R)) (x : U)
   (s : (structure_sheaf R).1.obj (op U)) :
-  stalk_to_fiber_ring_hom R x ((structure_sheaf R).1.germ x s) = s.1 x :=
+  stalk_to_fiber_ring_hom R x ((structure_sheaf R).presheaf.germ x s) = s.1 x :=
 by { cases x, exact stalk_to_fiber_ring_hom_germ' R U _ _ _ }
 
 @[simp] lemma to_stalk_comp_stalk_to_fiber_ring_hom (x : prime_spectrum.Top R) :
@@ -510,15 +510,15 @@ ring_hom.ext_iff.1 (to_stalk_comp_stalk_to_fiber_ring_hom R x) _
 /-- The ring isomorphism between the stalk of the structure sheaf of `R` at a point `p`
 corresponding to a prime ideal in `R` and the localization of `R` at `p`. -/
 @[simps] def stalk_iso (x : prime_spectrum.Top R) :
-  (structure_sheaf R).1.stalk x ≅ CommRing.of (localization.at_prime x.as_ideal) :=
+  (structure_sheaf R).presheaf.stalk x ≅ CommRing.of (localization.at_prime x.as_ideal) :=
 { hom := stalk_to_fiber_ring_hom R x,
   inv := localization_to_stalk R x,
-  hom_inv_id' := (structure_sheaf R).1.stalk_hom_ext $ λ U hxU,
+  hom_inv_id' := (structure_sheaf R).presheaf.stalk_hom_ext $ λ U hxU,
   begin
     ext s, simp only [comp_apply], rw [id_apply, stalk_to_fiber_ring_hom_germ'],
     obtain ⟨V, hxV, iVU, f, g, hg, hs⟩ := exists_const _ _ s x hxU,
     erw [← res_apply R U V iVU s ⟨x, hxV⟩, ← hs, const_apply, localization_to_stalk_mk'],
-    refine (structure_sheaf R).1.germ_ext V hxV (hom_of_le hg) iVU _,
+    refine (structure_sheaf R).presheaf.germ_ext V hxV (hom_of_le hg) iVU _,
     erw [← hs, res_const']
   end,
   inv_hom_id' := @is_localization.ring_hom_ext R _ x.as_ideal.prime_compl
@@ -813,15 +813,15 @@ def basic_open_iso (f : R) : (structure_sheaf R).1.obj (op (basic_open f)) ≅
   CommRing.of (localization.away f) :=
 (as_iso (show CommRing.of _ ⟶ _, from to_basic_open R f)).symm
 
-instance stalk_algebra (p : prime_spectrum R) : algebra R ((structure_sheaf R).val.stalk p) :=
+instance stalk_algebra (p : prime_spectrum R) : algebra R ((structure_sheaf R).presheaf.stalk p) :=
 (to_stalk R p).to_algebra
 
 @[simp] lemma stalk_algebra_map (p : prime_spectrum R) (r : R) :
-  algebra_map R ((structure_sheaf R).val.stalk p) r = to_stalk R p r := rfl
+  algebra_map R ((structure_sheaf R).presheaf.stalk p) r = to_stalk R p r := rfl
 
 /-- Stalk of the structure sheaf at a prime p as localization of R -/
 instance is_localization.to_stalk (p : prime_spectrum R) :
-  is_localization.at_prime ((structure_sheaf R).val.stalk p) p.as_ideal :=
+  is_localization.at_prime ((structure_sheaf R).presheaf.stalk p) p.as_ideal :=
 begin
   convert (is_localization.is_localization_iff_of_ring_equiv _ (stalk_iso R p).symm
     .CommRing_iso_to_ring_equiv).mp localization.is_localization,
@@ -885,13 +885,13 @@ as_iso (to_open R ⊤)
 @[simp, reassoc, elementwise]
 lemma to_stalk_stalk_specializes {R : Type*} [comm_ring R]
   {x y : prime_spectrum R} (h : x ⤳ y) :
-  to_stalk R y ≫ (structure_sheaf R).val.stalk_specializes h = to_stalk R x :=
-by { dsimp [ to_stalk], simpa }
+  to_stalk R y ≫ (structure_sheaf R).presheaf.stalk_specializes h = to_stalk R x :=
+by { dsimp[to_stalk], simpa [-to_open_germ], }
 
 @[simp, reassoc, elementwise]
 lemma localization_to_stalk_stalk_specializes {R : Type*} [comm_ring R]
   {x y : prime_spectrum R} (h : x ⤳ y) :
-  structure_sheaf.localization_to_stalk R y ≫ (structure_sheaf R).val.stalk_specializes h =
+  structure_sheaf.localization_to_stalk R y ≫ (structure_sheaf R).presheaf.stalk_specializes h =
     CommRing.of_hom (prime_spectrum.localization_map_of_specializes h) ≫
       structure_sheaf.localization_to_stalk R x :=
 begin
@@ -907,7 +907,7 @@ end
 @[simp, reassoc, elementwise]
 lemma stalk_specializes_stalk_to_fiber {R : Type*} [comm_ring R]
   {x y : prime_spectrum R} (h : x ⤳ y) :
-  (structure_sheaf R).val.stalk_specializes h ≫ structure_sheaf.stalk_to_fiber_ring_hom R x =
+  (structure_sheaf R).presheaf.stalk_specializes h ≫ structure_sheaf.stalk_to_fiber_ring_hom R x =
     structure_sheaf.stalk_to_fiber_ring_hom R y ≫
       prime_spectrum.localization_map_of_specializes h :=
 begin

src/category_theory/sites/sheaf.lean

@@ -206,6 +206,10 @@ lemma is_sheaf.hom_ext {A : Type u₂} [category.{max v₁ u₁} A]
   e₁ = e₂ :=
 (hP _ _ S.condition).is_separated_for.ext (λ Y f hf, h ⟨Y,f,hf⟩)
 
+lemma is_sheaf_of_iso_iff {P P' : Cᵒᵖ ⥤ A} (e : P ≅ P') : is_sheaf J P ↔ is_sheaf J P' :=
+forall_congr $ λ a, ⟨presieve.is_sheaf_iso J (iso_whisker_right e _),
+  presieve.is_sheaf_iso J (iso_whisker_right e.symm _)⟩
+
 variable (J)
 
 end presheaf

src/topology/sheaves/forget.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Scott Morrison
 -/
 import category_theory.limits.preserves.shapes.products
-import topology.sheaves.sheaf
+import topology.sheaves.sheaf_condition.sites
 
 /-!
 # Checking the sheaf condition on the underlying presheaf of types.
@@ -129,6 +129,8 @@ In fact we prove a stronger version with arbitrary complete target category.
 lemma is_sheaf_iff_is_sheaf_comp :
   presheaf.is_sheaf F ↔ presheaf.is_sheaf (F ⋙ G) :=
 begin
+  rw [presheaf.is_sheaf_iff_is_sheaf_equalizer_products,
+    presheaf.is_sheaf_iff_is_sheaf_equalizer_products],
   split,
   { intros S ι U,
     -- We have that the sheaf condition fork for `F` is a limit fork,

src/topology/sheaves/functors.lean

@@ -72,7 +72,7 @@ variables [has_products.{v} C]
 The pushforward of a sheaf (by a continuous map) is a sheaf.
 -/
 theorem pushforward_sheaf_of_sheaf
-  {F : presheaf C X} (h : F.is_sheaf) : (f _* F).is_sheaf :=
+  {F : X.presheaf C} (h : F.is_sheaf) : (f _* F).is_sheaf :=
 by rw is_sheaf_iff_is_sheaf_pairwise_intersections at h ⊢;
    exact sheaf_condition_pairwise_intersections.pushforward_sheaf_of_sheaf f h
 
@@ -81,7 +81,7 @@ The pushforward functor.
 -/
 def pushforward (f : X ⟶ Y) : X.sheaf C ⥤ Y.sheaf C :=
 { obj := λ ℱ, ⟨f _* ℱ.1, pushforward_sheaf_of_sheaf f ℱ.2⟩,
-  map := λ _ _, pushforward_map f }
+  map := λ _ _ g, ⟨pushforward_map f g.1⟩ }
 
 end sheaf
 

src/topology/sheaves/limits.lean

@@ -30,10 +30,7 @@ instance [has_colimits C] (X : Top) : has_colimits_of_size.{v} (presheaf C X) :=
 limits.functor_category_has_colimits_of_size
 
 instance [has_limits C] (X : Top) : creates_limits (sheaf.forget C X) :=
-(@@creates_limits_of_nat_iso _ _
-  (presheaf.Sheaf_spaces_equiv_sheaf_sites_inverse_forget C X))
-  (@@category_theory.comp_creates_limits _ _ _ _ _ _
-    Sheaf.category_theory.Sheaf_to_presheaf.category_theory.creates_limits.{u v v})
+Sheaf.category_theory.Sheaf_to_presheaf.category_theory.creates_limits.{u v v}
 
 
 instance [has_limits C] (X : Top) : has_limits_of_size.{v} (sheaf.{v} C X) :=
@@ -42,7 +39,7 @@ has_limits_of_has_limits_creates_limits (sheaf.forget C X)
 lemma is_sheaf_of_is_limit [has_limits C] {X : Top} (F : J ⥤ presheaf.{v} C X)
   (H : ∀ j, (F.obj j).is_sheaf) {c : cone F} (hc : is_limit c) : c.X.is_sheaf :=
 begin
-  let F' : J ⥤ sheaf C X := { obj := λ j, ⟨F.obj j, H j⟩, map := F.map },
+  let F' : J ⥤ sheaf C X := { obj := λ j, ⟨F.obj j, H j⟩, map := λ X Y f, ⟨F.map f⟩ },
   let e : F' ⋙ sheaf.forget C X ≅ F := nat_iso.of_components (λ _, iso.refl _) (by tidy),
   exact presheaf.is_sheaf_of_iso ((is_limit_of_preserves (sheaf.forget C X)
       (limit.is_limit F')).cone_points_iso_of_nat_iso hc e) (limit F').2

src/topology/sheaves/local_predicate.lean

@@ -215,7 +215,7 @@ def subsheaf_to_Types (P : local_predicate T) : sheaf (Type v) X :=
 There is a canonical map from the stalk to the original fiber, given by evaluating sections.
 -/
 def stalk_to_fiber (P : local_predicate T) (x : X) :
-  (subsheaf_to_Types P).1.stalk x ⟶ T x :=
+  (subsheaf_to_Types P).presheaf.stalk x ⟶ T x :=
 begin
   refine colimit.desc _
     { X := T x, ι := { app := λ U f, _, naturality' := _ } },
@@ -224,7 +224,7 @@ begin
 end
 
 @[simp] lemma stalk_to_fiber_germ (P : local_predicate T) (U : opens X) (x : U) (f) :
-  stalk_to_fiber P x ((subsheaf_to_Types P).1.germ x f) = f.1 x :=
+  stalk_to_fiber P x ((subsheaf_to_Types P).presheaf.germ x f) = f.1 x :=
 begin
   dsimp [presheaf.germ, stalk_to_fiber],
   cases x,
@@ -243,7 +243,7 @@ lemma stalk_to_fiber_surjective (P : local_predicate T) (x : X)
 begin
   rcases w t with ⟨U, f, h, rfl⟩,
   fsplit,
-  { exact (subsheaf_to_Types P).1.germ ⟨x, U.2⟩ ⟨f, h⟩, },
+  { exact (subsheaf_to_Types P).presheaf.germ ⟨x, U.2⟩ ⟨f, h⟩, },
   { exact stalk_to_fiber_germ _ U.1 ⟨x, U.2⟩ ⟨f, h⟩, }
 end
 
@@ -261,8 +261,8 @@ begin
   -- We promise to provide all the ingredients of the proof later:
   let Q :
     ∃ (W : (open_nhds x)ᵒᵖ) (s : Π w : (unop W).1, T w) (hW : P.pred s),
-      tU = (subsheaf_to_Types P).1.germ ⟨x, (unop W).2⟩ ⟨s, hW⟩ ∧
-      tV = (subsheaf_to_Types P).1.germ ⟨x, (unop W).2⟩ ⟨s, hW⟩ := _,
+      tU = (subsheaf_to_Types P).presheaf.germ ⟨x, (unop W).2⟩ ⟨s, hW⟩ ∧
+      tV = (subsheaf_to_Types P).presheaf.germ ⟨x, (unop W).2⟩ ⟨s, hW⟩ := _,
   { choose W s hW e using Q,
     exact e.1.trans e.2.symm, },
   -- Then use induction to pick particular representatives of `tU tV : stalk x`