ring localization

Stream: maths

[Yury G. Kudryashov]

@Amelia Livingston what is the status of your rewrite of localization in terms of monoid_localization?

[Amelia Livingston]

I haven't done much on it lately, sorry - revising for exams. I'm working on it in the evenings this week though and it's going ok. I'm thinking maybe I could PR the main bits of ring_theory.localization first as that's more important, then go back and PR the rest of monoid_localization, because the rest of that is just about specific kinds of localizations.

[Yury G. Kudryashov]

Thank you! I'm just tracking what has to be done to remove is_ring_hom.

[Amelia Livingston]

I've got the beginnings of the file ready to PR - just infrastructure & lift and map, and it's a sizeable PR. But until the rest is PR'ed, this will break all of fractional_ideal.lean :(

[Anne Baanen]

Since I wrote most of fractional_ideal.lean, I could help fixing it

[Amelia Livingston]

Thank you - I'm fine with fixing it - I just mean it's going to break unless I PR literally all of the refactored localization file at once, which would make a very big PR, and I could use some feedback on the initial set up first.

[Johan Commelin]

@Amelia Livingston I think that in that case it makes sense to open the big PR

[Johan Commelin]

Then we can take a look, and maybe see how to split things

[Johan Commelin]

And otherwise we'll just need to deal with a big PR (-;

[Amelia Livingston]

Okay, sure! I'll need a couple of days to get the rest tidied up, then, and I'll PR after that.