feat(topology/sheaves/*): sheaves have enough injectives under some condition

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

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,

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.

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