Commit 2022-09-30 13:10 a52be2a5View on Github →
feat(category_theory/localization): whiskering_left_equivalence and definition of the predicate (#16646)
In this PR, an equivalence
localization.construction.whiskering_left_equivalence W D : (W.localization ⥤ D) ≌ W.functors_inverting D is obtained and the predicate
L.is_localization W is defined for a functor
L : C ⥤ D.
added theorem category_theory.morphism_property.Q_inverts