Localization and Residue Fields

Stream: Is there code for X?

[Coleton Kotch]

Do we have that localizing at a prime and then taking residues is the same as quotienting and taking fractions?

[Coleton Kotch]

Also, do we have a version of the associativity of the tensor product for R,S bimodules? Seems to only exist for when all modules are under the same ring

[Coleton Kotch]

It appears not judging from here

[Coleton Kotch]

I was mistaken (upon a second glance the link doe not say what I had thought at first) I found what I was looking for in TensorProduct.Tower

[Riccardo Brasca]

IIRC @Antoine Chambert-Loir has thought about that

[Anne Baanen]

Coleton Kotch said:

Do we have that localizing at a prime and then taking residues is the same as quotienting and taking fractions?

I recall using something like this when working on the ideal norm, so you might find a place to start in file#Mathlib/RingTheory/Ideal/Norm