Confusion about ≤ in UFD

Stream: new members

[Riccardo Brasca]

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]

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]

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]

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]

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]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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]

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

[Riccardo Brasca]

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]

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]

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]

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.

[Aaron Anderson]

#5037

[Kevin Buzzard]

I love this place

[Aaron Anderson]

(Just proven for squarefree, not separable)

[Riccardo Brasca]

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

[Riccardo Brasca]

#5039 It was really quick :)

[Kevin Buzzard]

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.