feat(CategoryTheory): the equivalence of categories induced by a bijection

joelriou · joelriou · commit 1c8cca8aa673 · 2025-01-20T16:59:04.000+01:00
diff --git a/Mathlib/CategoryTheory/EqToHom.lean b/Mathlib/CategoryTheory/EqToHom.lean
@@ -338,4 +338,26 @@ theorem dcongr_arg {ι : Type*} {F G : ι → C} (α : ∀ i, F i ⟶ G i) {i j
   subst h
   simp
 
+/-- If `T ≃ D` is a bijection and `D` is a category, then
+`InducedCategory D e` is equivalent to `D`. -/
+@[simps]
+def Equivalence.induced {T : Type*} (e : T ≃ D) :
+    InducedCategory D e ≌ D where
+  functor := inducedFunctor e
+  inverse :=
+    { obj := e.symm
+      map {X Y} f := show e (e.symm X) ⟶ e (e.symm Y) from
+        eqToHom (e.apply_symm_apply X) ≫ f ≫
+          eqToHom (e.apply_symm_apply Y).symm
+      map_comp {X Y Z} f g := by
+        dsimp
+        erw [Category.assoc, Category.assoc, Category.assoc]
+        rw [eqToHom_trans_assoc, eqToHom_refl, Category.id_comp] }
+  unitIso := NatIso.ofComponents (fun _ ↦ eqToIso (by simp)) (fun {X Y} f ↦ by
+    dsimp
+    erw [eqToHom_trans_assoc _ (by simp), eqToHom_refl, Category.id_comp]
+    rfl )
+  counitIso := NatIso.ofComponents (fun _ ↦ eqToIso (by simp))
+  functor_unitIso_comp X := eqToHom_trans (by simp) (by simp)
+
 end CategoryTheory
diff --git a/Mathlib/CategoryTheory/EssentiallySmall.lean b/Mathlib/CategoryTheory/EssentiallySmall.lean
@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Kim Morrison
 -/
 import Mathlib.CategoryTheory.Category.ULift
+import Mathlib.CategoryTheory.EqToHom
 import Mathlib.CategoryTheory.Skeletal
 import Mathlib.Logic.UnivLE
 import Mathlib.Logic.Small.Basic
@@ -189,7 +190,7 @@ noncomputable instance [Small.{w} C] : Category.{v} (Shrink.{w} C) :=
 
 /-- The categorical equivalence between `C` and `Shrink C`, when `C` is small. -/
 noncomputable def equivalence [Small.{w} C] : C ≌ Shrink.{w} C :=
-  (inducedFunctor (equivShrink C).symm).asEquivalence.symm
+  (Equivalence.induced _).symm
 
 end Shrink
 
