universe issue of `ModuleCat.extendScalars`

Stream: mathlib4

[Nailin Guan]

I am currently working on proving Ext commute with localization if assuming the ring is Noetherian and module finitely generated.
We currently have Ext(M,N) => Ext(F(M),F(N)) when F is exact, we would like to apply it to the case F is base change R => S. However we found that ModuleCat.extendScalars need the universe of ModuleCat on the right exactly equal to max u v where v is the original level of universe and u is universe of S.
I am imagining using shrink to generalize this to assuming Small.{v'} S and v \le v',then we are able to define the version for universe v to universe v'

[Nailin Guan]

However this may need some total refactor with this part. As we need it to be adjoint functor with restrict scalars. I think picking v = v' is fine in this case, as the only generalization we can do to restrict scalars is leting v \ge v'.

[Andrew Yang]

I think we prefer to keep the defeqs for extendScalar so I think this should be its own def.

[Nailin Guan]

If nobody is against the codes that might seem duplicate, your suggestion is totally fine (which is what I intend to do).