Zulip Chat Archive

Stream: maths

Topic: Definition of `polynomial.splits`


view this post on Zulip Yury G. Kudryashov (Oct 20 2020 at 04:02):

Why docs#polynomial.splits uses an auxiliary ring_hom?

view this post on Zulip Yury G. Kudryashov (Oct 20 2020 at 04:02):

I mean, why not define

def splits (f : polynomial α) : Prop :=
f = 0   {g : polynomial α}, irreducible g  g  f  degree g = 1

then use splits (map i f) if needed?

view this post on Zulip Johan Commelin (Oct 20 2020 at 04:16):

@Kenny Lau :up:

view this post on Zulip Mario Carneiro (Oct 20 2020 at 04:30):

From a cursory look at the original definition, it looks not equivalent, because it has a disjunct f = 0 instead of map i f = 0

view this post on Zulip Mario Carneiro (Oct 20 2020 at 04:30):

What does the mathematics have to say about the cases where there is a difference?

view this post on Zulip Yury G. Kudryashov (Oct 20 2020 at 04:33):

docs#polynomial.splits_map_iff

view this post on Zulip Yury G. Kudryashov (Oct 20 2020 at 04:34):

docs#polynomial.map_eq_zero

view this post on Zulip Johan Commelin (Oct 20 2020 at 04:35):

I think mathematics doesn't really care about whether 0 splits or not. That's an implementation detail, and we can choose whatever we find most convenient.

view this post on Zulip Mario Carneiro (Oct 20 2020 at 04:35):

wait, is the codomain a field here?

view this post on Zulip Mario Carneiro (Oct 20 2020 at 04:35):

oh everything is a field

view this post on Zulip Mario Carneiro (Oct 20 2020 at 04:38):

ah, docs#polynomial.splits_id_iff_splits is even more explicit that this can be a unary predicate

view this post on Zulip Mario Carneiro (Oct 20 2020 at 04:42):

I guess the other question is whether the theorems in there follow easily from theorems about splits id and map

view this post on Zulip Yury G. Kudryashov (Oct 20 2020 at 04:49):

#4708 #4709

view this post on Zulip Kenny Lau (Oct 20 2020 at 07:01):

I believe @Chris Hughes wrote it


Last updated: May 11 2021 at 15:12 UTC