AB axioms in module categories

This file proves that the category of modules over a ring satisfies Grothendieck's axioms AB5, AB4, and AB4*. Further, it proves that R is a separator in the category of modules over R, and concludes that this category is Grothendieck abelian.

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)

theorem ModuleCat.isSeparator (R : Type u) [Ring R] [Small.{v, u} R] : CategoryTheory.IsSeparator (of R (Shrink.{v, u} R))

instance instHasSeparatorModuleCatOfSmall (R : Type u) [Ring R] [Small.{v, u} R] : CategoryTheory.HasSeparator (ModuleCat R)

instance instIsGrothendieckAbelianModuleCat (R : Type u) [Ring R] : CategoryTheory.IsGrothendieckAbelian.{u, u, u + 1} (ModuleCat R)