## Stream: new members

### Topic: Confusion about ≤ in UFD

#### Riccardo Brasca (Nov 18 2020 at 18:44):

Hi, I want to prove that if a separable polynomial $P$ divides a power $Q^n$ then it divides $Q$. I know that the factors of $P$ 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 $P$ is less or equal than the multiplicity in $Q$, then $P$ divides $Q$" 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.

#### 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.

#### 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"

#### 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.

#### 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.

#### 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

#### Kevin Buzzard (Nov 18 2020 at 18:57):

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

#### 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

#### Kevin Buzzard (Nov 18 2020 at 19:01):

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

#### 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!

#### 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.

#### 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.

#### 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.

#5037

#### Kevin Buzzard (Nov 18 2020 at 21:22):

I love this place

#### Aaron Anderson (Nov 18 2020 at 21:29):

(Just proven for squarefree, not separable`)

#### Riccardo Brasca (Nov 18 2020 at 21:40):

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

#### Riccardo Brasca (Nov 18 2020 at 21:58):

#5039 It was really quick :)

#### 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