## Stream: new members

### Topic: Project for learning Lean

#### Thomas Lanard (Nov 13 2023 at 13:18):

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.

#### Johan Commelin (Nov 13 2023 at 13:21):

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 (Nov 13 2023 at 13:22):

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

#### Thomas Lanard (Nov 13 2023 at 13:30):

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 (Nov 13 2023 at 13:32):

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 (Nov 13 2023 at 13:33):

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

#### Kevin Buzzard (Nov 13 2023 at 13:56):

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 (Nov 13 2023 at 15:00):

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

#### Antoine Chambert-Loir (Nov 13 2023 at 15:15):

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 (Nov 13 2023 at 15:15):

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

#### Kevin Buzzard (Nov 13 2023 at 15:21):

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

#### Riccardo Brasca (Nov 13 2023 at 15:40):

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 (Nov 13 2023 at 15:41):

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

#### Thomas Lanard (Nov 13 2023 at 16:07):

Great! Thank you very much for all these ideas!

#### Kevin Buzzard (Nov 13 2023 at 16:50):

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 (Nov 13 2023 at 17:39):

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

#### Andrew Yang (Nov 14 2023 at 04:31):

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 (Nov 14 2023 at 14:30):

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

#### Rubén Muñoz--Bertrand (Nov 14 2023 at 15:12):

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 (Nov 14 2023 at 15:15):

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

#### Riccardo Brasca (Nov 14 2023 at 15:16):

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 (Nov 14 2023 at 15:18):

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

#### Riccardo Brasca (Nov 14 2023 at 15:19):

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 (Nov 14 2023 at 15:23):

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 (Nov 14 2023 at 17:32):

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 (Nov 14 2023 at 17:35):

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 (Nov 14 2023 at 18:03):

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 (Nov 14 2023 at 18:04):

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 (Nov 14 2023 at 19:02):

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 (Nov 16 2023 at 15:18):

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

Last updated: Dec 20 2023 at 11:08 UTC