diff --git a/src/category_theory/concrete_category/basic.lean b/src/category_theory/concrete_category/basic.lean
index 29e9eb2079c0b..44d1596471c36 100644
--- a/src/category_theory/concrete_category/basic.lean
+++ b/src/category_theory/concrete_category/basic.lean
@@ -5,6 +5,7 @@ Authors: Scott Morrison, Johannes Hölzl, Reid Barton, Sean Leather, Yury Kudrya
 -/
 import category_theory.types
 import category_theory.functor.epi_mono
+import category_theory.limits.constructions.epi_mono
 
 /-!
 # Concrete categories
@@ -38,6 +39,8 @@ universes w v v' u
 
 namespace category_theory
 
+open category_theory.limits
+
 /--
 A concrete category is a category `C` with a fixed faithful functor `forget : C ⥤ Type`.
 
@@ -129,11 +132,37 @@ lemma concrete_category.mono_of_injective {X Y : C} (f : X ⟶ Y) (i : function.
   mono f :=
 (forget C).mono_of_mono_map ((mono_iff_injective f).2 i)
 
+lemma concrete_category.injective_of_mono_of_preserves_pullback {X Y : C} (f : X ⟶ Y) [mono f]
+  [preserves_limits_of_shape walking_cospan (forget C)] : function.injective f :=
+begin
+  haveI := category_theory.preserves_monomorphisms_of_preserves_limits_of_shape (forget C),
+  haveI : mono ((forget C).map f) := infer_instance,
+  exact (mono_iff_injective ((forget C).map f)).mp infer_instance,
+end
+
+lemma concrete_category.mono_iff_injective_of_preserves_pullback {X Y : C} (f : X ⟶ Y)
+  [preserves_limits_of_shape walking_cospan (forget C)] : mono f ↔ function.injective f :=
+⟨λ m, by resetI; exact concrete_category.injective_of_mono_of_preserves_pullback _,
+ concrete_category.mono_of_injective f⟩
+
 /-- In any concrete category, surjective morphisms are epimorphisms. -/
 lemma concrete_category.epi_of_surjective {X Y : C} (f : X ⟶ Y) (s : function.surjective f) :
   epi f :=
 (forget C).epi_of_epi_map ((epi_iff_surjective f).2 s)
 
+lemma concrete_category.surjective_of_epi_of_preserves_pushout {X Y : C} (f : X ⟶ Y) [epi f]
+  [preserves_colimits_of_shape walking_span (forget C)] : function.surjective f :=
+begin
+  haveI := category_theory.preserves_epimorphisms_of_preserves_colimits_of_shape (forget C),
+  haveI : epi ((forget C).map f) := infer_instance,
+  exact (epi_iff_surjective ((forget C).map f)).mp infer_instance
+end
+
+lemma concrete_category.epi_iff_surjective_of_preserves_pushout {X Y : C} (f : X ⟶ Y)
+  [preserves_colimits_of_shape walking_span (forget C)] : epi f ↔ function.surjective f :=
+⟨λ m, @@concrete_category.surjective_of_epi_of_preserves_pushout _ _ _ m  _,
+ concrete_category.epi_of_surjective f⟩
+
 @[simp] lemma concrete_category.has_coe_to_fun_Type {X Y : Type u} (f : X ⟶ Y) :
   coe_fn f = f :=
 rfl
diff --git a/src/category_theory/eq_to_hom.lean b/src/category_theory/eq_to_hom.lean
index c3c30dea4260a..2ab418d82eaa0 100644
--- a/src/category_theory/eq_to_hom.lean
+++ b/src/category_theory/eq_to_hom.lean
@@ -45,6 +45,16 @@ def eq_to_hom {X Y : C} (p : X = Y) : X ⟶ Y := by rw p; exact 𝟙 _
   eq_to_hom p ≫ eq_to_hom q = eq_to_hom (p.trans q) :=
 by { cases p, cases q, simp, }
 
+lemma eq_comp_eq_to_hom {X Y Y' : C} (p : Y = Y') (f : X ⟶ Y) (g : X ⟶ Y') :
+  f ≫ eq_to_hom p = g ↔ f = g ≫ eq_to_hom p.symm :=
+{ mp := λ h, h ▸ by simp,
+  mpr := λ h, by simp [eq_whisker h (eq_to_hom p)] }
+
+lemma eq_eq_to_hom_comp {X X' Y : C} (p : X = X') (f : X ⟶ Y) (g : X' ⟶ Y) :
+  eq_to_hom p ≫ g = f ↔ g = eq_to_hom p.symm ≫ f :=
+{ mp := λ h, h ▸ by simp,
+  mpr := λ h, h ▸ by simp [whisker_eq _ h] }
+
 /--
 If we (perhaps unintentionally) perform equational rewriting on
 the source object of a morphism,
diff --git a/src/category_theory/limits/shapes/products.lean b/src/category_theory/limits/shapes/products.lean
index 4bf49c165731f..4875d848ac28d 100644
--- a/src/category_theory/limits/shapes/products.lean
+++ b/src/category_theory/limits/shapes/products.lean
@@ -142,6 +142,17 @@ from a family of morphisms between the factors.
 abbreviation pi.map {f g : β → C} [has_product f] [has_product g]
   (p : Π b, f b ⟶ g b) : ∏ f ⟶ ∏ g :=
 lim_map (discrete.nat_trans (λ X, p X.as))
+
+instance pi.map_mono {f g : β → C} [has_product f] [has_product g]
+  (p : Π b, f b ⟶ g b) [Π i, mono (p i)] : mono $ pi.map p :=
+{ right_cancellation := λ c α₁ α₂ eq1,
+  begin
+    ext ⟨j⟩, dsimp,
+    have eq2 := eq_whisker eq1 (pi.π _ j),
+    rwa [category.assoc, lim_map_π, category.assoc, lim_map_π, ←category.assoc, ←category.assoc,
+      discrete.nat_trans_app, cancel_mono] at eq2,
+  end }
+
 /--
 Construct an isomorphism between categorical products (indexed by the same type)
 from a family of isomorphisms between the factors.
@@ -156,6 +167,17 @@ from a family of morphisms between the factors.
 abbreviation sigma.map {f g : β → C} [has_coproduct f] [has_coproduct g]
   (p : Π b, f b ⟶ g b) : ∐ f ⟶ ∐ g :=
 colim_map (discrete.nat_trans (λ X, p X.as))
+
+instance sigma.map_epi {f g : β → C} [has_coproduct f] [has_coproduct g]
+  (p : Π b, f b ⟶ g b) [Π i, epi (p i)] : epi $ sigma.map p :=
+{ left_cancellation := λ c α₁ α₂ eq1,
+  begin
+    ext ⟨j⟩, dsimp,
+    have eq2 := whisker_eq (sigma.ι _ j) eq1,
+    rwa [←category.assoc, ι_colim_map, ←category.assoc, ι_colim_map, discrete.nat_trans_app,
+      category.assoc, category.assoc, cancel_epi] at eq2,
+  end }
+
 /--
 Construct an isomorphism between categorical coproducts (indexed by the same type)
 from a family of isomorphisms between the factors.
diff --git a/src/category_theory/preadditive/injective.lean b/src/category_theory/preadditive/injective.lean
index 93388285bfa9f..c6121a0513034 100644
--- a/src/category_theory/preadditive/injective.lean
+++ b/src/category_theory/preadditive/injective.lean
@@ -6,6 +6,7 @@ Authors: Jujian Zhang, Kevin Buzzard
 
 import algebra.homology.exact
 import category_theory.types
+import category_theory.functor.epi_mono
 import category_theory.preadditive.projective
 import category_theory.limits.shapes.biproducts
 
diff --git a/src/topology/sheaves/godement.lean b/src/topology/sheaves/godement.lean
new file mode 100644
index 0000000000000..b1430cd6a6080
--- /dev/null
+++ b/src/topology/sheaves/godement.lean
@@ -0,0 +1,287 @@
+/-
+Copyright (c) 2022 Jujian Zhang. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Jujian Zhang
+-/
+import topology.sheaves.sheaf
+import topology.sheaves.limits
+import topology.sheaves.skyscraper
+import topology.sheaves.stalks
+import category_theory.preadditive.injective
+
+/-!
+# Godement resolution
+
+For a presheaf `𝓕 : (opens X)ᵒᵖ ⥤ C`, we can embedded `𝓕` into a sheaf `∏ₓ skyscraper(𝓕ₓ)` where
+`x` ranges over `X` and `𝓕 ⟶ ∏ₓ skyscraper(𝓕ₓ)` is mono.
+
+## Main definition
+* `godement_presheaf`: for a presheaf `𝓕`, its Godement presheaf is `∏ₓ skyscraper(𝓕ₓ)`
+* `to_godement_presheaf`: the canonical map `𝓕 ⟶ godement_presheaf 𝓕` sending `s : 𝓕(U)` to a
+  bundle of stalks `x ↦ sₓ`.
+* `godement_sheaf`: the Godement presheaf of any presheaf is a sheaf.
+* `to_godement_sheaf`: for a sheaf `𝓖`, the canonical sheaf morphism `𝓖 ⟶ godement_sheaf 𝓖.1`.
+For a sheaf `𝓖 : sheaf C X` where `C` is concrete and the forgetful functor preserves limits and
+filtered colimits
+* `mono_to_godement_sheaf`: the canonical map `𝓖 ⟶ godement_sheaf 𝓖` is mono.
+If further `C` has enough injectives
+* `sheaf_enough_inj_aux.injective_sheaf`: since each `𝓕ₓ` can be embedded into `𝓕ₓ ⟶ I(x)` via a
+  monomorphism, `𝓖` can be embedded into `∏ₓ skyscraper(I(x))`.
+* `sheaf_enough_inj_aux.injective_J`: `∏ₓ skyscraper(I(x))` is injective.
+* `sheaf_enough_inj_aux.to_J_mono`: the canonical map `𝓖 ⟶ ∏ₓ skyscraper(I(x))` is mono.
+* `sheaf_has_enough_injectives`: the category of sheaves on `X` in `C` has enough injectives.
+-/
+
+
+noncomputable theory
+
+section presheaf
+
+open Top
+open topological_space
+open category_theory
+open category_theory.limits
+
+universes u v
+
+variables {X : Top.{u}} {C : Type u} [category.{u} C]
+variables [has_limits C] [has_terminal C] [has_colimits C]
+variables [Π (x : X) (U : opens X), decidable (x ∈ U)]
+variables (𝓕 : presheaf C X) (𝓖 : sheaf C X)
+
+def godement_presheaf : presheaf C X :=
+∏ (λ x, skyscraper_presheaf x (𝓕.stalk x) : X → presheaf C X)
+
+@[simps] def godement_presheaf_obj (U : (opens X)ᵒᵖ) :
+  (godement_presheaf 𝓕).obj U ≅ ∏ (λ x, (skyscraper_presheaf x (𝓕.stalk x)).obj U) :=
+limit_obj_iso_limit_comp_evaluation _ _ ≪≫
+{ hom := lim_map
+  { app := λ _, 𝟙 _,
+    naturality' := by { rintros ⟨x⟩ ⟨y⟩ ⟨⟨(rfl : x = y)⟩⟩, refl } },
+  inv := lim_map
+  { app := λ _, 𝟙 _,
+    naturality' := by { rintros ⟨x⟩ ⟨y⟩ ⟨⟨(rfl : x = y)⟩⟩, refl } },
+  hom_inv_id' :=
+  begin
+    dsimp,
+    ext,
+    erw [category.assoc, lim_map_π, ←category.assoc, lim_map_π, category.id_comp, category.comp_id,
+      category.comp_id],
+  end,
+  inv_hom_id' :=
+  begin
+    dsimp,
+    ext,
+    erw [category.assoc, lim_map_π, ←category.assoc, lim_map_π, category.comp_id, category.id_comp,
+      category.comp_id],
+  end }
+
+@[reducible]
+def to_godement_presheaf_aux (U : (opens X)ᵒᵖ) :
+  𝓕.obj U ⟶ ∏ λ (x : X), ite (x ∈ opposite.unop U) (𝓕.stalk x) (⊤_ C) :=
+pi.lift (λ x, if m : x ∈ U.unop
+  then 𝓕.germ ⟨x, m⟩ ≫ eq_to_hom ((skyscraper_presheaf_obj_of_mem _ m).symm.trans (by congr) :
+    𝓕.stalk (⟨x, m⟩ : U.unop) = (skyscraper_presheaf x (𝓕.stalk x)).obj U)
+  else terminal.from _ ≫ eq_to_hom (skyscraper_presheaf_obj_of_not_mem _ m).symm)
+
+@[reducible]
+def to_godement_presheaf_aux_comp_π {U : (opens X)ᵒᵖ} (p : U.unop) :
+  𝓕.obj U ⟶ 𝓕.stalk p :=
+to_godement_presheaf_aux 𝓕 U ≫ pi.π _ p ≫ eq_to_hom (if_pos p.2)
+
+lemma to_godement_presheaf_aux_comp_π_eq {U : (opens X)ᵒᵖ} (p : U.unop) :
+  to_godement_presheaf_aux_comp_π 𝓕 p = presheaf.germ 𝓕 p :=
+begin
+  dunfold to_godement_presheaf_aux_comp_π presheaf.germ to_godement_presheaf_aux,
+  rw [←category.assoc, limit.lift_π],
+  simp only [fan.mk_π_app],
+  split_ifs,
+  { rw [category.assoc, eq_to_hom_trans, eq_to_hom_refl, category.comp_id],
+    refl },
+  { exfalso, exact h p.2, },
+end
+
+@[simps] def to_godement_presheaf : 𝓕 ⟶ godement_presheaf 𝓕 :=
+{ app := λ U, to_godement_presheaf_aux 𝓕 U ≫ (godement_presheaf_obj 𝓕 U).inv,
+  naturality' :=
+  begin
+    intros U V inc,
+    ext ⟨x⟩,
+    dsimp,
+    simp only [category.assoc, limit_obj_iso_limit_comp_evaluation_inv_π_app, lim_map_π,
+      category.comp_id, nat_trans.naturality],
+    simp only [←category.assoc _ _ ((skyscraper_presheaf _ _).map inc),
+      limit_obj_iso_limit_comp_evaluation_inv_π_app, lim_map_π, category.comp_id],
+    simp only [limit.lift_π, fan.mk_π_app, skyscraper_presheaf_map, category.id_comp,
+      eq_to_hom_trans, comp_dite],
+    dsimp,
+    split_ifs with hV,
+    { have hU : x ∈ U.unop := (le_of_hom inc.unop) hV,
+      split_ifs,
+      erw [category.assoc, eq_to_hom_trans, ←category.assoc, eq_comp_eq_to_hom,
+        category.assoc, eq_to_hom_trans, eq_to_hom_refl, category.comp_id, 𝓕.germ_res inc.unop],
+      refl },
+    { rw [←category.assoc, eq_comp_eq_to_hom, category.assoc, category.assoc, eq_to_hom_trans,
+        eq_to_hom_refl, category.comp_id],
+      exact terminal_is_terminal.hom_ext _ _ },
+  end }
+
+lemma godement_presheaf_is_sheaf (h : 𝓕.is_sheaf) : (godement_presheaf 𝓕).is_sheaf :=
+limit_is_sheaf _ $ λ ⟨x⟩, (skyscraper_sheaf x _).2
+
+def godement_sheaf : sheaf C X :=
+⟨godement_presheaf 𝓖.1, godement_presheaf_is_sheaf _ 𝓖.2⟩
+
+def godement_sheaf_obj (U : (opens X)ᵒᵖ) :
+  (godement_sheaf 𝓖).1.obj U ≅ ∏ (λ x, (skyscraper_presheaf x (𝓖.presheaf.stalk x)).obj U) :=
+godement_presheaf_obj 𝓖.1 U
+
+def to_godement_sheaf : 𝓖 ⟶ godement_sheaf 𝓖 :=
+⟨to_godement_presheaf 𝓖.1⟩
+
+variables [concrete_category.{u} C] [preserves_limits (forget C)]
+variables [reflects_isomorphisms (forget C)] [preserves_filtered_colimits (forget C)]
+
+@[simps] def sheaf_in_Type : sheaf C X ⥤ sheaf (Type u) X :=
+{ obj := λ F, ⟨F.1 ⋙ forget C, (presheaf.is_sheaf_iff_is_sheaf_comp (forget C) F.1).mp F.2⟩,
+  map := λ F G f, Sheaf.hom.mk
+  { app := λ U, (forget C).map (f.1.app U),
+    naturality' := λ U V inc, by erw [←(forget C).map_comp, ←(forget C).map_comp, f.1.naturality] },
+  map_id' := λ F, by { ext, dsimp, rw [id_apply] },
+  map_comp' := λ F G H f g, by { ext, dsimp, rw [comp_apply] } }
+
+def stalk_bundles_eq0 (U : (opens X)ᵒᵖ) (x y : (sheaf_in_Type.obj 𝓖).1.obj U)
+  (eq1 : (sheaf_in_Type.map (to_godement_sheaf 𝓖)).val.app U x =
+      (sheaf_in_Type.map (to_godement_sheaf 𝓖)).val.app U y) (p : U.unop) :
+  (forget C).map (to_godement_presheaf_aux 𝓖.presheaf U) x =
+  (forget C).map (to_godement_presheaf_aux 𝓖.presheaf U) y :=
+begin
+  change (forget C).map ((to_godement_presheaf 𝓖.presheaf).app _) x =
+    (forget C).map ((to_godement_presheaf 𝓖.presheaf).app _) y at eq1,
+  dsimp at eq1,
+  change (forget C).map _ x = (forget C).map _ y at eq1,
+  have eq2 := congr_arg ((forget C).map (limit_obj_iso_limit_comp_evaluation (discrete.functor _) U).hom) eq1,
+  dsimp at eq2,
+  erw [←comp_apply, ←comp_apply, ←category.assoc] at eq2,
+  simp only [category.assoc, iso.inv_hom_id, category.comp_id] at eq2,
+  set α : nat_trans (discrete.functor (λ (x : ↥X), ite (x ∈ opposite.unop U) (𝓖.presheaf.stalk x) (⊤_ C)))
+  (discrete.functor (λ (x : ↥X), skyscraper_presheaf x (𝓖.presheaf.stalk x)) ⋙
+     (evaluation (opens ↥X)ᵒᵖ C).obj U) := _,
+  change (forget C).map (_ ≫ lim_map α) x = (forget C).map (_ ≫ lim_map α) y at eq2,
+  haveI : is_iso (lim_map α),
+  { refine is_iso.mk ⟨lim_map { app := λ x, 𝟙 _, naturality' := _ }, _, _⟩,
+    { rintros ⟨x⟩ ⟨y⟩ ⟨⟨eq0 : x = y⟩⟩, subst eq0, refl},
+    { ext1, simp only [category.assoc, lim_map_π, category.comp_id, category.id_comp], },
+    { ext1, simp only [category.assoc, lim_map_π, category.comp_id, category.id_comp], }, },
+  have eq3 := congr_arg ((forget C).map (inv (lim_map α))) eq2,
+  change ((forget C).map _ ≫ (forget C).map _) _ = ((forget C).map _ ≫ (forget C).map _) _ at eq3,
+  simpa only [←(forget C).map_comp, category.assoc, is_iso.hom_inv_id,category.comp_id] using eq3,
+end
+
+def stalk_bundles_eq (U : (opens X)ᵒᵖ) (x y : (sheaf_in_Type.obj 𝓖).1.obj U)
+  (eq1 : (sheaf_in_Type.map (to_godement_sheaf 𝓖)).val.app U x =
+      (sheaf_in_Type.map (to_godement_sheaf 𝓖)).val.app U y) (p : U.unop) :
+  (forget C).map (𝓖.presheaf.germ p) x = (forget C).map (𝓖.presheaf.germ p) y :=
+begin
+  have eq1' := stalk_bundles_eq0 𝓖 U x y eq1 p,
+  have eq1'' : (forget C).map (to_godement_presheaf_aux_comp_π 𝓖.presheaf p) x =
+    (forget C).map (to_godement_presheaf_aux_comp_π 𝓖.presheaf p) y,
+  { dsimp at eq1' ⊢,
+    dunfold to_godement_presheaf_aux_comp_π,
+    simp only [comp_apply, eq1'], },
+  rwa to_godement_presheaf_aux_comp_π_eq at eq1'',
+end
+
+example : true := trivial
+
+instance mono_to_godement_sheaf : mono $ to_godement_sheaf 𝓖 :=
+begin
+  rw presheaf.mono_iff_stalk_mono,
+  intros x,
+  change mono ((presheaf.stalk_functor C x).map (to_godement_presheaf 𝓖.1)),
+  rw concrete_category.mono_iff_injective_of_preserves_pullback,
+  exact (presheaf.app_injective_iff_stalk_functor_map_injective (to_godement_presheaf 𝓖.1)).mpr
+    (λ U x y H, presheaf.section_ext _ _ _ _ (λ p, stalk_bundles_eq 𝓖 (opposite.op U) x y H p)) x,
+end
+
+section enough_injectives
+
+variables [enough_injectives C]
+
+namespace sheaf_enough_inj_aux
+
+def injective_sheaf : sheaf C X :=
+⟨∏ (λ x, skyscraper_presheaf x (injective.under $ 𝓕.stalk x) : X → presheaf C X),
+ limit_is_sheaf _ $ λ ⟨x⟩, (skyscraper_sheaf x _).2⟩
+
+def injective_sheaf_iso :
+  injective_sheaf 𝓖.1 ≅
+  ∏ (λ x, skyscraper_sheaf x (injective.under $ 𝓖.presheaf.stalk x)) :=
+{ hom := Sheaf.hom.mk $ eq_to_hom begin
+    change limit _ = limit _, congr, apply category_theory.functor.ext,
+    { rintros ⟨p⟩ ⟨q⟩ ⟨⟨(eq1 : p = q)⟩⟩, subst eq1,
+      rw [eq_to_hom_refl, category.id_comp, eq_to_hom_refl, category.comp_id], refl, },
+    { rintros ⟨p⟩, dsimp, refl, },
+  end ≫ (preserves_limit_iso (sheaf.forget C X) _).inv,
+  inv := Sheaf.hom.mk $ (preserves_limit_iso (sheaf.forget C X) _).hom ≫ eq_to_hom begin
+    change limit _ = limit _, congr, apply category_theory.functor.ext,
+    { rintros ⟨p⟩ ⟨q⟩ ⟨⟨(eq1 : p = q)⟩⟩, subst eq1,
+      rw [eq_to_hom_refl, category.id_comp, eq_to_hom_refl, category.comp_id], refl, },
+    { rintros ⟨p⟩, dsimp, refl, },
+  end,
+  hom_inv_id' :=
+  begin
+    ext ⟨p⟩ U, dsimp,
+    rw [←category.assoc, category.assoc _ _ ((preserves_limit_iso (sheaf.forget C X) _).hom.app U),
+      iso.inv_hom_id_app, category.comp_id, category.id_comp, ←nat_trans.comp_app, eq_to_hom_trans,
+      eq_to_hom_refl],
+    convert category.id_comp _,
+  end,
+  inv_hom_id' :=
+  begin
+    ext ⟨p⟩ U, dsimp,
+    rw [←category.assoc, category.assoc _ _ (eq_to_hom _), eq_to_hom_trans, eq_to_hom_refl,
+      category.comp_id, iso.hom_inv_id],
+  end }
+
+local notation `J` := injective_sheaf 𝓖.1
+
+instance injective_J : injective J :=
+injective.of_iso (injective_sheaf_iso 𝓖).symm $
+@@injective.category_theory.limits.pi_obj.injective _ _ _ $ λ p,
+(skyscraper_sheaf_injective p _ : injective
+  (skyscraper_sheaf p (injective.under (𝓖.presheaf.stalk p))))
+
+def to_J : 𝓖 ⟶ J :=
+Sheaf.hom.mk $ to_godement_presheaf _ ≫
+  pi.map (λ p, (skyscraper_presheaf_functor p).map $ injective.ι _)
+
+instance mono_to_J : mono (to_J 𝓖) :=
+(Sheaf.hom.mono_iff_presheaf_mono _ _ _).mpr
+begin
+  haveI t1 : mono (to_godement_sheaf 𝓖) := infer_instance,
+  rw Sheaf.hom.mono_iff_presheaf_mono at t1,
+  change mono (to_godement_presheaf 𝓖.1) at t1,
+  resetI,
+  have t21 : ∀ (p : X), mono ((skyscraper_presheaf_functor p).map
+    (injective.ι (presheaf.stalk 𝓖.val p))),
+  { exact λ p, @@functor.map_mono _ _ (skyscraper_presheaf_functor p)
+      (functor.preserves_monomorphisms_of_adjunction (stalk_skyscraper_presheaf_adj p))
+      (injective.ι (presheaf.stalk 𝓖.val p)) _, },
+  haveI t22 : mono (pi.map (λ p, (skyscraper_presheaf_functor p).map
+    (injective.ι (presheaf.stalk 𝓖.val p)))) := @pi.map_mono _ _ _ _ _ _ _ _ t21,
+  apply mono_comp,
+end
+
+end sheaf_enough_inj_aux
+
+instance sheaf_has_enough_injectives : enough_injectives (sheaf C X) :=
+{ presentation := λ 𝓖, nonempty.intro
+  { J := sheaf_enough_inj_aux.injective_sheaf 𝓖.1,
+    injective := sheaf_enough_inj_aux.injective_J _,
+    f := sheaf_enough_inj_aux.to_J _,
+    mono := sheaf_enough_inj_aux.mono_to_J 𝓖 } }
+
+end enough_injectives
+
+end presheaf
diff --git a/src/topology/sheaves/skyscraper.lean b/src/topology/sheaves/skyscraper.lean
new file mode 100644
index 0000000000000..9bfe0407f2064
--- /dev/null
+++ b/src/topology/sheaves/skyscraper.lean
@@ -0,0 +1,901 @@
+/-
+Copyright (c) 2022 Jujian Zhang. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Jujian Zhang
+-/
+import algebraic_geometry.sheafed_space
+import topology.sheaves.sheaf_condition.unique_gluing
+import topology.sheaves.stalks
+import category_theory.sites.sheafification
+import category_theory.preadditive.injective
+
+/-!
+# Skyscraper (pre)sheaves
+
+A skyscraper (pre)sheaf is a (pre)sheaf supported at a single point: if `p₀ ∈ X` is a specified
+point, then the skyscraper (pre)sheaf `𝓕` with value `A` is defined by `U ↦ A` if `p₀ ∈ U` and
+`U ↦ *` if `p₀ ∉ A` where `*` is some terminal object.
+
+## Main definitions
+
+* `skyscraper_presheaf`:  `skyscraper_presheaf p₀ A` is the skyscraper presheaf at point `p₀` with
+  value `A`.
+* `skyscraper_sheaf`: the skyscraper presheaf satisfies the sheaf condition.
+
+## Main statements
+
+* `skyscraper_stalk_of_mem_closure₀`: if `y ∈ closure {p₀}` then the stalk of
+  `skyscraper_presheaf p₀ S` at `y` is `S`.
+* `skyscraper_stalk_of_not_mem_closure₀`: if `y ∉ closure {p₀}` then the stalk of
+  `skyscraper_presheaf p₀ S` at `y` is `*` the terminal object.
+
+-/
+
+noncomputable theory
+
+section
+
+open topological_space
+open category_theory category_theory.limits
+open Top
+open opposite
+
+universes u v w
+
+variables {X : Top.{u}} (p₀ : X) {C : Type v} [category.{w} C] (S : C)
+variables [has_terminal C] [Π (U : opens X), decidable (p₀ ∈ U)]
+
+/--
+A skyscraper presheaf is a presheaf supported at a single point: if `p₀ ∈ X` is a specified
+point, then the skyscraper presheaf `𝓕` with value `A` is defined by `U ↦ A` if `p₀ ∈ U` and
+`U ↦ *` if `p₀ ∉ A` where `*` is some terminal object.
+-/
+@[simps] def skyscraper_presheaf : presheaf C X :=
+{ obj := λ U, ite (p₀ ∈ unop U) S (terminal C),
+  map := λ U V i, dite (p₀ ∈ unop V)
+    (λ h, eq_to_hom (if_pos (le_of_hom i.unop h)) ≫ 𝟙 S ≫ eq_to_hom (if_pos h).symm)
+    (λ h, terminal.from _ ≫ eq_to_hom (if_neg h).symm),
+  map_id' := λ U,
+  begin
+    split_ifs,
+    { simp, },
+    { simpa only [eq_comp_eq_to_hom] using terminal_is_terminal.hom_ext _ _, },
+  end,
+  map_comp' := λ U V W iVU iWV,
+  begin
+    by_cases hW : p₀ ∈ unop W,
+    { have hV : p₀ ∈ unop V := le_of_hom iWV.unop hW,
+      have hU : p₀ ∈ unop U := le_of_hom iVU.unop hV,
+      split_ifs,
+      simp },
+    { split_ifs;
+      simpa only [eq_comp_eq_to_hom] using terminal_is_terminal.hom_ext _ _, }
+  end }
+
+@[simps] def skyscraper_presheaf' {c : C} (it : is_terminal c) : presheaf C X :=
+{ obj := λ U, ite (p₀ ∈ unop U) S c,
+  map := λ U V i, dite (p₀ ∈ unop V)
+    (λ h, eq_to_hom (if_pos (le_of_hom i.unop h)) ≫ 𝟙 S ≫ eq_to_hom (if_pos h).symm)
+    (λ h, it.from _ ≫ eq_to_hom (if_neg h).symm),
+  map_id' := λ U,
+  begin
+    split_ifs,
+    { simp, },
+    { simpa only [eq_comp_eq_to_hom] using it.hom_ext _ _, },
+  end,
+  map_comp' := λ U V W iVU iWV,
+  begin
+    by_cases hW : p₀ ∈ unop W,
+    { have hV : p₀ ∈ unop V := le_of_hom iWV.unop hW,
+      have hU : p₀ ∈ unop U := le_of_hom iVU.unop hV,
+      split_ifs,
+      simp },
+    { split_ifs;
+      simpa only [eq_comp_eq_to_hom] using it.hom_ext _ _, }
+  end }
+
+def skyscraper_presheaf_iso {c : C} (it : is_terminal c) :
+  (skyscraper_presheaf p₀ S) ≅ (skyscraper_presheaf' p₀ S it) :=
+nat_iso.of_components
+  (λ U, iso.mk
+    (if m : p₀ ∈ U.unop
+      then eq_to_hom (by simp [if_pos m])
+      else it.from _ ≫ eq_to_hom (by simp [if_neg m]))
+    (if m : p₀ ∈ U.unop
+      then eq_to_hom (by simp [if_pos m])
+      else terminal.from _ ≫ eq_to_hom (by simp [if_neg m]))
+    begin
+      dsimp,
+      split_ifs,
+      { rw [eq_to_hom_trans, eq_to_hom_refl], },
+      { rw [←category.assoc, eq_comp_eq_to_hom],
+        exact terminal_is_terminal.hom_ext _ _, }
+    end
+    begin
+      dsimp,
+      split_ifs,
+      { rw [eq_to_hom_trans, eq_to_hom_refl], },
+      { rw [←category.assoc, eq_comp_eq_to_hom],
+        exact it.hom_ext _ _, }
+    end) $ λ U V inc,
+  begin
+    dsimp,
+    by_cases hV : p₀ ∈ V.unop,
+    { have hU : p₀ ∈ U.unop := le_of_hom inc.unop hV,
+      split_ifs,
+      simp only [category.id_comp, eq_to_hom_trans, eq_to_hom_refl], },
+    { split_ifs;
+      rw [←category.assoc, eq_comp_eq_to_hom];
+      exact it.hom_ext _ _, },
+  end
+
+section
+
+variables {p₀}
+
+lemma skyscraper_presheaf_obj_of_mem {U : opens X} (h : p₀ ∈ U) :
+  (skyscraper_presheaf p₀ S).obj (op U) = S := if_pos h
+
+lemma skyscraper_presheaf_obj_of_not_mem {U : opens X} (h : p₀ ∉ U) :
+  (skyscraper_presheaf p₀ S).obj (op U) = terminal C := if_neg h
+
+end
+
+/--
+A skyscraper sheaf is a sheaf supported at a single point: if `p₀ ∈ X` is a specified
+point, then the skyscraper sheaf `𝓕` with value `A` is defined by `U ↦ A` if `p₀ ∈ U` and
+`U ↦ *` if `p₀ ∉ A` where `*` is some terminal object.
+-/
+def skyscraper_sheaf : sheaf C X :=
+⟨skyscraper_presheaf p₀ S, λ c U s hs x hx,
+  ⟨dite (p₀ ∈ U)
+    (λ h, x (hs p₀ h).some_spec.some (hs p₀ h).some_spec.some_spec.1 ≫
+        eq_to_hom ((skyscraper_presheaf_obj_of_mem S (hs p₀ h).some_spec.some_spec.2).trans
+          (skyscraper_presheaf_obj_of_mem S h).symm))
+    (λ h, terminal.from c ≫ (eq_to_hom (skyscraper_presheaf_obj_of_not_mem S h).symm)),
+    λ V inc h,
+    begin
+      by_cases hV : p₀ ∈ V,
+      { have hU : p₀ ∈ U := le_of_hom inc hV,
+        split_ifs,
+        generalize_proofs h₁ h₂ h₃ h₄,
+        dsimp,
+        split_ifs,
+        rw [category.id_comp, eq_to_hom_trans, category.assoc, eq_to_hom_trans],
+        generalize_proofs h₅,
+        have := hx (hom_of_le inf_le_left) (hom_of_le inf_le_right) h₂.some_spec.1 h rfl,
+        dsimp at this,
+        have hV' : p₀ ∈ h₁.some ⊓ V := ⟨h₂.some_spec.2, hV⟩,
+        split_ifs at this;
+        rw [category.id_comp, eq_to_hom_trans, eq_to_hom_trans, eq_comp_eq_to_hom,
+          category.assoc, eq_to_hom_trans] at this;
+        generalize_proofs h₆ at this;
+        rw [this, category.assoc, eq_to_hom_trans, eq_to_hom_refl, category.comp_id] },
+      { dsimp,
+        split_ifs,
+        rw [←category.assoc, eq_comp_eq_to_hom],
+        exact terminal_is_terminal.hom_ext _ _, }
+    end,
+    λ y (hy : x.is_amalgamation y),
+    begin
+      split_ifs,
+      { generalize_proofs h₁ h₂ h₃ h₄,
+        have := hy h₂.some h₂.some_spec.1,
+        dsimp at this,
+        split_ifs at this with H,
+        { rw [category.id_comp, eq_to_hom_trans, eq_comp_eq_to_hom] at this,
+          rw [this, eq_comp_eq_to_hom, category.assoc, eq_to_hom_trans, eq_to_hom_refl,
+            category.comp_id], },
+        { exfalso,
+          exact H h₂.some_spec.2, }, },
+      { rw [←eq_comp_eq_to_hom],
+        exact terminal_is_terminal.hom_ext _ _, }
+    end⟩⟩
+
+def skyscraper_sheaf' {c : C} (it : is_terminal c) : sheaf C X :=
+⟨skyscraper_presheaf' p₀ S it,
+ (presheaf.is_sheaf_iso_iff (skyscraper_presheaf_iso p₀ S it)).mp (skyscraper_sheaf p₀ S).2⟩
+
+def skyscraper_sheaf_iso {c : C} (it : is_terminal c) :
+  skyscraper_sheaf p₀ S ≅ skyscraper_sheaf' p₀ S it :=
+{ hom := Sheaf.hom.mk (skyscraper_presheaf_iso p₀ S it).hom,
+  inv := Sheaf.hom.mk (skyscraper_presheaf_iso p₀ S it).inv,
+  hom_inv_id' := by { ext, dsimp, simp only [iso.hom_inv_id_app] },
+  inv_hom_id' := by { ext, dsimp, simp only [iso.inv_hom_id_app] } }
+
+end
+
+section
+
+-- In this section, we calculate the stalks for skyscraper presheaves.
+-- We need to restrict universe level.
+
+open topological_space
+open category_theory category_theory.limits
+open Top
+open opposite
+
+universes u v
+
+variables {X : Top.{u}} (p₀ : X) {C : Type v} [category.{u} C] (S : C) [has_terminal C]
+
+lemma mem_nhds_of_not_mem_closure_singleton {y : X} (h : ¬p₀ ⤳ y) :
+  ∃ (U : open_nhds y), p₀ ∉ U.1 :=
+begin
+  have := (not_iff_not.mpr specializes_iff_forall_open).mp h,
+  push_neg at this,
+  rcases this with ⟨s, o, h₁, h₂⟩,
+  exact ⟨⟨⟨s, o⟩, h₁⟩, h₂⟩,
+end
+
+variable [Π (U : opens X), decidable (p₀ ∈ U)]
+/--
+The cocone at `S` for the salk functor of `skyscraper_presheaf p₀ S` when `y ∈ closure {p₀}`
+-/
+@[simps] def skyscraper_presheaf_cocone_of_mem_closure₀ {y : X} (h : p₀ ⤳ y) :
+  cocone ((open_nhds.inclusion y).op ⋙ skyscraper_presheaf p₀ S) :=
+{ X := S,
+  ι :=
+  { app := λ U, eq_to_hom $ if_pos (h.mem_open U.unop.1.2 U.unop.2),
+    naturality' := λ U V inc,
+    begin
+      simp only [functor.op_obj, unop_op, functor.comp_map, functor.op_map, skyscraper_presheaf_map,
+        category.id_comp, eq_to_hom_trans, functor.const_obj_map, category.assoc],
+      by_cases hV : p₀ ∈ (open_nhds.inclusion y).obj V.unop,
+      { have hU : p₀ ∈ unop ((open_nhds.inclusion y).op.obj U) := le_of_hom inc.unop hV,
+        split_ifs,
+        erw [eq_to_hom_trans, category.comp_id],
+        refl },
+      { split_ifs with hU;
+        erw [category.comp_id, category.assoc, eq_to_hom_trans, eq_comp_eq_to_hom, eq_to_hom_trans];
+        exact terminal_is_terminal.hom_ext _ _, },
+    end } }
+
+/--
+The canonical map `S ⟶ (skyscraper_presheaf p₀ S t).stalk y` when `y ∈ closure {p₀}`
+-/
+noncomputable def skyscraper_presheaf_from [has_colimits C] {y : X} :
+  S ⟶ (skyscraper_presheaf p₀ S).stalk y :=
+eq_to_hom (skyscraper_presheaf_obj_of_mem S (by tauto : p₀ ∈ ⊤)).symm ≫
+  (skyscraper_presheaf p₀ S).germ (⟨y, trivial⟩ : (⊤ : opens X))
+
+/--
+The cocone at `S` for the salk functor of `skyscraper_presheaf p₀ S` when `y ∈ closure {p₀}` is a
+colimit
+-/
+noncomputable def skyscraper_presheaf_cocone_of_mem_closure₀_is_colimit [has_colimits C]
+  {y : X} (h : p₀ ⤳ y) : is_colimit (skyscraper_presheaf_cocone_of_mem_closure₀ p₀ S h) :=
+{ desc := λ c, (skyscraper_presheaf_from p₀ S ≫ colimit.desc _ _ : S ⟶ c.X),
+  fac' := λ c U,
+  begin
+    dsimp,
+    simp only [skyscraper_presheaf_from, presheaf.germ, category.comp_id,
+      category.assoc, colimit.ι_desc, eq_to_hom_trans_assoc],
+    have := c.ι.naturality (hom_of_le $ (le_top : unop U ≤ _)).op,
+    dsimp at this,
+    have h' : p₀ ∈ (open_nhds.inclusion y).obj (unop U) := h.mem_open U.unop.1.2 U.unop.2,
+    have h'' : p₀ ∈ (open_nhds.inclusion y).obj ⊤ := trivial,
+    split_ifs at this,
+    rw [category.comp_id, category.id_comp, eq_to_hom_trans, eq_eq_to_hom_comp] at this,
+    rw [this, eq_eq_to_hom_comp, ←category.assoc, eq_to_hom_trans, eq_to_hom_refl,
+      category.id_comp],
+    congr,
+  end,
+  uniq' := λ c f h,
+  begin
+    simp only [skyscraper_presheaf_from, presheaf.germ, category.assoc],
+    erw [colimit.ι_desc],
+    specialize h (op ⟨⊤, trivial⟩),
+    erw [←h],
+    simp only [skyscraper_presheaf_cocone_of_mem_closure₀_ι_app, category.assoc,
+      eq_to_hom_trans_assoc, eq_to_hom_refl, category.id_comp],
+  end }
+
+/--
+If `y ∈ closure {p₀}`, then the stalk of `skyscraper_presheaf p₀ S` at `y` is `S`
+-/
+@[reducible]
+noncomputable def skyscraper_presheaf_stalk_of_mem_closure₀ [has_colimits C]
+  {y : X} (h : p₀ ⤳ y) : (skyscraper_presheaf p₀ S).stalk y ≅ S :=
+colimit.iso_colimit_cocone ⟨_, (skyscraper_presheaf_cocone_of_mem_closure₀_is_colimit p₀ S h)⟩
+
+/--
+The cocone at `*` for the salk functor of `skyscraper_presheaf p₀ S` when `y ∉ closure {p₀}`
+-/
+@[simps] def skyscraper_presheaf_cocone {y : X} :
+  cocone ((open_nhds.inclusion y).op ⋙ skyscraper_presheaf p₀ S) :=
+{ X := terminal C,
+  ι :=
+  { app := λ U, terminal.from _,
+    naturality' := λ U V inc, terminal_is_terminal.hom_ext _ _ } }
+
+/--
+The canonical map `* ⟶ (skyscraper_presheaf p₀ S).stalk y` when `y ∉ closure {p₀}`
+-/
+noncomputable def skyscraper_presheaf_of_not_mem_closure₀_from [has_colimits C]
+  {y : X} (h : ¬p₀ ⤳ y) : terminal C ⟶ (skyscraper_presheaf p₀ S).stalk y :=
+eq_to_hom (skyscraper_presheaf_obj_of_not_mem S $
+  (mem_nhds_of_not_mem_closure_singleton p₀ h).some_spec).symm ≫
+  (skyscraper_presheaf p₀ S).germ (⟨y, (mem_nhds_of_not_mem_closure_singleton p₀ h).some.2⟩ :
+    (mem_nhds_of_not_mem_closure_singleton p₀ h).some.1)
+
+/--
+The cocone at `*` for the salk functor of `skyscraper_presheaf p₀ S` when `y ∉ closure {p₀}` is a
+colimit
+-/
+noncomputable def skyscraper_presheaf_cocone_of_not_mem_closure₀_is_colimit [has_colimits C]
+  {y : X} (h : ¬p₀ ⤳ y) : is_colimit (skyscraper_presheaf_cocone p₀ S) :=
+{ desc := λ c, (eq_to_hom ((skyscraper_presheaf_obj_of_not_mem _
+      (mem_nhds_of_not_mem_closure_singleton p₀ h).some_spec).symm)) ≫
+    presheaf.germ (skyscraper_presheaf p₀ S)
+      ⟨y, (mem_nhds_of_not_mem_closure_singleton p₀ h).some.2⟩ ≫ colimit.desc _ _,
+  fac' := λ c U,
+  begin
+    simp only [presheaf.germ, skyscraper_presheaf_cocone_ι_app],
+    erw [colimit.ι_desc],
+    dsimp,
+    by_cases h' : p₀ ∈ (open_nhds.inclusion y).obj (unop U),
+    { have eq1 : terminal.from (ite (p₀ ∈ (open_nhds.inclusion y).obj (unop U)) S (terminal C)) =
+          eq_to_hom (if_pos h') ≫ terminal.from _ := terminal_is_terminal.hom_ext _ _,
+      rw [eq1, category.assoc, eq_eq_to_hom_comp],
+      have := c.ι.naturality (hom_of_le (le_top : U.unop ≤ ⊤)).op,
+      dsimp at this,
+      have h'' : p₀ ∈ (open_nhds.inclusion y).obj ⊤ := trivial,
+      split_ifs at this,
+      rw [category.comp_id, category.id_comp, eq_to_hom_trans, eq_eq_to_hom_comp] at this,
+      rw [this, ←category.assoc _ _ (c.ι.app (op ⊤)), eq_to_hom_trans],
+      clear this,
+      have := c.ι.naturality
+        (hom_of_le (le_top : (mem_nhds_of_not_mem_closure_singleton p₀ h).some ≤ ⊤)).op,
+      dsimp at this,
+      have h''' : p₀ ∉ (mem_nhds_of_not_mem_closure_singleton p₀ h).some.1 :=
+        (mem_nhds_of_not_mem_closure_singleton p₀ h).some_spec,
+      split_ifs at this,
+      have eq2 : terminal.from (ite (p₀ ∈ (open_nhds.inclusion y).obj ⊤) S (terminal C)) =
+        eq_to_hom (if_pos h'') ≫ terminal.from _ := terminal_is_terminal.hom_ext _ _,
+      rw [category.comp_id, eq2, category.assoc, category.assoc] at this,
+      simp only [←this, ←category.assoc],
+      convert eq_whisker _ _,
+      { ext, refl, },
+      { rw [eq_comp_eq_to_hom],
+        exact terminal_is_terminal.hom_ext _ _ } },
+    { have eq1 : terminal.from (ite (p₀ ∈ (open_nhds.inclusion y).obj (unop U)) S (terminal C)) =
+        eq_to_hom (if_neg h') := terminal_is_terminal.hom_ext _ _,
+      have eq2 : terminal.from (ite (p₀ ∈ (open_nhds.inclusion y).obj ⊤) S (terminal C)) =
+        eq_to_hom (if_pos trivial) ≫ terminal.from _ := terminal_is_terminal.hom_ext _ _,
+      have eq3 : terminal.from (ite (p₀ ∈ (open_nhds.inclusion y).obj
+          (mem_nhds_of_not_mem_closure_singleton p₀ h).some) S (terminal C)) =
+        eq_to_hom (if_neg (mem_nhds_of_not_mem_closure_singleton p₀ h).some_spec):=
+      terminal_is_terminal.hom_ext _ _,
+      rw [eq1, ←category.assoc, eq_to_hom_trans],
+      have := c.ι.naturality (hom_of_le (inf_le_left :
+          (mem_nhds_of_not_mem_closure_singleton p₀ h).some ⊓ unop U ≤
+          (mem_nhds_of_not_mem_closure_singleton p₀ h).some)).op,
+      dsimp at this,
+      rw [dite_comp, category.comp_id] at this,
+      simp_rw [category.id_comp, eq_to_hom_trans, eq3, eq_to_hom_trans] at this,
+      generalize_proofs h₁ h₂ h₃ h₄ at this,
+      have h' : p₀ ∉ (open_nhds.inclusion y).obj (h₁.some ⊓ unop U) := λ r, h₁.some_spec r.1,
+      split_ifs at this,
+      { exfalso, exact h₁.some_spec (by assumption), },
+      have eq_coe : c.ι.app (op ⟨h₁.some.1, h₂⟩) =
+        eq_to_hom (by { congr, ext, refl }) ≫ c.ι.app (op h₁.some) ≫
+          eq_to_hom (by { congr, ext, refl }),
+      { symmetry,
+        rw [eq_eq_to_hom_comp],
+        have e := c.ι.naturality (eq_to_hom (by {ext, refl}) :
+          (⟨h₁.some.1, h₂⟩ : open_nhds y) ⟶ h₁.some).op,
+        dsimp at e,
+        split_ifs at e with temp,
+        rw [category.comp_id, show terminal.from (ite (p₀ ∈ (open_nhds.inclusion y).obj h₁.some)
+          S (terminal C)) = eq_to_hom (if_neg h₁.some_spec), from terminal_is_terminal.hom_ext _ _,
+          eq_to_hom_trans, eq_to_hom_refl, category.id_comp] at e,
+        rw [←e, eq_to_hom_refl, category.comp_id, eq_to_hom_refl, category.id_comp], },
+      erw [eq_coe, ←this, ←category.assoc, eq_to_hom_trans, eq_to_hom_refl, category.comp_id,
+        ←category.assoc, eq_to_hom_trans],
+      clear this,
+      have := c.ι.naturality (hom_of_le (inf_le_right :
+          (mem_nhds_of_not_mem_closure_singleton p₀ h).some ⊓ unop U ≤ unop U)).op,
+      dsimp at this,
+      rw [dite_comp, category.comp_id] at this,
+      split_ifs at this,
+      rw [←this, eq1, eq_to_hom_trans], }
+  end,
+  uniq' := λ c f H,
+  begin
+    erw [colimit.ι_desc, ←H],
+    simp only [skyscraper_presheaf_cocone_ι_app],
+    dsimp,
+    have : terminal.from
+      (ite (p₀ ∈ (mem_nhds_of_not_mem_closure_singleton p₀ h).some.1) S (terminal C)) =
+      eq_to_hom (if_neg (mem_nhds_of_not_mem_closure_singleton p₀ h).some_spec) :=
+    terminal_is_terminal.hom_ext _ _,
+    erw [this, ←category.assoc, eq_to_hom_trans, eq_to_hom_refl, category.id_comp]
+  end }
+
+/--
+ If `y ∉ closure {p₀}`, then the stalk of `skyscraper_presheaf p₀ S` at `y` is `*`
+ -/
+@[reducible]
+noncomputable def skyscraper_presheaf_stalk_of_not_mem_closure₀ [has_colimits C]
+  {y : X} (h : ¬p₀ ⤳ y) : (skyscraper_presheaf p₀ S).stalk y ≅ terminal C :=
+colimit.iso_colimit_cocone ⟨_, (skyscraper_presheaf_cocone_of_not_mem_closure₀_is_colimit _ S h)⟩
+
+end
+
+section
+
+/-!
+Skyscraper sheaf alternatively can be defined as the pushforward of a sheaf on a single point space
+`{p₀}` defined by `∅ ↦ *` and `{p₀} ↦ S` under the inclusion `{p₀} ↪ X`.
+-/
+
+open topological_space
+open category_theory category_theory.limits
+open Top
+open opposite
+open_locale classical
+
+universes u v w
+
+variables {X : Top.{u}} (p₀ : X) {C : Type v} [category.{w} C] (S : C) [has_terminal C]
+
+/--The topological space with on a point `{p₀}`. Hence the only open sets are ∅ and ⊤.-/
+def single_point_space : Top := ⟨({p₀} : set X), infer_instance⟩
+
+instance : inhabited (single_point_space p₀) := ⟨⟨p₀, rfl⟩⟩
+instance : unique (single_point_space p₀) := unique.subtype_eq p₀
+
+/--
+The presheaf on a single point space `{p₀}` defined by `∅ ↦ *` and `{p₀} ↦ S`
+-/
+@[simps]
+noncomputable def single_point_presheaf : presheaf C (single_point_space p₀) :=
+{ obj := λ U, if U.unop ≠ ⊥ then S else terminal C,
+  map := λ U V inc, if h : V.unop ≠ ⊥
+    then eq_to_hom (if_pos $ λ r, h $ le_bot_iff.mp $ r ▸ le_of_hom inc.unop) ≫
+      𝟙 S ≫ eq_to_hom (if_pos h).symm
+    else terminal.from _ ≫ eq_to_hom (if_neg h).symm,
+  map_id' := λ U,
+  begin
+    split_ifs,
+    { rw [category.id_comp, eq_to_hom_trans, eq_to_hom_refl] },
+    { rw [eq_comp_eq_to_hom, category.id_comp],
+      exact terminal_is_terminal.hom_ext _ _, },
+  end,
+  map_comp' := λ U V W inc1 inc2,
+  begin
+    rw comp_dite,
+    by_cases hW : W.unop ≠ ⊥,
+    { have hV : V.unop ≠ ⊥,
+      { intros r,
+        refine hW (eq_bot_iff.mpr (r ▸ le_of_hom inc2.unop)), },
+      have hU : U.unop ≠ ⊥,
+      { intros r,
+        refine hW (eq_bot_iff.mpr (r ▸ le_of_hom (inc1 ≫ inc2).unop)) },
+      split_ifs,
+      simp only [category.id_comp, eq_to_hom_trans], },
+    { split_ifs;
+      rw [eq_comp_eq_to_hom, category.assoc, category.assoc, eq_to_hom_trans,
+        eq_to_hom_refl, category.comp_id];
+      exact terminal_is_terminal.hom_ext _ _, },
+  end }
+
+/--
+The trivial inclusion `{p₀} ↪ X`.
+-/
+@[simps] def single_point_inclusion : single_point_space p₀ ⟶ X :=
+{ to_fun := λ p, p.1,
+  continuous_to_fun := by continuity }
+
+/--
+The morphism from skyscraper presheaf to pushforward sheaf
+-/
+@[simps] noncomputable def skyscraper_presheaf_to_pushforward :
+  skyscraper_presheaf p₀ S ⟶ (single_point_inclusion p₀) _* (single_point_presheaf p₀ S) :=
+{ app := λ U, if h : p₀ ∈ U.unop
+    then eq_to_hom (skyscraper_presheaf_obj_of_mem _ h) ≫ eq_to_hom
+    begin
+      dsimp,
+      rw if_pos,
+      erw opens.map_obj _ _ U.unop.2,
+      change _ ≠ ⊥,
+      rw opens.ne_bot_iff_nonempty,
+      refine ⟨⟨p₀, rfl⟩, _⟩,
+      erw set.mem_preimage,
+      exact h,
+    end
+    else terminal.from _ ≫ eq_to_hom
+    begin
+      dsimp,
+      rw if_neg,
+      push_neg,
+      rw ←opens.not_nonempty_iff_eq_bot,
+      rintros ⟨⟨x, hx₁⟩, hx₂⟩,
+      rw set.mem_singleton_iff at hx₁,
+      subst hx₁,
+      erw set.mem_preimage at hx₂,
+      exact h hx₂,
+    end,
+  naturality' := λ U V inc,
+  begin
+    by_cases hV : p₀ ∈ V.unop,
+    { have hU : p₀ ∈ U.unop := le_of_hom inc.unop hV,
+      have hV' : ¬(opens.map (single_point_inclusion p₀)).obj (unop V) = ⊥,
+      { change _ ≠ ⊥,
+        rw opens.ne_bot_iff_nonempty,
+        refine ⟨⟨p₀, rfl⟩, _⟩,
+        erw set.mem_preimage,
+        exact hV, },
+      rw [comp_dite, dite_comp],
+      split_ifs,
+      { exfalso, exact hV' h, },
+      { dsimp,
+        split_ifs,
+        simp only [eq_to_hom_trans, category.id_comp], }, },
+    { split_ifs;
+      rw [←category.assoc, eq_comp_eq_to_hom];
+      exact terminal_is_terminal.hom_ext _ _ },
+  end }
+
+/--
+The morphism from pushforward sheaf to skyscraper presheaf
+-/
+@[simps] noncomputable def pushforward_to_skyscraper_presheaf :
+  (single_point_inclusion p₀) _* (single_point_presheaf p₀ S) ⟶
+  skyscraper_presheaf p₀ S :=
+{ app := λ U, if h : p₀ ∈ unop U
+    then eq_to_hom
+    begin
+      dsimp,
+      rw if_pos,
+      erw opens.map_obj _ _ U.unop.2,
+      change _ ≠ ⊥,
+      rw opens.ne_bot_iff_nonempty,
+      refine ⟨⟨p₀, rfl⟩, _⟩,
+      erw set.mem_preimage,
+      exact h,
+    end ≫ eq_to_hom (skyscraper_presheaf_obj_of_mem _ h).symm
+    else terminal.from _ ≫ eq_to_hom (skyscraper_presheaf_obj_of_not_mem _ h).symm,
+  naturality' := λ U V inc,
+  begin
+    rw [comp_dite, dite_comp],
+    by_cases hV : p₀ ∈ V.unop,
+    { have hU : p₀ ∈ U.unop := le_of_hom inc.unop hV,
+      have hV' : ¬(opens.map (single_point_inclusion p₀)).obj (unop V) = ⊥,
+      { change _ ≠ ⊥,
+        rw opens.ne_bot_iff_nonempty,
+        refine ⟨⟨p₀, rfl⟩, _⟩,
+        erw set.mem_preimage,
+        exact hV, },
+      split_ifs,
+      { exfalso, exact hV' h, },
+      { dsimp,
+        split_ifs;
+        rw [eq_to_hom_trans, category.id_comp, eq_to_hom_trans, eq_to_hom_trans,
+          category.id_comp, eq_to_hom_trans, eq_to_hom_trans, eq_to_hom_trans], }, },
+    { split_ifs;
+      rw [←category.assoc, eq_comp_eq_to_hom];
+      exact terminal_is_terminal.hom_ext _ _ },
+  end }
+
+/--
+Skyscraper presheaf is isomorphic to pushforward of sheaf on single point.
+-/
+noncomputable def skyscraper_presheaf_as_pushforward :
+  skyscraper_presheaf p₀ S ≅ (single_point_inclusion p₀) _* (single_point_presheaf p₀ S) :=
+{ hom := skyscraper_presheaf_to_pushforward p₀ S,
+  inv := pushforward_to_skyscraper_presheaf p₀ S,
+  hom_inv_id' :=
+  begin
+    ext U,
+    dsimp,
+    split_ifs,
+    { rw [eq_to_hom_trans, eq_to_hom_trans, eq_to_hom_trans, eq_to_hom_refl], },
+    { rw [←category.assoc, eq_comp_eq_to_hom],
+      exact terminal_is_terminal.hom_ext _ _, },
+  end,
+  inv_hom_id' :=
+  begin
+    ext U,
+    dsimp,
+    by_cases hU : p₀ ∈ U.unop,
+    { split_ifs;
+      rw [eq_to_hom_trans, eq_to_hom_trans, eq_to_hom_trans, eq_to_hom_refl], },
+    { split_ifs;
+      rw [←category.assoc, eq_comp_eq_to_hom];
+      exact terminal_is_terminal.hom_ext _ _, },
+  end }
+
+end
+
+section adjoints
+
+open topological_space
+open category_theory category_theory.limits
+open Top
+open opposite
+
+universes u v
+
+variables {X : Top.{u}} (p₀ : X) {C : Type v} [category.{u} C]
+variables [has_terminal C] -- {star : C} (ts : is_terminal star)
+variable [Π (U : opens X), decidable (p₀ ∈ U)]
+
+@[simps]
+def skyscraper_presheaf_functor : C ⥤ presheaf C X :=
+{ obj := λ S, skyscraper_presheaf p₀ S,
+  map := λ x y f,
+  { app := λ U, if h : p₀ ∈ U.unop
+    then eq_to_hom (skyscraper_presheaf_obj_of_mem _ h) ≫ f ≫
+      eq_to_hom (skyscraper_presheaf_obj_of_mem _ h).symm
+    else terminal.from _ ≫ eq_to_hom (skyscraper_presheaf_obj_of_not_mem _ h).symm,
+    naturality' := λ U V inc,
+    begin
+      dsimp,
+      simp_rw [category.id_comp, eq_to_hom_trans],
+      by_cases hV : p₀ ∈ V.unop,
+      { have hU : p₀ ∈ U.unop := le_of_hom inc.unop hV,
+        split_ifs,
+        rw [←category.assoc, eq_to_hom_trans, category.assoc, category.assoc, eq_to_hom_trans],
+        refl, },
+      { split_ifs;
+        rw [←category.assoc, eq_comp_eq_to_hom];
+        exact terminal_is_terminal.hom_ext _ _ }
+    end },
+  map_id' := λ c,
+  begin
+    ext U,
+    dsimp,
+    split_ifs,
+    { simp, },
+    { rw [eq_comp_eq_to_hom],
+      exact terminal_is_terminal.hom_ext _ _ },
+  end,
+  map_comp' := λ x y z f g,
+  begin
+    ext U,
+    dsimp,
+    split_ifs,
+    { simp },
+    { rw [eq_comp_eq_to_hom],
+      exact terminal_is_terminal.hom_ext _ _ },
+  end }
+
+@[simps]
+def skyscraper_sheaf_functor : C ⥤ sheaf C X :=
+{ obj := λ S, skyscraper_sheaf p₀ S,
+  map := λ x y f, ⟨(skyscraper_presheaf_functor p₀).map f⟩,
+  map_id' := λ c,
+  begin
+    ext1,
+    exact (skyscraper_presheaf_functor p₀).map_id c,
+  end,
+  map_comp' := λ x y z f g,
+  begin
+    ext1,
+    exact (skyscraper_presheaf_functor p₀).map_comp f g,
+  end }
+
+variable [has_colimits C]
+
+@[simps]
+noncomputable def from_stalk_to_to_skyscraper_presheaf {𝓕 : presheaf C X} {c : C}
+  (f : 𝓕.stalk p₀ ⟶ c) : 𝓕 ⟶ skyscraper_presheaf p₀ c :=
+{ app := λ U, if h : p₀ ∈ U.unop
+  then 𝓕.germ ⟨p₀, h⟩ ≫ f ≫ eq_to_hom (skyscraper_presheaf_obj_of_mem _ h).symm
+  else terminal.from _ ≫ eq_to_hom (skyscraper_presheaf_obj_of_not_mem _ h).symm,
+  naturality' := λ U V inc,
+  begin
+    dsimp,
+    by_cases hV : p₀ ∈ V.unop,
+    { have hU : p₀ ∈ U.unop := le_of_hom inc.unop hV,
+      split_ifs,
+      erw [←category.assoc, 𝓕.germ_res inc.unop, category.id_comp, eq_to_hom_trans,
+        category.assoc, category.assoc, eq_to_hom_trans],
+      refl, },
+    { split_ifs,
+      rw [←category.assoc, eq_comp_eq_to_hom, category.assoc, category.assoc, eq_to_hom_trans,
+        eq_to_hom_refl, category.comp_id],
+      exact terminal_is_terminal.hom_ext _ _ },
+  end }
+
+@[reducible]
+noncomputable def to_skyscraper_presheaf_to_from_stalk {𝓕 : presheaf C X} {c : C}
+  (f : 𝓕 ⟶ skyscraper_presheaf p₀ c) : 𝓕.stalk p₀ ⟶ c :=
+let CC : cocone ((open_nhds.inclusion p₀).op ⋙ 𝓕) :=
+{ X := c,
+  ι :=
+  { app := λ U, f.app (op U.unop.1) ≫ eq_to_hom
+    begin
+      dsimp,
+      rw if_pos,
+      exact U.unop.2,
+    end,
+    naturality' := λ U V inc,
+    begin
+      dsimp,
+      rw [category.comp_id, ←category.assoc, eq_comp_eq_to_hom, category.assoc, eq_to_hom_trans],
+      generalize_proofs h,
+      erw f.naturality,
+      dsimp,
+      have hV : p₀ ∈ (open_nhds.inclusion p₀).obj V.unop := V.unop.2,
+      split_ifs,
+      rw [category.id_comp, eq_to_hom_trans, eq_comp_eq_to_hom, category.assoc, eq_to_hom_trans,
+        eq_to_hom_refl, category.comp_id],
+      refl,
+    end} } in
+colimit.desc _ CC
+
+lemma from_stalk_to_to_skyscraper_presheaf_to_skyscraper_presheaf_to_from_stalk
+  {𝓕 : presheaf C X} {c : C} (f : 𝓕.stalk p₀ ⟶ c) :
+to_skyscraper_presheaf_to_from_stalk p₀ (from_stalk_to_to_skyscraper_presheaf p₀ f) = f :=
+begin
+  ext U,
+  dsimp,
+  simp only [subtype.val_eq_coe, unop_op, colimit.ι_desc, from_stalk_to_to_skyscraper_presheaf_app],
+  split_ifs,
+  { rw [category.assoc, category.assoc, eq_to_hom_trans, eq_to_hom_refl, category.comp_id],
+    congr,
+    dunfold presheaf.germ,
+    dsimp,
+    congr,
+    convert op_unop _,
+    ext,
+    refl, },
+  { exfalso, exact h U.unop.2,  }
+end
+
+lemma to_skyscraper_presheaf_to_from_stalk_from_stalk_to_to_skyscraper_presheaf
+  {𝓕 : presheaf C X} {c : C} (f : 𝓕 ⟶ skyscraper_presheaf p₀ c) :
+from_stalk_to_to_skyscraper_presheaf p₀ (to_skyscraper_presheaf_to_from_stalk p₀ f) = f :=
+begin
+  ext U,
+  dsimp,
+  split_ifs,
+  { rw [to_skyscraper_presheaf_to_from_stalk],
+    dsimp,
+    dunfold presheaf.germ,
+    rw [←category.assoc, colimit.ι_desc],
+    dsimp,
+    rw [category.assoc, eq_to_hom_trans, eq_to_hom_refl, category.comp_id], },
+  { rw [eq_comp_eq_to_hom],
+    exact terminal_is_terminal.hom_ext _ _ , }
+end
+
+@[simps]
+noncomputable def stalk_skyscraper_presheaf_adj_unit :
+  𝟭 (presheaf C X) ⟶ presheaf.stalk_functor C p₀ ⋙ skyscraper_presheaf_functor p₀ :=
+{ app := λ 𝓕,
+  { app := λ U, if h : p₀ ∈ U.unop
+    then 𝓕.germ ⟨p₀, h⟩ ≫ eq_to_hom (if_pos h).symm
+    else terminal.from _ ≫ eq_to_hom (if_neg h).symm,
+    naturality' := λ U V inc,
+    begin
+      dsimp,
+      by_cases hV : p₀ ∈ V.unop,
+      { have hU : p₀ ∈ U.unop := le_of_hom inc.unop hV,
+        split_ifs,
+        erw [←category.assoc, 𝓕.germ_res inc.unop, category.id_comp, eq_to_hom_trans,
+          category.assoc, eq_to_hom_trans],
+        congr, },
+      { split_ifs,
+        rw [←category.assoc, eq_comp_eq_to_hom],
+        exact terminal_is_terminal.hom_ext _ _, },
+    end },
+  naturality' := λ 𝓕 𝓖 f,
+  begin
+    ext U,
+    dsimp,
+    split_ifs,
+    { rw [←category.assoc, eq_comp_eq_to_hom],
+      simp only [category.assoc, eq_to_hom_trans, eq_to_hom_refl, category.comp_id],
+      rw [←category.assoc _ _ ((presheaf.stalk_functor C p₀).map f), eq_to_hom_trans,
+        eq_to_hom_refl, category.id_comp],
+      erw [colimit.ι_map],
+      congr, },
+    { rw [←category.assoc, eq_comp_eq_to_hom],
+      exact terminal_is_terminal.hom_ext _ _ },
+  end }
+
+@[simps]
+noncomputable def stalk_skyscraper_presheaf_adj_counit :
+  skyscraper_presheaf_functor p₀ ⋙ presheaf.stalk_functor C p₀ ⟶ 𝟭 C :=
+{ app := λ c, (skyscraper_presheaf_stalk_of_mem_closure₀ p₀ c (specializes_rfl : p₀ ⤳ p₀)).hom,
+  naturality' := λ x y f,
+  begin
+    ext U,
+    dsimp,
+    simp only [colimit.iso_colimit_cocone_ι_hom_assoc,
+      skyscraper_presheaf_cocone_of_mem_closure₀_ι_app, category.assoc],
+    erw [←category.assoc, colimit.ι_map],
+    dsimp,
+    split_ifs,
+    { rw [category.assoc, skyscraper_presheaf_stalk_of_mem_closure₀,
+        colimit.iso_colimit_cocone_ι_hom],
+      dsimp,
+      simpa, },
+    { exfalso, exact h U.unop.2 }
+  end }
+
+noncomputable def stalk_skyscraper_presheaf_adj :
+  presheaf.stalk_functor C p₀ ⊣ skyscraper_presheaf_functor p₀ :=
+{ hom_equiv := λ 𝓕 c, ⟨from_stalk_to_to_skyscraper_presheaf p₀,
+    to_skyscraper_presheaf_to_from_stalk p₀,
+    from_stalk_to_to_skyscraper_presheaf_to_skyscraper_presheaf_to_from_stalk p₀,
+    to_skyscraper_presheaf_to_from_stalk_from_stalk_to_to_skyscraper_presheaf p₀⟩,
+  unit := stalk_skyscraper_presheaf_adj_unit p₀,
+  counit := stalk_skyscraper_presheaf_adj_counit p₀,
+  hom_equiv_unit' := λ 𝓕 𝓖 f,
+  begin
+    ext U,
+    dsimp,
+    split_ifs,
+    { simp, },
+    { rw [eq_comp_eq_to_hom],
+      exact terminal_is_terminal.hom_ext _ _ },
+  end,
+  hom_equiv_counit' := λ 𝓕 c g,
+  begin
+    ext U,
+    dsimp,
+    erw [colimit.ι_desc, ←category.assoc, colimit.ι_map, category.assoc,
+      colimit.iso_colimit_cocone_ι_hom],
+    dsimp,
+    rw [eq_comp_eq_to_hom, category.assoc, eq_to_hom_trans, eq_to_hom_refl,
+      category.comp_id],
+    refl,
+  end }
+
+variable (C)
+noncomputable def stalk_skyscraper_sheaf_adj :
+  sheaf.forget C X ⋙ presheaf.stalk_functor _ p₀ ⊣ skyscraper_sheaf_functor p₀ :=
+{ hom_equiv := λ 𝓕 c,
+  ⟨λ f, ⟨from_stalk_to_to_skyscraper_presheaf p₀ f⟩,
+   λ g, to_skyscraper_presheaf_to_from_stalk p₀ g.1,
+   λ f, from_stalk_to_to_skyscraper_presheaf_to_skyscraper_presheaf_to_from_stalk
+     p₀ f,
+   begin
+     intros g,
+     ext1,
+     exact to_skyscraper_presheaf_to_from_stalk_from_stalk_to_to_skyscraper_presheaf p₀ g.1,
+   end⟩,
+  unit :=
+  { app := λ 𝓕, ⟨(stalk_skyscraper_presheaf_adj_unit p₀).app 𝓕.1⟩,
+    naturality' := λ 𝓐 𝓑 ⟨f⟩,
+    begin
+      ext1,
+      dsimp,
+      exact (stalk_skyscraper_presheaf_adj_unit p₀).naturality f,
+    end },
+  counit := stalk_skyscraper_presheaf_adj_counit p₀,
+  hom_equiv_unit' :=
+  begin
+    intros 𝓐 c f,
+    ext1,
+    exact (stalk_skyscraper_presheaf_adj p₀).hom_equiv_unit,
+  end,
+  hom_equiv_counit' := λ 𝓐 c f, (stalk_skyscraper_presheaf_adj p₀).hom_equiv_counit }
+
+end adjoints
+
+section injective
+
+-- need to restrict universe level again
+
+open topological_space
+open category_theory category_theory.limits
+open Top
+open opposite
+
+universes u
+variables {X : Top.{u}} (p₀ : X) [Π (U : opens X), decidable (p₀ ∈ U)]
+variables {C : Type u} [category.{u} C] [concrete_category.{u} C] [has_colimits C]
+variables [has_limits C] [preserves_limits (forget C)] [reflects_isomorphisms (forget C)]
+variables [preserves_filtered_colimits (forget C)]
+
+lemma skyscraper_sheaf_injective (S : C) [injective S] :
+  injective (skyscraper_sheaf p₀ S) :=
+injective.injective_of_adjoint (stalk_skyscraper_sheaf_adj p₀ C) S
+
+end injective
diff --git a/src/topology/sheaves/stalks.lean b/src/topology/sheaves/stalks.lean
index 90f4f1ce8cb0c..fd147878b77a6 100644
--- a/src/topology/sheaves/stalks.lean
+++ b/src/topology/sheaves/stalks.lean
@@ -9,9 +9,11 @@ import topology.sheaves.sheaf_condition.unique_gluing
 import category_theory.limits.types
 import category_theory.limits.preserves.filtered
 import category_theory.limits.final
+import category_theory.adjunction.evaluation
 import topology.sober
 import tactic.elementwise
 import algebra.category.Ring
+import category_theory.sites.sheafification
 
 /-!
 # Stalks
@@ -421,6 +423,51 @@ lemma app_injective_iff_stalk_functor_map_injective {F : sheaf C X}
 ⟨λ h U, app_injective_of_stalk_functor_map_injective f U (λ x, h x.1),
   stalk_functor_map_injective_of_app_injective f⟩
 
+section
+
+variable (C)
+
+instance stalk_functor_preserves_mono (x : X) :
+  functor.preserves_monomorphisms (sheaf.forget C X ⋙ stalk_functor C x) :=
+begin
+  refine ⟨λ 𝓐 𝓑 f im, _⟩,
+  apply concrete_category.mono_of_injective,
+  haveI : preserves_limits_of_shape walking_cospan (forget C) := infer_instance,
+  haveI im2 : mono f.1 := @@category_theory.presheaf_mono_of_mono _ _ _ _ _ _ _ _ _ _ _ im,
+  have im3 := (nat_trans.mono_iff_app_mono _ f.1).mp im2,
+  have : ∀ (c : (opens X)ᵒᵖ), function.injective (f.1.app c) := λ c,
+    (@@concrete_category.mono_iff_injective_of_preserves_pullback _ _ (f.1.app c) _).mp (im3 c),
+  refine (app_injective_iff_stalk_functor_map_injective f.1).mpr _ x,
+  rintros U,
+  apply this,
+end
+
+instance stalk_mono_of_mono (x : X) {F G : sheaf C X} (f : F ⟶ G) [mono f] :
+  mono $ (stalk_functor C x).map f.1 :=
+begin
+  have := functor.map_mono (sheaf.forget C X ⋙ stalk_functor C x) f,
+  exact this,
+end
+
+instance mono_of_stalk_mono {F G : sheaf C X} (f : F ⟶ G)
+  [Π (x : X), mono $ (stalk_functor C x).map f.1] :
+  mono f :=
+begin
+  rw [Sheaf.hom.mono_iff_presheaf_mono, nat_trans.mono_iff_app_mono],
+  intros U,
+  rw concrete_category.mono_iff_injective_of_preserves_pullback,
+  refine app_injective_of_stalk_functor_map_injective f.1 U.unop _,
+  rintros ⟨x, hx⟩,
+  rw ←concrete_category.mono_iff_injective_of_preserves_pullback,
+  apply_instance,
+end
+
+lemma mono_iff_stalk_mono {F G : sheaf C X} (f : F ⟶ G) :
+  mono f ↔ ∀ x, mono ((stalk_functor C x).map f.1) :=
+⟨λ m, by { resetI, apply_instance }, λ m, by { resetI, apply_instance }⟩
+
+end
+
 /-- For surjectivity, we are given an arbitrary section `t` and need to find a preimage for it.
 We claim that it suffices to find preimages *locally*. That is, for each `x : U` we construct
 a neighborhood `V ≤ U` and a section `s : F.obj (op V))` such that `f.app (op V) s` and `t`