Mapping ideals to localizations

Stream: Is there code for X?

[Kenji Nakagawa]

Hi, recently I've wanted to formalize some stuff with neotherian domains and localizations at the nonzero prime P. More specifically, I want to show that for any other prime Q, QR_P=R_P, and several other related facts, however, I'm not sure if there's already a way to do this. At first I thought this was done with fractional ideals, but after thinking about it some, realized it wasn't.

[Anne Baanen]

Maybe docs#ideal.map helps?

[Kenji Nakagawa]

Thanks, this is precisely what I want!