Localization of modules

[Alizter]

Now that we have localizations of rings #2089 we should introduce localizations of R-modules. This will require two things:

1. Tensor products of modules Tensor products of modules #1926.
2. Showing that rng_localization R S is an R-module.

I have a WIP for 1, which turned out to be trickier than expected, however 2 seems more immediately doable. It only needs to have the action of R on rng_localization R S characterized.

Afterwards, the localization of a moudle will be

$$ S^{-1} M := S^{-1}R \otimes_{R} M$$

We should then be able to give many nice properties about localizations.

[jdchristensen]

Isn't the second check box a special case of the fact that for any ring homomorphism R $-> S, S gets an R-module structure?

About how to define S^-1 M, I'd lean towards defining it using fractions. Then what was just done for rings would be a special case, since R is an R-module. It would just happen that in that case, S^-1 R is again a ring.

Then it would be a theorem that S^-1 M $<~> S^-1 R ⊗ M.

[Alizter]

Is it really a special case? The ring localisation we have included the multiplication which we don't have in the module case. There is definitely some overlap, but it's not clear what the best option would be.

You're correct that this is a special case of extension of scalars along a ring homomorphism, but I'm not convinced we need to avoid the tensor product in the definition.

[jdchristensen]

I'm not sure what you mean. The underlying R-module of the ring localization S^-1 R is the module localization S^-1 R. So if we define localization of R-modules as a quotient of the type of fractions, then this will also be the underlying type of the ring localization. We can also define a map S^-1 R -> S^-1 M -> S^-1 M for any R-module M. When we take M to be R, this will give the multiplication. And for general M, this will make S^-1 M into an S^-1 R-module.