[Merged by Bors] - feat(CategoryTheory): the left Kan extension functor

[joelriou]

Given a functor F : C ⥤ D, we define the left Kan extension functor F.lan : (C ⥤ E) ⥤ (D ⥤ E) which sends a functor G : C ⥤ E to its left Kan extension along F. (This is a step towards the refactor of Lan/Ran in mathlib using the new API for Kan extensions of functors #10425.)

---

[dagurtomas]

Could you make the variable names throughout the folder Functor/KanExtension more consistent? For example, always use L: C ⥤ D for the "along" functor and F : C ⥤ E for the "of" functor (or whatever). It's a bit confusing that F becomes the "along" functor in the adjunction file when it was the "of" functor in the basic file, and also the categories changed names.

[joelriou]

Thanks @dagurtomas for the suggestion. It was indeed very confusing... Now, we extend F : C ⥤ H along L : C ⥤ D. I use the category H because E is sometimes used for terms in LeftExtension L F. (Doing so, the notations will be more consistent with the future API for derived functors, where L shall be a localization functor.)

[dagurtomas]

Thanks! LGTM

[erdOne]

Thanks!
maintainer merge

[github-actions]

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

[jcommelin]

Thanks so much! 1 minor request.

bors d+

[mathlib-bors]

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

[joelriou]

Thanks!

bors merge

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• Build
• Check all files imported
• Lint style