Zulip Chat Archive

Stream: new members

Topic: Gauss's lemma for polynomials


view this post on Zulip Iain Monro (Aug 14 2020 at 14:08):

Looking for a decent piece of work to use to teach myself Lean, I've sized up https://github.com/leanprover-community/mathlib/issues/2871 as something that looks nice and chunky (and will require me to learn a lot) while still being reasonably achievable. Can't see any work on it in any pull requests / public branches, so I'm gonna give it a try unless someone tells me not to :)

view this post on Zulip Johan Commelin (Aug 14 2020 at 14:09):

Hmmm, I'm still surprised we don't have this.

view this post on Zulip Johan Commelin (Aug 14 2020 at 14:10):

But I don't think we got it since that issue was opened...

view this post on Zulip Johan Commelin (Aug 14 2020 at 14:14):

@Iain Monro A quick grep through the source code confirms that this is still an open hole. I greatly encourage you to take this on (-;

view this post on Zulip Johan Commelin (Aug 14 2020 at 14:14):

I assume you've seen the maths before?

view this post on Zulip Iain Monro (Aug 14 2020 at 14:16):

Yep, in a lecture ten years ago and on the Wikipedia page yesterday :p

view this post on Zulip Iain Monro (Aug 14 2020 at 14:17):

I shouldn't be too rusty though!

view this post on Zulip Kevin Buzzard (Aug 14 2020 at 15:18):

You should also probably prove that polynomial rings over a finite set of variables are UFD's.

view this post on Zulip Iain Monro (Aug 14 2020 at 16:16):

@Kevin Buzzard I'll start with the version for univariate polynomials, and once I've got my head around that, hopefully it won't be too bad to generalise it!

view this post on Zulip Johan Commelin (Aug 14 2020 at 16:18):

@Iain Monro We've done that several times before, I'm pretty sure it will work fine.

view this post on Zulip Iain Monro (Aug 14 2020 at 16:39):

Early sketch of the proof:

import ring_theory.localization

namespace polynomial

variables {R: Type} [normalization_domain R] [unique_factorization_domain R] [decidable_eq (associates R)]

def content (p: polynomial R): R := sorry
def is_primitive (p: polynomial R): Prop := content p = 1
def primitive_part (p: polynomial (fraction_ring R)): polynomial R := sorry
noncomputable def embed_in_field_of_fractions (p: polynomial R): polynomial (fraction_ring R) := p.map (of R).to_map
lemma primitive_part_is_primitive (p: polynomial (fraction_ring R)): p.primitive_part.is_primitive := sorry
lemma primitive_part_of_irreducible_is_irreducible (p: polynomial (fraction_ring R)): irreducible p  irreducible p.primitive_part := sorry
lemma irreducibility_condition (p: polynomial R): irreducible p  p.is_primitive  irreducible p.embed_in_field_of_fractions := sorry

-- Turn the PID instance for `polynomial (fraction_ring R)` into a UFD instance
local attribute [instance] principal_ideal_ring.to_unique_factorization_domain

noncomputable instance : unique_factorization_domain (polynomial R) := unique_factorization_domain.of_unique_irreducible_factorization {
  factors := λ p, (unique_factorization_domain.factors p.embed_in_field_of_fractions).map primitive_part,
  factors_prod := sorry,
  irreducible_factors := sorry,
  unique := sorry
}

end polynomial

I'm guessing that the polynomial namespace and src\ring_theory\polynomial\unique_factorization.lean are a good place for it.

view this post on Zulip Kevin Buzzard (Aug 14 2020 at 16:46):

Hey, before you embark on this, do you know mathlib's crazy definition of a UFD?

view this post on Zulip Kevin Buzzard (Aug 14 2020 at 16:46):

It's not a predicate on integral domains, it contains data. Maybe you want to prove this for some predicate is_UFD?

view this post on Zulip Kevin Buzzard (Aug 14 2020 at 16:50):

@Aaron Anderson do you have one of these up your sleeve? Lean currently only (as far as I know) has constructive UFD's; to make a UFD structure on an ID you actually have to produce a function which factors each nonzero element, as opposed to just proving that such a function exists. I am unclear about whether such a thing will be easier to reason about but my guess is that it will cause problems.

view this post on Zulip Iain Monro (Aug 14 2020 at 16:50):

mathlib's definition of a UFD makes a reasonable amount of sense to me.

view this post on Zulip Iain Monro (Aug 14 2020 at 16:51):

What would a predicate-based proof of this look like?

view this post on Zulip Aaron Anderson (Aug 14 2020 at 17:04):

So far the only thing I have is that with an instance of normalization_domain, we could choose a constructive UFD instance

view this post on Zulip Kevin Buzzard (Aug 14 2020 at 17:12):

I suspect that making the function (probably using the axiom of choice) and then proving things about it won't be much fun. I'd happily be proved wrong! After much discussion on how commutative ring theory should look, we decided on base definitions of comm_ring and integral_domain, and then everything else should be predicates on top, because this solves type class inference. It's on my job list to make a Prop-valued is_UFD but I've not done it yet (we have Prop-valued local rings and DVRs and principal ideal rings, but I have been distracted by valuations and haven't got to UFD's yet). For reasoning, Prop-valued classes are the best.

view this post on Zulip Iain Monro (Aug 14 2020 at 17:16):

Ah, that does explain my confusion at the difference between the definitions of UFDs and PIDs.

view this post on Zulip Iain Monro (Aug 14 2020 at 17:30):

I was going to be hiding the AoC stuff behind normalization_domain, which I had unquestioningly picked up from the GCD domain definition.

view this post on Zulip Iain Monro (Aug 14 2020 at 17:31):

Happy to try to convert UFD into a predicate before trying this, if it helps standardise things.

view this post on Zulip Aaron Anderson (Aug 14 2020 at 17:42):

On the math stream, I’ve been talking about my plans for some of the domain criteria

view this post on Zulip Johan Commelin (Aug 17 2020 at 06:46):

@Iain Monro If you start working on #2871, please also post a note on that issue page to "claim" the task :smile:

view this post on Zulip Aaron Anderson (Aug 17 2020 at 17:59):

I've claimed it, because I already have plans for part of it, but I certainly don't want to keep you out of it, @Iain Monro.

view this post on Zulip Aaron Anderson (Aug 17 2020 at 18:01):

I'm going to try to refactor UFDs once #3838 merges, and then it'll be easy to prove that a Noetherian GCD domain is a UFD.

view this post on Zulip Aaron Anderson (Aug 17 2020 at 18:01):

However, it'll still be necessary to prove the formulation of Gauss's lemma that says that the polynomial ring over a GCD domain is a GCD domain.

view this post on Zulip Aaron Anderson (Aug 17 2020 at 18:04):

So @Iain Monro, if you haven't made up your mind, I'd recommend working on Gauss's lemma in the context of gcd_monoid first. Technically this will still require a normalization_monoid instance, but it sounds like you were going to use that anyway.

view this post on Zulip Aaron Anderson (Sep 15 2020 at 01:32):

#4156

view this post on Zulip Aaron Anderson (Sep 15 2020 at 01:33):

Once that's done, Gauss's Lemma (in the sense of putting an instance of gcd_monoid on a polynomial ring over a gcd_monoid) should be enough to solve #2871

view this post on Zulip Floris van Doorn (Sep 15 2020 at 03:15):

(deleted)

view this post on Zulip Kevin Buzzard (Sep 15 2020 at 06:39):

Nice!

view this post on Zulip Riccardo Brasca (Sep 18 2020 at 15:40):

Sorry for the maybe stupid question, but is there enough material in the last PR (or somewhere else) to prove that if fZ[X]f \in \mathbf{Z}[X] and g,hQ[X]g,h\in \mathbf{Q}[X] are all monic and f=ghf = gh then g,hZ[X]g,h \in \mathbf{Z}[X]? Thanks!

view this post on Zulip Heather Macbeth (Sep 19 2020 at 23:01):

@Aaron Anderson ?

view this post on Zulip Aaron Anderson (Sep 19 2020 at 23:05):

Riccardo Brasca said:

Sorry for the maybe stupid question, but is there enough material in the last PR (or somewhere else) to prove that if fZ[X]f \in \mathbf{Z}[X] and g,hQ[X]g,h\in \mathbf{Q}[X] are all monic and f=ghf = gh then g,hZ[X]g,h \in \mathbf{Z}[X]? Thanks!

That's part of Gauss's lemma, which isn't in #4156.

view this post on Zulip Aaron Anderson (Sep 19 2020 at 23:07):

My impression was that @Iain Monro was interested in proving Gauss's lemma.

view this post on Zulip Aaron Anderson (Sep 19 2020 at 23:12):

For now, I just have some notions on what formulation of Gauss's lemma we should prove in Lean, and I'm not 100% sure which parts @Iain Monro is looking to prove.

view this post on Zulip Aaron Anderson (Sep 19 2020 at 23:19):

First, we define what it means for a polynomial with coefficients in a gcd domain to be primitive (gcd of the coefficients is 1). This will need the theory of gcd of a multiset/finset.

view this post on Zulip Aaron Anderson (Sep 19 2020 at 23:23):

Then we show Gauss's Lemma, defined as "the product of two primitive polynomials is primitive".

view this post on Zulip Aaron Anderson (Sep 19 2020 at 23:33):

That'd (at least basically) imply what @Riccardo Brasca was saying.

view this post on Zulip Aaron Anderson (Sep 19 2020 at 23:33):

Then we put a gcd_monoid instance on the polynomial ring over our gcd domain.

view this post on Zulip Aaron Anderson (Sep 19 2020 at 23:33):

That finishes #2871.

view this post on Zulip Aaron Anderson (Oct 01 2020 at 01:09):

I started branch#gauss_lemma, which now has a basic version of Gauss's lemma, although it might not build overall, because I changed the definition of coprime.

view this post on Zulip Aaron Anderson (Oct 01 2020 at 01:14):

There's still a lot of work that'd need to go into chopping it up into PRs, and a decent amount more work in turning it from this form (the content of the product of two polynomials is the product of the contents of the polynomials) to other forms

view this post on Zulip Aaron Anderson (Oct 03 2020 at 17:42):

@Johan Commelin, when I get back to my computer, I’ll link to this branch on the github pull page

view this post on Zulip Johan Commelin (Oct 03 2020 at 17:48):

thx

view this post on Zulip Riccardo Brasca (Oct 21 2020 at 12:36):

I see that multiplicitavity of content in now in mathlib, that's great!

view this post on Zulip Riccardo Brasca (Oct 21 2020 at 12:38):

Is someone working on other versions of Gauss lemma? Like irreducibility in Z[X]\mathbf{Z}[X] is the same as irreducibility in Q[X]\mathbf{Q}[X]?

view this post on Zulip Johan Commelin (Oct 21 2020 at 13:30):

@Aaron Anderson :up:

view this post on Zulip Aaron Anderson (Oct 21 2020 at 17:31):

I’m working first on providing a gcd instance on polynomials (which will also imply a ufd instance)

view this post on Zulip Aaron Anderson (Oct 21 2020 at 17:34):

(deleted)

view this post on Zulip Riccardo Brasca (Nov 14 2020 at 15:50):

@Aaron Anderson Is the fact that if p,qZ[X]p, q\in \mathbf{Z}[X] monic with pqp | q in Q[X]\mathbf{Q}[X] then the quotient has integer coefficients written somewhere now? It should be not too hard but I don't want to redo something already done :sweat_smile:

view this post on Zulip Aaron Anderson (Nov 14 2020 at 18:40):

I don't think so... as I've already been dealing with the relevant things, I can make it happen.

view this post on Zulip Aaron Anderson (Nov 14 2020 at 19:24):

#5003

view this post on Zulip Johan Commelin (Nov 14 2020 at 19:32):

reviewed

view this post on Zulip Riccardo Brasca (Nov 14 2020 at 19:47):

Wow, thank you!!

view this post on Zulip Aaron Anderson (Nov 14 2020 at 20:24):

Technically it’ll only work over a gcd domain, but that’ll work fine here.

view this post on Zulip Aaron Anderson (Nov 14 2020 at 20:26):

I think soon I should refactor is_primitive to mean “not divisible by non-unit constants”, which is equivalent over gcd domains

view this post on Zulip Aaron Anderson (Nov 14 2020 at 20:27):

But I doubt there are any applications coming down the pipeline now that need that generality

view this post on Zulip Riccardo Brasca (Nov 14 2020 at 20:40):

For me it is more than enough! To start writing down the irreducibility of cyclotomic polynomials now I only need that minimal polynomials are irreducible (we have it for fields, it shouldn't be difficult). I will work on it tomorrow.

view this post on Zulip Aaron Anderson (Nov 14 2020 at 21:26):

There is a lemma minimal_polynomial.irreducible, and I think it should apply here?

view this post on Zulip Aaron Anderson (Nov 14 2020 at 21:33):

The trouble as I see it is showing that the product definition is in fact minimal, but perhaps you've figured that out.

view this post on Zulip Riccardo Brasca (Nov 14 2020 at 21:46):

The point is that minimal_polynomial.irreducible works for minimal polynomials over a field. What I plan to do is to take μ a primitive root of unity, show h : is_integral ℤ μ (that is trivial), so I can consider P := minimal_polynomial h. At the end I want to prove that P = cyclotomic n ℤ, but first of all I need that P is the minimal polynomial over . I thought this was easy with Gauss' lemma, but now I see that I have to prove that P is irreducible. By definition it is the monic polynomial with minimal degree that has μ as root, showing the irreducibiity seems a little long, but not difficult.


Last updated: May 13 2021 at 06:15 UTC