refactor(CategoryTheory): the structure Functor.FullyFaithful

[joelriou]

trafficstars

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 be 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.

---

[YaelDillies]

I moved

This was suggested by @erdOne.

to under --- to avoid Andrew getting pinged on Github whenever someone merges the future commit on master into their branch.

[erdOne]

Oops, forgot about this. Thanks a lot! maintainer merge

[github-actions[bot]]

🚀 Pull request has been placed on the maintainer queue by erdOne.

[riccardobrasca]

Thanks!

bors merge

[mathlib-bors[bot]]

Pull request successfully merged into master.

Build succeeded:

• Build
• Check all files imported
• Lint style