Gauss's lemma for polynomials

Stream: new members

[Iain Monro]

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 :)

[Johan Commelin]

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

[Johan Commelin]

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

[Johan Commelin]

@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 (-;

[Johan Commelin]

I assume you've seen the maths before?

[Iain Monro]

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

[Iain Monro]

I shouldn't be too rusty though!

[Kevin Buzzard]

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

[Iain Monro]

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

[Johan Commelin]

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

[Iain Monro]

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.

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Iain Monro]

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

[Iain Monro]

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

[Aaron Anderson]

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

[Kevin Buzzard]

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.

[Iain Monro]

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

[Iain Monro]

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

[Iain Monro]

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

[Aaron Anderson]

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

[Johan Commelin]

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

[Aaron Anderson]

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.

[Aaron Anderson]

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.

[Aaron Anderson]

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.

[Aaron Anderson]

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.

[Aaron Anderson]

#4156

[Aaron Anderson]

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

[Floris van Doorn]

(deleted)

[Kevin Buzzard]

Nice!

[Riccardo Brasca]

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

[Heather Macbeth]

@Aaron Anderson ?

[Aaron Anderson]

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 $f \in \mathbf{Z}[X]$ and $g,h\in \mathbf{Q}[X]$ are all monic and $f = gh$ then $g,h \in \mathbf{Z}[X]$? Thanks!

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

[Aaron Anderson]

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

[Aaron Anderson]

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.

[Aaron Anderson]

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.

[Aaron Anderson]

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

[Aaron Anderson]

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

[Aaron Anderson]

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

[Aaron Anderson]

That finishes #2871.

[Aaron Anderson]

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.

[Aaron Anderson]

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

[Aaron Anderson]

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

[Johan Commelin]

thx

[Riccardo Brasca]

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

[Riccardo Brasca]

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

[Johan Commelin]

@Aaron Anderson :up:

[Aaron Anderson]

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

[Aaron Anderson]

(deleted)

[Riccardo Brasca]

@Aaron Anderson Is the fact that if $p, q\in \mathbf{Z}[X]$ monic with $p | q$ in $\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:

[Aaron Anderson]

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

[Aaron Anderson]

#5003

[Johan Commelin]

reviewed

[Riccardo Brasca]

Wow, thank you!!

[Aaron Anderson]

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

[Aaron Anderson]

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

[Aaron Anderson]

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

[Riccardo Brasca]

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.

[Aaron Anderson]

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

[Aaron Anderson]

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

[Riccardo Brasca]

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.