feat(CategoryTheory): Grothendieck abelian categories have enough injectives

[joelriou]

We formalize the proof by Grothendieck that abelian categories which have exact filtering colimits and a generator have enough injectives (Sur quelques points d'algèbre homologique, Tôhoku Mathematical Journal 9, 1957).

---

• depends on: feat(CategoryTheory): IsDetecting.isIso_iff_of_mono #22135
• depends on: feat(CategoryTheory): monomorphisms are stable under coproducts in Grothendieck abelian categories #22133
• depends on: [Merged by Bors] - feat(CategoryTheory/Abelian/GrothendieckCategory): computing colimits in Subobject #22123
• depends on: [Merged by Bors] - feat(CategoryTheory/Subobject): hasCardinalLT_of_mono #22122
• depends on: [Merged by Bors] - feat(CategoryTheory/Abelian): the exact sequence attached to a pushout square #22110
• depends on: [Merged by Bors] - feat(CategoryTheory): characterization of injective objects in terms of lifting properties #22104
• depends on: feat(Order): Set.Ici.isSuccLimit_coe #22103
• depends on: [Merged by Bors] - feat(CategoryTheory): Monotone.final_functor_iff #22101
• depends on: [Merged by Bors] - feat(CategoryTheory/MorphismProperty): more basic API #22099
• depends on: [Merged by Bors] - feat(CategoryTheory/Abelian): mono are stable under transfinite composition #22060
• depends on: [Merged by Bors] - feat(CategoryTheory/Abelian): mono are stable under cobase change #22057
• depends on: [Merged by Bors] - feat(CategoryTheory/MorphismProperty): classes of morphisms that are stable under transfinite compositions #19306
• depends on: [Merged by Bors] - chore(CategoryTheory): generalize universes for WellPowered #19992
• depends on: [Merged by Bors] - feat(Order): the transfinite iteration of a map #19935
• depends on: [Merged by Bors] - feat(CategoryTheory): pullbacks/pushouts/limits/colimits of a class of morphisms #20157
• depends on: [Merged by Bors] - feat(CategoryTheory): commutation of coyoneda.obj to some colimits in Grothendieck abelian categories #20014
• depends on: [Merged by Bors] - feat(CategoryTheory): the small object argument #20245