chore(category/equivalence): remove functor.fun_inv_id (#6450)

`F.fun_inv_id` was just a confusing alternative way to write `F.as_equivalence.unit_iso.symm`, and meant that many lemmas couldn't fire.

Deletes the definitions `functor.fun_inv_id` and `functor.inv_hom_id`, and the lemmas `is_equivalence.functor_unit_comp` and `is_equivalence.inv_fun_id_inv_comp`.

Co-authored-by: Scott Morrison <scott.morrison@gmail.com>

src/category_theory/adjunction/lifting.lean

@@ -205,7 +205,8 @@ begin
     { resetI,
       apply_instance },
     { let : R' ⋙ (monad.comparison (adjunction.of_right_adjoint U)).inv ≅ R :=
-        (iso_whisker_left R (monad.comparison _).fun_inv_id : _) ≪≫ R.right_unitor,
+        (iso_whisker_left R (monad.comparison _).as_equivalence.unit_iso.symm : _) ≪≫
+          R.right_unitor,
       exactI adjunction.right_adjoint_of_nat_iso this } },
   let : is_right_adjoint (R' ⋙ monad.forget (adjunction.of_right_adjoint U).to_monad) :=
     adjunction.right_adjoint_of_nat_iso

src/category_theory/adjunction/limits.lean

@@ -85,7 +85,7 @@ instance is_equivalence_reflects_colimits (E : D ⥤ C) [is_equivalence E] : ref
   { reflects_colimit := λ K,
     { reflects := λ c t,
       begin
-        have l := (is_colimit_of_preserves E.inv t).map_cocone_equiv E.fun_inv_id,
+        have l := (is_colimit_of_preserves E.inv t).map_cocone_equiv E.as_equivalence.unit_iso.symm,
         refine (((is_colimit.precompose_inv_equiv K.right_unitor _).symm) l).of_iso_colimit _,
         tidy,
       end } } }
@@ -113,7 +113,7 @@ lemma has_colimit_of_comp_equivalence (E : C ⥤ D) [is_equivalence E] [has_coli
   has_colimit K :=
 @has_colimit_of_iso _ _ _ _ (K ⋙ E ⋙ inv E) K
 (@adjunction.has_colimit_comp_equivalence _ _ _ _ _ _ (K ⋙ E) (inv E) _ _)
-((functor.right_unitor _).symm ≪≫ (iso_whisker_left K (fun_inv_id E)).symm)
+((functor.right_unitor _).symm ≪≫ iso_whisker_left K (E.as_equivalence.unit_iso))
 
 end preservation_colimits
 
@@ -182,7 +182,7 @@ instance is_equivalence_reflects_limits (E : D ⥤ C) [is_equivalence E] : refle
   { reflects_limit := λ K,
     { reflects := λ c t,
       begin
-        have := (is_limit_of_preserves E.inv t).map_cone_equiv E.fun_inv_id,
+        have := (is_limit_of_preserves E.inv t).map_cone_equiv E.as_equivalence.unit_iso.symm,
         refine (((is_limit.postcompose_hom_equiv K.left_unitor _).symm) this).of_iso_limit _,
         tidy,
       end } } }
@@ -210,7 +210,7 @@ lemma has_limit_of_comp_equivalence (E : D ⥤ C) [is_equivalence E] [has_limit
   has_limit K :=
 @has_limit_of_iso _ _ _ _ (K ⋙ E ⋙ inv E) K
 (@adjunction.has_limit_comp_equivalence _ _ _ _ _ _ (K ⋙ E) (inv E) _ _)
-((iso_whisker_left K (fun_inv_id E)) ≪≫ (functor.right_unitor _))
+((iso_whisker_left K E.as_equivalence.unit_iso.symm) ≪≫ (functor.right_unitor _))
 
 end preservation_limits
 

src/category_theory/equivalence.lean

@@ -432,16 +432,6 @@ is_equivalence.of_equivalence F.as_equivalence.symm
 @[simp] lemma inv_inv (F : C ⥤ D) [is_equivalence F] :
   inv (inv F) = F := rfl
 
-/-- The composition of functor that is an equivalence with its inverse is naturally isomorphic to
-    the identity functor. -/
-def fun_inv_id (F : C ⥤ D) [is_equivalence F] : F ⋙ F.inv ≅ 𝟭 C :=
-is_equivalence.unit_iso.symm
-
-/-- The composition of functor that is an equivalence with its inverse is naturally isomorphic to
-    the identity functor. -/
-def inv_fun_id (F : C ⥤ D) [is_equivalence F] : F.inv ⋙ F ≅ 𝟭 D :=
-is_equivalence.counit_iso
-
 variables {E : Type u₃} [category.{v₃} E]
 
 instance is_equivalence_trans (F : C ⥤ D) (G : D ⥤ E) [is_equivalence F] [is_equivalence G] :
@@ -471,28 +461,18 @@ end equivalence
 namespace is_equivalence
 
 @[simp] lemma fun_inv_map (F : C ⥤ D) [is_equivalence F] (X Y : D) (f : X ⟶ Y) :
-  F.map (F.inv.map f) = F.inv_fun_id.hom.app X ≫ f ≫ F.inv_fun_id.inv.app Y :=
+  F.map (F.inv.map f) = F.as_equivalence.counit.app X ≫ f ≫ F.as_equivalence.counit_inv.app Y :=
 begin
   erw [nat_iso.naturality_2],
   refl
 end
 @[simp] lemma inv_fun_map (F : C ⥤ D) [is_equivalence F] (X Y : C) (f : X ⟶ Y) :
-  F.inv.map (F.map f) = F.fun_inv_id.hom.app X ≫ f ≫ F.fun_inv_id.inv.app Y :=
+  F.inv.map (F.map f) = F.as_equivalence.unit_inv.app X ≫ f ≫ F.as_equivalence.unit.app Y :=
 begin
-  erw [nat_iso.naturality_2],
+  erw [nat_iso.naturality_1],
   refl
 end
 
--- We should probably restate many of the lemmas about `equivalence` for `is_equivalence`,
--- but these are the only ones I need for now.
-@[simp] lemma functor_unit_comp (E : C ⥤ D) [is_equivalence E] (Y) :
-  E.map (E.fun_inv_id.inv.app Y) ≫ E.inv_fun_id.hom.app (E.obj Y) = 𝟙 _ :=
-equivalence.functor_unit_comp E.as_equivalence Y
-
-@[simp] lemma inv_fun_id_inv_comp (E : C ⥤ D) [is_equivalence E] (Y) :
-  E.inv_fun_id.inv.app (E.obj Y) ≫ E.map (E.fun_inv_id.hom.app Y) = 𝟙 _ :=
-eq_of_inv_eq_inv (functor_unit_comp _ _)
-
 end is_equivalence
 
 namespace equivalence
@@ -503,7 +483,7 @@ An equivalence is essentially surjective.
 See https://stacks.math.columbia.edu/tag/02C3.
 -/
 lemma ess_surj_of_equivalence (F : C ⥤ D) [is_equivalence F] : ess_surj F :=
-⟨λ Y, ⟨F.inv.obj Y, ⟨F.inv_fun_id.app Y⟩⟩⟩
+⟨λ Y, ⟨F.inv.obj Y, ⟨F.as_equivalence.counit_iso.app Y⟩⟩⟩
 
 /--
 An equivalence is faithful.
@@ -525,9 +505,9 @@ See https://stacks.math.columbia.edu/tag/02C3.
 -/
 @[priority 100] -- see Note [lower instance priority]
 instance full_of_equivalence (F : C ⥤ D) [is_equivalence F] : full F :=
-{ preimage := λ X Y f, F.fun_inv_id.inv.app X ≫ F.inv.map f ≫ F.fun_inv_id.hom.app Y,
+{ preimage := λ X Y f, F.as_equivalence.unit.app X ≫ F.inv.map f ≫ F.as_equivalence.unit_inv.app Y,
   witness' := λ X Y f, F.inv.map_injective $
-  by simpa only [is_equivalence.inv_fun_map, assoc, iso.hom_inv_id_app_assoc, iso.hom_inv_id_app]
+  by simpa only [is_equivalence.inv_fun_map, assoc, iso.inv_hom_id_app_assoc, iso.inv_hom_id_app]
     using comp_id _ }
 
 @[simps] private noncomputable def equivalence_inverse (F : C ⥤ D) [full F] [faithful F]