Stream: Is there code for X?

Topic: Gcd type tags

Aaron Anderson (Sep 21 2020 at 07:12):

Gauss’s lemma (or some version of it) needs a finset/multiset version of gcd. To do this, I could just copy/paste the API from multiset.lattice and finset.lattice, but this seems inefficient. Is there a way to use to_additive or another tactic to streamline this?

Aaron Anderson (Sep 21 2020 at 07:17):

If we have a gcd_monoid, to_additive could be a preorder, but you’d need to mod out somehow to turn it directly into a partial-order, and thus a lattice.

Aaron Anderson (Sep 21 2020 at 07:18):

A lattice instance on associates would be easy, but how would we translate to that with a tactic?

Kevin Buzzard (Sep 21 2020 at 09:56):

This is a great question. We should always push these ideas of two processes being "the same" to a mathematician, to try and make it as transparent as possible in Lean. These are good test cases.

Johan Commelin (Sep 21 2020 at 10:07):

Sorry, I'm not sure I follow... can you give an example of a formal statement that you would like to prove "by tactic"?

Reid Barton (Sep 21 2020 at 14:18):

Probably stuff like big-gcd of s union t equals the gcd of (big-gcd of s) and (big-gcd of t)

Reid Barton (Sep 21 2020 at 14:21):

Maybe we could just declare that the order on associates is given by divisibility (or reverse divisibility?) and work there?

Aaron Anderson (Sep 21 2020 at 19:04):

Ideally, we'd translate everything on this page, including what Reid said https://leanprover-community.github.io/mathlib_docs/data/finset/lattice.html

Aaron Anderson (Sep 21 2020 at 19:06):

You could possibly get to Gauss's Lemma using only the fact that a constant divides a polynomial if and only if it divides the gcd of the coefficients, which probably just needs the fact that an element divides the gcd of a finset iff it divides all of the elements of the finset.

Heather Macbeth (Sep 21 2020 at 19:08):

@Riccardo Brasca I took the liberty of subscribing you to this stream, you might be interested in the discussion of Gauss' lemma :up:

Aaron Anderson (Sep 21 2020 at 19:08):

For now, I could probably translate any one result like that one, pretty easily, if I had the lattice structure on associates, which already has the partial order structure. I can start with that PR.

Riccardo Brasca (Sep 21 2020 at 19:11):

@Heather Macbeth thank you!

Aaron Anderson (Sep 21 2020 at 21:17):

Oh right, the awkward thing is that that lattice structure exists... but only for UFDs... and it's used to build the gcd structure

Aaron Anderson (Sep 21 2020 at 21:18):

So this'll need to wait for my UFD refactor to go through

Last updated: May 16 2021 at 05:21 UTC