[Merged by Bors] - chore(CategoryTheory/Adjunction): move Adjunction.restrictFullyFaithful to separate file

[dagurtomas]

Also resolves a TODO to add lemmas about Adjunction.restrictFullyFaithful

---

• depends on: [Merged by Bors] - feat(CategoryTheory/Adjunction): given an abstract isomorphism, the counit is an isomorphism #12344

[leanprover-community-mathlib4-bot]

This PR/issue depends on:

• [Merged by Bors] - feat(CategoryTheory/Adjunction): given an abstract isomorphism, the counit is an isomorphism #12344
  By Dependent Issues (🤖). Happy coding!

[joelriou]

You removed two TODOs from the original file, but I do not see them after your moved the code. There was one about full/faithful separately, and the other one was about lemmas describing the produced adjunction, but I do not see where are these lemmas?!

[joelriou]

The equational lemmas that are automatically produced are not the greatest (because of the presence of Functor.preimage in the RHS). For unit_app, I would suggest this one instead:

@[simp, reassoc]
lemma map_restrictFullyFaithful_unit_app (X : C) :
    iC.map ((restrictFullyFaithful iC iD adj comm1 comm2).unit.app X) =
    adj.unit.app (iC.obj X) ≫ R'.map (comm1.hom.app X) ≫ comm2.hom.app (L.obj X) := by
  simp [restrictFullyFaithful]

(and something similar for counit_app).

[dagurtomas]

Ok, thanks for the suggestion, it's done.

Do I understand correctly that adding specific lemmas for homEquiv_apply and homEquiv_symm_apply is unnecessary, becuause homEquiv_unit/homEquiv_counit together with the lemmas I added about unit/counit will simplify expressions of that form automatically?

[joelriou]

Thanks!

bors d+

[mathlib-bors]

✌️ dagurtomas can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

[dagurtomas]

bors merge

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• Build
• Check all files imported
• Lint style