chore(CategoryTheory/Abelian/GrothendieckAxioms): remove unnecessary premise, clarify definition of AB4/5 (#18810)

Remove the unnecessary `HasFiniteCoproducts` premise from `AB4.ofAB5` and clarify in the module docstring that the typeclasses `AB4` and `AB5` don't require `Abelian`.



Co-authored-by: Paul Reichert <6992158+datokrat@users.noreply.github.com>

Author: Paul Reichert

Mathlib/CategoryTheory/Abelian/GrothendieckAxioms.lean

@@ -17,8 +17,8 @@ basic facts about them.
 
 ## Definitions
 
-- `AB4` -- an abelian category satisfies `AB4` provided that coproducts are exact.
-- `AB5` -- an abelian category satisfies `AB5` provided that filtered colimits are exact.
+- `AB4` -- a category satisfies `AB4` provided that coproducts are exact.
+- `AB5` -- a category satisfies `AB5` provided that filtered colimits are exact.
 - The duals of the above definitions, called `AB4Star` and `AB5Star`.
 
 ## Theorems
@@ -33,10 +33,13 @@ comments of the linked Stacks page.
 Exactness as the preservation of short exact sequences is introduced in
 `CategoryTheory.Abelian.Exact`.
 
+We do not require `Abelian` in the definition of `AB4` and `AB5` because these classes represent
+individual axioms. An `AB4` category is an _abelian_ category satisfying `AB4`, and similarly for
+`AB5`.
+
 ## Projects
 
 - Add additional axioms, especially define Grothendieck categories.
-- Prove that `AB5` implies `AB4`.
 
 ## References
 * [Stacks: Grothendieck's AB conditions](https://stacks.math.columbia.edu/tag/079A)
@@ -117,7 +120,7 @@ instance preservesFiniteLimitsLiftToFinset : PreservesFiniteLimits (liftToFinset
     preservesFiniteLimitsOfNatIso (liftToFinsetEvaluationIso  I).symm
 
 /-- A category with finite biproducts and finite limits is AB4 if it is AB5. -/
-def AB4.ofAB5 [HasFiniteCoproducts C] [HasFilteredColimits C] [AB5 C] : AB4 C where
+def AB4.ofAB5 [HasFilteredColimits C] [AB5 C] : AB4 C where
   preservesFiniteLimits J :=
     letI : PreservesFiniteLimits (liftToFinset C J ⋙ colim) :=
       compPreservesFiniteLimits _ _