mathlib4

mathlib4 copied to clipboard

In this PR, it is shown that left/right Kan extensions of functors F : C ⥤ H along a functor L : C ⥤ D are compatible with changing the functors F and L by isomorphic functors, by the precomposition with an equivalence G : C' ⥤ C, and postcomposition with an equivalence D ⥤ D'.

---

LGTM, but maybe @dagurtomas can give it a look as well?

Thanks for the ping. I'll take a look but I don't have time until tomorrow evening

Thanks! (and thanks Dagur!) maintainer merge

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

This is great, thanks!

bors merge

Pull request successfully merged into master.

Build succeeded:

• Build
• Check all files imported
• Lint style