Zulip Chat Archive

Stream: triage

Topic: issue #2871: unique factorisation of polynomials over a UFD


view this post on Zulip Random Issue Bot (Dec 12 2020 at 14:24):

Today I chose issue 2871 for discussion!

unique factorisation of polynomials over a UFD
Created by @Johan Commelin (@jcommelin) on 2020-05-30
Labels: feature-request

Is this issue still relevant? Any recent updates? Anyone making progress?

view this post on Zulip Johan Commelin (Dec 12 2020 at 15:36):

@Aaron Anderson is there anything left here? I don't think so, right?

view this post on Zulip Johan Commelin (Dec 12 2020 at 15:36):

So I guess we can close this issue

view this post on Zulip Aaron Anderson (Dec 12 2020 at 17:37):

You added mv_polynomials to the issue

view this post on Zulip Aaron Anderson (Dec 12 2020 at 17:38):

And I haven’t done the induction on variables, because I was hoping to do it in a super-general way instead of copy-paste

view this post on Zulip Johan Commelin (Dec 12 2020 at 17:39):

aha, makes sense

view this post on Zulip Aaron Anderson (Dec 12 2020 at 17:47):

Perhaps I should copy-paste and then make a new issue calling for the induction principle?

view this post on Zulip Johan Commelin (Dec 12 2020 at 17:50):

whatever you think is best

view this post on Zulip Johan Commelin (Dec 12 2020 at 17:50):

I think there was some chat about an induction principle recently

view this post on Zulip Johan Commelin (Dec 12 2020 at 17:50):

but I don't think it got PRd in the end

view this post on Zulip Aaron Anderson (Dec 12 2020 at 17:54):

No, it didn’t.

view this post on Zulip Aaron Anderson (Dec 12 2020 at 17:55):

I think ideally we’d have some definition of what it means to be a ring property that’s preserved under isos, but that’s got too many universe variables to be easy

view this post on Zulip Johan Commelin (Dec 12 2020 at 17:57):

well, there is the equiv_rw tactic that Scott wrote

view this post on Zulip Johan Commelin (Dec 12 2020 at 17:58):

And he has some category-theoretic machinery to support exactly this "preserved under isos" reasoning

view this post on Zulip Johan Commelin (Dec 12 2020 at 17:58):

But it hasn't seen a lot of use so far

view this post on Zulip Johan Commelin (Dec 12 2020 at 17:58):

And Scott seems to be very busy atm, so I don't think he'll be able to offer support for the time being

view this post on Zulip Random Issue Bot (Dec 28 2020 at 14:28):

Today I chose issue 2871 for discussion!

unique factorisation of polynomials over a UFD
Created by @Johan Commelin (@jcommelin) on 2020-05-30
Labels: feature-request

Is this issue still relevant? Any recent updates? Anyone making progress?


Last updated: May 09 2021 at 16:20 UTC