feat(CategoryTheory): whiskering a fully faithful functor is full (#1…

…2527)

We already had that whiskering by a faithful functor is faithful. This PR also adds the relevant `Full` and `Faithful` instances for the sheaf version of whiskering, (`sheafCompose`).

Mathlib/CategoryTheory/Sites/Whiskering.lean

@@ -53,6 +53,18 @@ def sheafCompose : Sheaf J A ⥤ Sheaf J B where
 set_option linter.uppercaseLean3 false in
 #align category_theory.Sheaf_compose CategoryTheory.sheafCompose
 
+instance [F.Faithful] : (sheafCompose J F ⋙ sheafToPresheaf _ _).Faithful :=
+  show (sheafToPresheaf _ _ ⋙ (whiskeringRight Cᵒᵖ A B).obj F).Faithful from inferInstance
+
+instance [F.Faithful] [F.Full] : (sheafCompose J F ⋙ sheafToPresheaf _ _).Full :=
+  show (sheafToPresheaf _ _ ⋙ (whiskeringRight Cᵒᵖ A B).obj F).Full from inferInstance
+
+instance [F.Faithful] : (sheafCompose J F).Faithful :=
+  Functor.Faithful.of_comp (sheafCompose J F) (sheafToPresheaf _ _)
+
+instance [F.Full] [F.Faithful] : (sheafCompose J F).Full :=
+  Functor.Full.of_comp_faithful (sheafCompose J F) (sheafToPresheaf _ _)
+
 variable {F G}
 
 /--

Mathlib/CategoryTheory/Whiskering.lean

@@ -114,6 +114,13 @@ instance faithful_whiskeringRight_obj {F : D ⥤ E} [F.Faithful] :
     exact F.map_injective <| congr_fun (congr_arg NatTrans.app hαβ) X
 #align category_theory.faithful_whiskering_right_obj CategoryTheory.faithful_whiskeringRight_obj
 
+instance full_whiskeringRight_obj {F : D ⥤ E} [F.Faithful] [F.Full] :
+    ((whiskeringRight C D E).obj F).Full where
+  map_surjective f := by
+    refine ⟨⟨fun P ↦ F.preimage (f.app P), fun _ _ _ ↦ F.map_injective ?_⟩, ?_⟩
+    · simpa using f.naturality _
+    · ext; simp
+
 @[simp]
 theorem whiskerLeft_id (F : C ⥤ D) {G : D ⥤ E} :
     whiskerLeft F (NatTrans.id G) = NatTrans.id (F.comp G) :=