restrict scalar for tensor product

Stream: Is there code for X?

[Kenny Lau]

If R -> S map of rings, with S-modules M and N, then there should be an R-linear map TensorProduct R M N -> TensorProduct S M N?

[Junyan Xu]

TensorProduct.mapOfCompatibleSMul should work

[Kenny Lau]

oh wow thanks, how did you even find this

[Junyan Xu]

I wrote it ...

[Junyan Xu]

but indeed I forgot what it's called, and I loogled TensorProduct, AlgEquiv to find Algebra.TensorProduct.equivOfCompatibleSMul

[Kenny Lau]

I guess I didn't know that it could be strengthened to an isomorphism.

[Kenny Lau]

Are R and S isomorphic from those assumptions?

[Junyan Xu]

No, S might be a localization or quotient of R, or more generally R -> S might be any epimorphism of rings.