# Zulip Chat Archive

## Stream: new members

### Topic: Gauss's lemma for polynomials

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

#### Johan Commelin (Aug 14 2020 at 14:09):

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

#### Johan Commelin (Aug 14 2020 at 14:10):

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

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

#### Johan Commelin (Aug 14 2020 at 14:14):

I assume you've seen the maths before?

#### Iain Monro (Aug 14 2020 at 14:16):

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

#### Iain Monro (Aug 14 2020 at 14:17):

I shouldn't be too rusty though!

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

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

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

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

#### Kevin Buzzard (Aug 14 2020 at 16:46):

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

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

?

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

#### Iain Monro (Aug 14 2020 at 16:50):

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

#### Iain Monro (Aug 14 2020 at 16:51):

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

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

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

#### Iain Monro (Aug 14 2020 at 17:16):

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

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

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

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

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

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

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

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

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

#### Aaron Anderson (Sep 15 2020 at 01:32):

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

#### Floris van Doorn (Sep 15 2020 at 03:15):

(deleted)

#### Kevin Buzzard (Sep 15 2020 at 06:39):

Nice!

#### 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 $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 (Sep 19 2020 at 23:01):

@Aaron Anderson ?

#### 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 $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 (Sep 19 2020 at 23:07):

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

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

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

#### Aaron Anderson (Sep 19 2020 at 23:23):

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

#### Aaron Anderson (Sep 19 2020 at 23:33):

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

#### Aaron Anderson (Sep 19 2020 at 23:33):

Then we put a `gcd_monoid`

instance on the polynomial ring over our gcd domain.

#### Aaron Anderson (Sep 19 2020 at 23:33):

That finishes #2871.

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

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

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

#### Johan Commelin (Oct 03 2020 at 17:48):

thx

#### Riccardo Brasca (Oct 21 2020 at 12:36):

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

#### Riccardo Brasca (Oct 21 2020 at 12:38):

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 (Oct 21 2020 at 13:30):

@Aaron Anderson :up:

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

#### Aaron Anderson (Oct 21 2020 at 17:34):

(deleted)

#### Riccardo Brasca (Nov 14 2020 at 15:50):

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

#### Aaron Anderson (Nov 14 2020 at 19:24):

#### Johan Commelin (Nov 14 2020 at 19:32):

reviewed

#### Riccardo Brasca (Nov 14 2020 at 19:47):

Wow, thank you!!

#### Aaron Anderson (Nov 14 2020 at 20:24):

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

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

#### Aaron Anderson (Nov 14 2020 at 20:27):

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

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

#### Aaron Anderson (Nov 14 2020 at 21:26):

There is a lemma `minimal_polynomial.irreducible`

, and I think it should apply here?

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

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