feat(CategoryTheory): the small object argument

[joelriou]

This is a formalization of the small object argument, which is often attributed to Quillen (even though this argument originally due to Baer appeared in works by Cartan-Eilenberg and Grothendieck).

Under favorable circumstances, if f i : A i ⟶ B i is a family of morphisms in a category C, any morphism p : X ⟶ Y can be factored as a transfinite composition of pushouts of coproducts of morphisms in f, followed by a morphism that has the right lifting property with respect to the family f.

In the PR #20079, we obtain that any Grothendieck abelian category has enough injectives. In particular, using #19986, we shall know that categories of (abelian) sheaves have enough injectives.

---

(This is WIP. The main PR is #20245.)

• depends on: [Merged by Bors] - feat(CategoryTheory/SmallObject/Iteration): Functor.ofCocone #19643
• depends on: feat(CategoryTheory/SmallObject/Iteration): existence of objects (limit case) #19264
• depends on: feat(CategoryTheory/SmallObject): the transfinite iteration of a functor #20142
• depends on: [Merged by Bors] - feat(CategoryTheory): pullbacks/pushouts/limits/colimits of a class of morphisms #20157

[joelriou]

I will work more on #20245 and extract new smaller chunks after part of the code is refactored.