Commit 2024-07-06 14:51 06352df9

feat(CategoryTheory/Functor): refactoring Ran (#14291) This PR refactors the definition of the right Kan extension functor (Functor.ran : (C ⥤ E) ⥤ (D ⥤ E)) which sends a functor to its right Kan extension along a given functor F : C ⥤ D. It used to be defined under the existence of certain colimits. It is now part of the general Kan extension API. The only significant change in this PR is about showing that the right Kan extension functor associated to a cocontinuous functors between sites sends sheaves to sheaves (this is in the file CategoryTheory.Sites.CoverLifting). As this functor is no longer based on the limits API, the proofs had to be changed. In the new proof, we proceed directly with sheaves with values in a category A rather than translating the sheaf property in terms of sheaves of types. This PR is the dual counterpart of #10425 which refactored left Kan extensions.