Project for learning Lean

Stream: new members

[Thomas Lanard]

Hello,

With the team of Algebra and Geometry at the University of Versailles (France), we are very motivated to learn Lean and we are doing a study group. To do so, we would like to do a little project. Would you have any recommendations, that are suitable for beginners? If possible, if it is something that could contribute to the Lean community (mathlib) in the future it would be great.

Thank you in advance!

[Johan Commelin]

Welcome! Can you say a bit more about the mathematical level of the members of your group? 1st year students? Or PhD students? Something in between or beyond?

[Riccardo Brasca]

Welcome! At the beginning it is probably easier to prove theorems rather than to give new definition. Something in commutative algebra maybe?

[Thomas Lanard]

Thank you! We are around 10 people composed of researchers between PhD students and Professors, all in algebra, number theory, and geometry. Are there some interesting theorems or results in commutative algebra that are not already in Mathlib?

[Riccardo Brasca]

A random idea: projective modules over a local ring are free (without any noetherian/finite assumption). I don't think we have it.

[Riccardo Brasca]

But it's possible that the proof is a rather unpleasant transfinite induction...

[Kevin Buzzard]

Transfinite induction is delicate in lean, as Dagur found out when formalising the Nobeling result. Brian Conrad once told me a proof which avoided transfinite induction but I don't remember it any more :-( although I could just ask him again ...

I need finite flat group schemes for the FLT project. Are we ready for Cohen-Macauley/Gorenstein/complete intersection rings yet? Structure theorem for Artin semilocal rings? Structure theorem for fg modules over $\Z_p[[T]]$? Kummer theory? (that one is definitely accessible)

[Filippo A. E. Nuccio]

:thumbs_up: for the structure theorem of fg modules over $\mathbb{Z}_p[[T]]$!

[Antoine Chambert-Loir]

That's a very good and cool idea. Among possible topics, I think it should be possible to formalize the proof of Serre's non-conjecture that projective modules over a polynomial ring are free. I don't think that mathlib knows about dimension theory neither.

[Antoine Chambert-Loir]

Also, if you need help, tutorials, etc., I would be happy to help in some way or another.

[Kevin Buzzard]

@Jujian Zhang did you make any PRs for dimension theory?

[Riccardo Brasca]

Dimension theory is probably exactly the thing I wouldn't suggest to beginners (and this why we don't have it I think. Endless discussions about the dimension of an infinite dimensional thing. Is the dimension a cardinal? A natural number?)

[Riccardo Brasca]

Of course it is doable, but it can be annoying at the beginning.

[Thomas Lanard]

Great! Thank you very much for all these ideas!

[Kevin Buzzard]

Yes, Jujian had to make some decisions about that whole cardinal nonsense. You forgot the zero ring, which has dimension -infinity, which is neither a cardinal nor a natural number :-)

[Jujian Zhang]

Here is a branch containing some basic definition and results regarding dimension of rings and topological spaces

[Andrew Yang]

I didn't know that such a project exists! I also had some dimension theory here which contains krull's height theorem among other things.

[Yaël Dillies]

There was a reason why I told both of you to talk to each other :wink:

[Rubén Muñoz--Bertrand]

Thanks everybody for the answers! We saw that Weierstrass preparation theorem is needed for the proof of the structure theorem of fg modules over $\mathbb{Z}_{p}[[T]]$. It does not seem to be on Mathlib, or is it? Then it might be another idea for our first goal. Almost everybody in the group have never done any Lean, so we want something easy at first.

[Riccardo Brasca]

Weierstrass preparation for power series seems a good idea to start!

[Riccardo Brasca]

What you can do is to write (on paper) a precise formulation (for example I don't know over which rings it holds), and then try to state it.

[Riccardo Brasca]

You can have a look at this file (and files in the same folder) to see what we have about power series.

[Riccardo Brasca]

Power series in one variable are called PowerSeries R, where R is... well, it makes sense without any assumption on R, but Lean will automatically understand that PowerSeries R is, say, a ring if R is.

[Riccardo Brasca]

Then remember that a very important thing is to break your proof in as much as possible very very small steps. A normal math proof that becomes 50 or even 100 lemmas in Lean is nothing really special.

[Antoine Chambert-Loir]

Riccardo Brasca said:

Weierstrass preparation for power series seems a good idea to start!

I'm not sure it is possible now. Lean/mathlib is not very knowledgeable about power series, it lacks many basic results about evaluation, substitution, differentiation, etc. (Some of them are needed for our work with Maria Ines…).

[Antoine Chambert-Loir]

And regarding dimension (of noetherian rings or finitely generated algebras over a field), I do not agree with Riccardo on that point. There is much sensible work to do here, and you can set the dimension of something infinite dimensional to be either infinite (using docs#PartENat) or zero (as docs#Set.ncard does), together with a predicate IsFiniteDimensional, that will be totally fine. If people want/need to upgrade the theory to a cardinal, they're free to do so, but since almost no mathematical theory exists on this matter, I believe that you're safe. (The same discussion exists for the length of modules; if you want to go out of the realm of modules of finite length, you can take ascending chains, descending chains, index them by integers, ordinals, you'll get genuinely different answers…)

[Riccardo Brasca]

Do we really need that much for weirstrass preparation? Anyway writing down a very detailed mathematical proof should be the first step anyway, then we can check what we are missing (of course we will be missing something).

[Riccardo Brasca]

Concerning dimension I raised the question because it's not the first time we speak about it, and this problem has already been pointed out .

[Filippo A. E. Nuccio]

FWIW let me mention here that as part of our project with @María Inés de Frutos Fernández we formalize a proof that the Laurent series over a field are the $T$-adic completion of the rational functions and we deduce that the polynomials are dense in the power series. That this only happens over a field is because all this comes from valuations on Dedekind domains, and $R[T]$ is one such DD only for fields...

[Antoine Chambert-Loir]

With the general definition of a topology on rings of power series (simple convergence for each coefficient, any topology on the ring of coefficients), this is basically obvious. We don't treat Laurent series, though, this may be a pity. This is docs#HahnSeries, but is it neatly interfaced with docs#MvPowerSeries? (For Hahn series, I don't expect the correct topology to be given by simple convergence, but rather the inductive limit of the topologies of simple convergence on series with order at least something.)