Zulip Chat Archive

Stream: new members

Topic: Confusion about ≤ in UFD


view this post on Zulip Riccardo Brasca (Nov 18 2020 at 18:44):

Hi, I want to prove that if a separable polynomial PP divides a power QnQ^n then it divides QQ. I know that the factors of PP are simple, by polynomial.is_unit_of_self_mul_dvd_separable or a similar result, but how can I use it? I thought I would have found something like "if the multiplicity of any prime factor in PP is less or equal than the multiplicity in QQ, then PP divides QQ" in ring_theory.unique_factorization_domain. Is what associates.prod_mono actually says? I am not able to find the definition of in this case.

view this post on Zulip Kevin Buzzard (Nov 18 2020 at 18:48):

Seems to me that a term of type factor_set R is either a multiset (a.k.a. finite set with multiplicities allowed) of irreducible-elements-of-R-modulo-equivalence, where the equivalence is "differ by a unit", or a "top" element which is presumably used to represent 0.

view this post on Zulip Kevin Buzzard (Nov 18 2020 at 18:50):

prod is a function which takes one of these multisets (so irreducibles, defined up to units) and multiplies them all together to get an element of the UFD, defined up to units. I guess <= will be defined as "divides", which makes sense in this context. So prod_mono says something like "if you have two multisets of factors, one contained in the other, then the product of the smaller set divides the product of the larger set"

view this post on Zulip Riccardo Brasca (Nov 18 2020 at 18:52):

Yes, it is what I think too, but how can I apply this in practice? I mean, transform my in with some rw.

view this post on Zulip Kevin Buzzard (Nov 18 2020 at 18:55):

I've not ever used this new UFD stuff and don't know my way around the library at all, but I do know that if you knock up a MWE then you're more likely to get a good answer.

view this post on Zulip Kevin Buzzard (Nov 18 2020 at 18:56):

Looking at where is_unit_of_self_mul_dvd_separable is used, I have run into multiplicity_le_one_of_seperable

view this post on Zulip Kevin Buzzard (Nov 18 2020 at 18:57):

which is not how you spell separable but it still might help

view this post on Zulip Kevin Buzzard (Nov 18 2020 at 19:00):

Isn't there some general theory of squarefree stuff somewhere? Did I see this in a recent PR? For me, the natural proof would go separable -> squarefree (using this seperable thing) and P squarefree -> P|Q^n->P|Q

view this post on Zulip Kevin Buzzard (Nov 18 2020 at 19:01):

src/algebra/squarefree.lean was merged 4 days ago

view this post on Zulip Riccardo Brasca (Nov 18 2020 at 19:02):

What I want to prove is

import field_theory.separable

variables (F : Type*) [field F] (P : polynomial F) (Q : polynomial F)

open polynomial

lemma divides (hsep : separable P) (hzero : Q  0) (n : ) (hdiv: P  Q ^ n) : P  Q :=
begin
  sorry
end

I'll have a look at `squarefree, thank you!

view this post on Zulip Kevin Buzzard (Nov 18 2020 at 19:05):

is_unit_of_self_mul_dvd_separable can be used to prove separable polynomials are squarefree and then it looks like you'll have to get your hands dirty. I suspect that r is squarefree if and only if for all q, r|q^n -> r|q (at least when one has uniqueness of factorization) but this doesn't seem to be in the PR.

view this post on Zulip Kevin Buzzard (Nov 18 2020 at 19:07):

I'm currently working on another branch which doesn't have squarefree so I'm not much help to you :-( You have this nodup thing, so anyone who knows their way around multisets should be able to add it. You'll need that if n>=1 then the finset of factors of q^n and q are the same, and so you'll have an inclusion of finsets, and using nodup you'll be able to get an inclusion of multisets.

view this post on Zulip Riccardo Brasca (Nov 18 2020 at 19:13):

I see that

lemma test {α : Type*} [comm_cancel_monoid_with_zero α] {a b : associates.factor_set α} (h : a  b) :
  a.prod  b.prod :=
begin
  exact associates.prod_mono h,
end

works, so lean "knows" that means . I think I can figure out the rest of the proof.

view this post on Zulip Aaron Anderson (Nov 18 2020 at 20:55):

#5037

view this post on Zulip Kevin Buzzard (Nov 18 2020 at 21:22):

I love this place

view this post on Zulip Aaron Anderson (Nov 18 2020 at 21:29):

(Just proven for squarefree, not separable)

view this post on Zulip Riccardo Brasca (Nov 18 2020 at 21:40):

I'm taking care of it, I will make a PR tomorrow.

view this post on Zulip Riccardo Brasca (Nov 18 2020 at 21:58):

#5039 It was really quick :)

view this post on Zulip Kevin Buzzard (Nov 18 2020 at 22:06):

This is the advantage of making all these little steps.

I was reading something by Deligne, describing Grothendieck's work. Deligne said that he would write arguments and everything would be short and simple and easy, and nothing seemed to be happening, and then all of a sudden out of nowhere you had proved something. This is also the mathlib approach. Introduce the concepts which have been proven to be useful and then make the API relating them and one can really make progress in a very elegant way.


Last updated: May 13 2021 at 18:26 UTC