AB axioms in module categories

This file proves that the category of modules over a ring satisfies Grothendieck's axioms AB5, AB4, and AB4*.

instance instAB5ModuleCat (R : Type u) [Ring R] : CategoryTheory.AB5 (ModuleCat R)

instance instAB4ModuleCat (R : Type u) [Ring R] : CategoryTheory.AB4 (ModuleCat R)

instance instAB4StarModuleCat (R : Type u) [Ring R] : CategoryTheory.AB4Star (ModuleCat R)