chore(category_theory/adjunction): reflective lemmas (#5968)

Improves the docstring and changes the name to be more appropriate (the lemma has nothing to do with essential images).
leanprover-community · Feb 1, 2021 · 3f9b035 · 3f9b035
1 parent c5e0d10
commit 3f9b035
Showing 1 changed file with 3 additions and 2 deletions.
diff --git a/src/category_theory/adjunction/reflective.lean b/src/category_theory/adjunction/reflective.lean
@@ -47,11 +47,12 @@ begin
 end
 
 /--
-When restricted to objects in `D` given by `i : D ⥤ C`, the unit is an isomorphism.
+When restricted to objects in `D` given by `i : D ⥤ C`, the unit is an isomorphism. In other words,
+`η_iX` is an isomorphism for any `X` in `D`.
 More generally this applies to objects essentially in the reflective subcategory, see
 `functor.ess_image.unit_iso`.
 -/
-instance functor.ess_image.unit_iso_restrict [reflective i] {B : D} :
+instance is_iso_unit_obj [reflective i] {B : D} :
   is_iso ((adjunction.of_right_adjoint i).unit.app (i.obj B)) :=
 begin
   have : (adjunction.of_right_adjoint i).unit.app (i.obj B) =