Exactness of functors for change of rings. #
In this file we provide exactness of restrictScalars for general universe level using it preserves
short exact sequences.
Note : previously exactness of ModuleCat.restrictScalars is synthesized via being adjoint functor,
however this needs the universe level to be some max u v, where u is the universe level
of the ring.
theorem
ModuleCat.restrictScalars_map_exact
{R : Type u}
[Ring R]
{R' : Type u'}
[Ring R']
(f : R →+* R')
(S : CategoryTheory.ShortComplex (ModuleCat R'))
(h : S.Exact)
:
(S.map (restrictScalars f)).Exact