Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-10-25 06:39 1a5e56f2

View on Github →

feat(category_theory/localization): basic API for localization of categories (#16969) In this PR, the basic API for the localization of categories is introduced. If a functor L : C ⥤ D is a localization functor for W : morphism_property C, we shall say that a functor F' : D ⥤ E lifts a functor F : C ⥤ E if an isomorphism L ⋙ F' ≅ F is given: this is the class [lifting L W F F']. The basic API for lifting of functors and lifting of natural transformations is included.

Estimated changes