Zulip Chat Archive

Stream: maths

Topic: ring localization


view this post on Zulip Yury G. Kudryashov (Apr 26 2020 at 21:44):

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

view this post on Zulip Amelia Livingston (Apr 27 2020 at 09:44):

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.

view this post on Zulip Yury G. Kudryashov (Apr 27 2020 at 18:37):

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

view this post on Zulip Amelia Livingston (May 08 2020 at 09:17):

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 :(

view this post on Zulip Anne Baanen (May 08 2020 at 09:19):

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

view this post on Zulip Amelia Livingston (May 08 2020 at 09:22):

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.

view this post on Zulip Johan Commelin (May 08 2020 at 09:26):

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

view this post on Zulip Johan Commelin (May 08 2020 at 09:26):

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

view this post on Zulip Johan Commelin (May 08 2020 at 09:26):

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

view this post on Zulip Amelia Livingston (May 08 2020 at 09:34):

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


Last updated: May 14 2021 at 18:28 UTC