Module localization

Stream: Is there code for X?

[Filippo A. E. Nuccio]

Do we have the notion of the localization of an R-module M at some multiplicative submonoid S of R? I know about localizing rings and localizing arbitrary monoids at their submonoids, but I cannot figure out how to use them to localize a module at a submonoid of the ring. In my mind everything is commutative (and rings are rings) but I am happy to have it for semi-quasi-modules over pre-commutative-semi-almost-rings...

[Riccardo Brasca]

See algebra.module.localized_module and friends.

[Riccardo Brasca]

We have both the construction and the characteristic predicate, but both landed in mathlib quite recently, so there can be basic results still missing.

[Filippo A. E. Nuccio]

Thanks!

[Filippo A. E. Nuccio]

In particular, it seems to me that basic properties of localizing linear maps are missing: something like

1. Given $f\colon M \rightarrow N$ that is $R$-linear, we can construct a $S^{-1}R$-linear map $S^{-1}f \colon S^{-1}M\rightarrow S^{-1}N$
2. Kernels and cokernels are the localizations (aka localizing is flat).
   Am I dumb and not finding them, or is that correct?

[Riccardo Brasca]

We have the universal property, and that's it I think

[Riccardo Brasca]

see #15559

[Jujian Zhang]

I have plans to work on localization of modules and flatness, do you need them urgently?

[Filippo A. E. Nuccio]

No, on the contrary; I was thinking about assigning it to a student of mine, at least the part concerning the localization of maps.

[Filippo A. E. Nuccio]

Are you planning to work on them soon?