Exact filtered colimits, products and coproducts of modules with independent universes

Filtered colimits, products and coproducts of modules are exact even when the coefficient ring and the modules live in different universes. This supplies the exactness needed for homology with varying coefficients and to commute cohomology with products of cochain complexes. The indexing category or type must be small in the universe of the modules.

The arguments follow Mathlib's AB instances for ModuleCat, by Dagur Asgeirsson: transfer exactness from abelian groups along the forgetful functor. For products, the index type is first replaced by a small copy. In both cases the ring universe is independent of the module universe.

instance TauCeti.moduleCat_ab5OfSize (R : Type u) [Ring R] [UnivLE.{w, v}] [UnivLE.{w', v}] : CategoryTheory.AB5OfSize.{w, w', v, max (v + 1) u} (ModuleCat R)

Filtered colimits of modules indexed by small categories are exact, with no restriction on the universe of the coefficient ring.

instance TauCeti.moduleCat_ab4OfSize (R : Type u) [Ring R] : CategoryTheory.AB4OfSize.{v, v, max (v + 1) u} (ModuleCat R)

Coproducts of modules are exact, with no restriction on the universe of the coefficient ring.

instance TauCeti.moduleCat_hasExactLimitsOfShape_discrete (R : Type u) [Ring R] (ι : Type w) [Small.{v, w} ι] [CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.Discrete ι) (ModuleCat R)] : CategoryTheory.HasExactLimitsOfShape (CategoryTheory.Discrete ι) (ModuleCat R)

Products of modules indexed by a small type are exact, with no restriction on the universe of the coefficient ring.