Commit 2024-05-30 18:46 4cdf280b

refactor(CategoryTheory): the structure Functor.FullyFaithful (#12929) This PR introduces a structure containing the data involved in a fully faithful functor F, i.e. inverse maps to F.map. (This was suggested by Andrew Yang.) This should also restore certain definitional properties which may have been lost in #12449 and #12462. Better names have been given to lemmas IsIso.of_iso and IsIso.of_iso_inv which are now Iso.isIso_hom and Iso.isIso_inv.