feat(category_theory/adjunction/reflective): show compositions of ref…

…lective are reflective (#6298) Show compositions of reflective are reflective.
leanprover-community · Feb 18, 2021 · 8696990 · 8696990
1 parent 96f8933
commit 8696990
Showing 1 changed file with 7 additions and 0 deletions.
diff --git a/src/category_theory/adjunction/reflective.lean b/src/category_theory/adjunction/reflective.lean
@@ -102,4 +102,11 @@ begin
   exact mem_ess_image_of_unit_is_iso A,
 end
 
+universes v₃ u₃
+variables {E : Type u₃} [category.{v₃} E]
+
+/-- Composition of reflective functors. -/
+instance reflective.comp (F : C ⥤ D) (G : D ⥤ E) [Fr : reflective F] [Gr : reflective G] :
+  reflective (F ⋙ G) := { to_faithful := faithful.comp F G, }
+
 end category_theory