mathlib3

0bb88094 - feat(category_theory/limits): left adjoint if preserves colimits (#4942)

feat(category_theory/limits): left adjoint if preserves colimits (#4942) A slight generalisation of a construction from before. Maybe this is the dual version you were talking about @jcommelin - if so my mistake! I think the advantage of doing it this way is that you definitionally get the old version but also the new version too.