mathlib

032f11f8 - feat(category_theory/localization): developing the predicate is_localization (#16890)

feat(category_theory/localization): developing the predicate is_localization (#16890) When `L : C ⥤ D` and `W : morphism_property C`, a constructor for the predicate `L.is_localization W` is introduced: it takes as inputs the universal property of the localized category. In this PR, it is also shown that is `L.is_localization W`, the functor `L` is essentially surjective. Co-authored-by: Joël Riou <37772949+joelriou@users.noreply.github.com>