## Stream: maths

### Topic: list of mathlib targets

#### Kevin Buzzard (Aug 25 2018 at 11:48):

Over the next couple of days I'm going to have a good look at the perfectoid project from a "bottom up" perspective and try and get a coherent idea of some easy targets for mathlib. For example (although not directly related to the perfectoid project) I would imagine it would be relatively easy to define PID's now and prove that Euclidean domains are PID's and that PID's are UFD's. My feeling is that achievable goals like this should be on some sort of informal list somewhere. Once the p-adic numbers get accepted then defining the adeles of a number field should also be on this list (and if people aren't happy with a definition being on the list then I can propose a random simple theorem about adeles, but for me a definition is fine). Where should such a list live? I remember once, when I was thinking about formalising my graduate course of earlier this year, I thought about formalising the adeles and I made it an issue in mathlib, but now I realise that probably there is a huge list of little things which I'd like to see in mathlib (several of which I'll probably end up doing myself) and I don't think it's sane to have an issue for each of them.

#### Kevin Buzzard (Aug 25 2018 at 11:52):

I should perhaps say that as well as some easy targets I guess I might also end up listing some harder targets. Is there already a place for this? I've realised now that I want mathlib to become the new Bourbaki; that's what people are doing here, and that's the style that they're writing. I think it would be nice to help things along the way by having a list of goals.

#### Kevin Buzzard (Aug 25 2018 at 13:08):

I didn't notice that it already got merged! I was just leaving for a holiday the day it did

#### Kevin Buzzard (Aug 25 2018 at 14:43):

This is not works in progress -- this is stuff which I want there to be progress on :-)

#### Scott Morrison (Aug 25 2018 at 14:47):

I agree PIDs are gap that needs fixing soon! I've been suggesting my students @Jack Crawford and Ed Hofflin look at those, but as they're still getting started on Lean it may take a while.

#### Scott Morrison (Aug 25 2018 at 14:48):

Let's have a list on the leanprover-community wiki!

#### Kevin Buzzard (Aug 25 2018 at 14:51):

How does that work? If you start something, can other people edit it?

#### Scott Morrison (Aug 25 2018 at 14:51):

I think so --- everyone who has commit access on leanprover-community, and I think the intention is that everyone who wants to make PRs to mathlib can have this.

#### Scott Morrison (Aug 25 2018 at 14:52):

You should try editing the list I wrote for ideas of things to go over next week: https://github.com/leanprover-community/mathlib/wiki/Lean-in-Orsay,-2018

#### Reid Barton (Aug 25 2018 at 14:52):

My first thought would be to just use the github issue tracker. You can organize issues using labels, so I don't think having lots of "feature request" issues would be overwhelming.

#### Scott Morrison (Aug 25 2018 at 14:53):

What if we used issues on the main mathlib repository to indicate defects, and issues on the leanprover-community fork of mathlib for summaries of work in progress, or for wishlists?

#### Reid Barton (Aug 25 2018 at 14:58):

That's possible if that arrangement is clearly signposted somewhere (like, at the top of mathlib's README.md). I do like the idea of including entries for work-in-progress since we're already at the stage at which it can be hard to keep track of what everyone is working on.
Actually, brainstorming small projects of just the sort that Kevin mentioned is on my list of things to do next week, and part of the aim here is to give potential new contributors things to work on.

#### Reid Barton (Aug 25 2018 at 15:01):

For example, Zulip has the "good first issue" tag
https://github.com/zulip/zulip/issues?q=is%3Aopen+is%3Aissue+label%3A%22good+first+issue%22

#### Scott Morrison (Aug 25 2018 at 15:07):

Maybe it does make sense to have them all in one place...

#### Reid Barton (Aug 25 2018 at 15:09):

I'm kind of neutral about it. I do also see the appeal of keeping a separate list.

#### Reid Barton (Aug 25 2018 at 15:10):

BTW, one of the items on my wishlist is the structure theorem for f.g. modules over a PID. Guess I didn't realize there are no PIDs yet either :)

#### Scott Morrison (Aug 25 2018 at 15:13):

Smith normal form is a great project for someone who wants to learn how to do recursion well!

#### Jack Crawford (Aug 25 2018 at 15:24):

Yeah @Scott Morrison I’m pretty keen on tackling Smith Normal Form sometime soon, along with PIDs. (At least, after midsems next week)

#### Johan Commelin (Aug 25 2018 at 17:40):

Someone should also take a serious stab at algebraic closures.

#### Kevin Buzzard (Aug 25 2018 at 18:42):

I'm occasionally pestering @Kenny Lau to do these :-) Kenny -- can you give us an update of what needs to be done?

#### Kevin Buzzard (Aug 25 2018 at 18:43):

I think the issue is that there's some infrastructure which isn't there yet, but I've forgotten what.

#### Kevin Buzzard (Aug 25 2018 at 18:43):

For a while the hold-up was no robust theory of polynomials in 1 variable, but that is now done thanks to Chris.

splitting fields

boggle

#### Kevin Buzzard (Aug 25 2018 at 18:43):

Do you need all the facts about them?

#### Kevin Buzzard (Aug 25 2018 at 18:44):

I mean -- uniqueness? That's the annoying one

no

#### Kenny Lau (Aug 25 2018 at 18:44):

we don't even need minimality

#### Kevin Buzzard (Aug 25 2018 at 18:45):

Given a polynomial of degree n over a field K it's not too hard to prove by induction on n that there's a bigger field L contaning K where that polynomial factors into linear factors.

yeah

right

Is that tough?

Oh!

#### Kevin Buzzard (Aug 25 2018 at 18:46):

You need that K[X]/(irred poly) is a field.

#### Kenny Lau (Aug 25 2018 at 18:46):

and you also need to prove that K[X] is UFD

#### Kevin Buzzard (Aug 25 2018 at 18:46):

I don't think you need as much as that

#### Kevin Buzzard (Aug 25 2018 at 18:47):

Do you need uniqueness?

no

#### Kenny Lau (Aug 25 2018 at 18:47):

actually we don't need it to be a field

#### Kevin Buzzard (Aug 25 2018 at 18:47):

It suffices to prove we can add a root of a poly to a field and get a new field

given f

#### Kenny Lau (Aug 25 2018 at 18:47):

K[X]/(f) is a ring

#### Kenny Lau (Aug 25 2018 at 18:47):

now what do you do with rings

#### Kevin Buzzard (Aug 25 2018 at 18:47):

now take a max ideal

#### Kenny Lau (Aug 25 2018 at 18:47):

you quotient by a maximal ideal

right

genius

#### Kevin Buzzard (Aug 25 2018 at 18:48):

I think Chris proved quotient by a max ideal was a field, recently

#### Chris Hughes (Aug 25 2018 at 19:00):

Polynomials are a Euclidean domain is there. I don't think Euclidean implies PID and PID implies prime ideals are maximal is that hard.

#### Kenny Lau (Aug 25 2018 at 19:00):

also PID doesn't imply prime ideals are maximal

also s/is/are/

#### Johan Commelin (Aug 25 2018 at 19:04):

Would the following idea be an option. It's a bit of a hack, because of K : Type u, then K-bar : Type (u+1).

#### Johan Commelin (Aug 25 2018 at 19:05):

You let Alg(K) be the type of algebraic extensions of K, and then apply Zorn's lemma.

#### Johan Commelin (Aug 25 2018 at 19:05):

Maybe with some trickery you can even get K-bar back into Type u. I'm not an expert on this.

#### Johan Commelin (Aug 25 2018 at 19:07):

Anyway, whatever the definition, we will want a theorem that says that K-bar is unique up to iso.

#### Morenikeji Neri (Aug 26 2018 at 12:46):

I've actually defined PIDs and have a proof that compiles of ED -> PID (with some help from Chris) @Kevin Buzzard

#### Kenny Lau (Aug 26 2018 at 12:53):

great, now get it to mathlib :P

#### Scott Morrison (Aug 26 2018 at 13:08):

I saw that yesterday!

#### Scott Morrison (Aug 26 2018 at 13:08):

I'm hoping we can bring the proof down to something much smaller. After all, to explain it to a human is only a few lines!

Last updated: May 19 2021 at 02:10 UTC