New Member - Clarification questions

Stream: new members

[Thomas Moulin]

Hi everyone, I discovered lean a couple months ago and wanted to contribute to it's development. I had a project in lean and it made me love the language and the community arround it.

I am curious about how the Undergrad math in mathlib and Undergrad math not in mathlib pages work: on both pages it says "To update this list, please submit a PR modifying docs/undergrad.yaml in the mathlib repository." and when clicking on it both pages go to the same github file.
My confusion comes from the fact that it feels like the two webpages should redirect to two separate lists, or there is something I don't understand?

Thanks!
Thomas

[Ruben Van de Velde]

It's one list that is used to generate two web pages

[Snir Broshi]

excercpt from https://github.com/leanprover-community/mathlib4/blob/master/docs/undergrad.yaml:

  Duality:
    dual vector space: 'Module.Dual'
    dual basis: 'Module.Basis.dualBasis'
    transpose of a linear map: 'Module.Dual.transpose'
    orthogonality: 'https://en.wikipedia.org/wiki/Dual_space#Quotient_spaces_and_annihilators'

Some concepts have names of definitions or theorems, others just a wikipedia link

[Thomas Moulin]

Oooh I see thank you very much

[Julian Berman]

Can I ask which course you were in which had a project in Lean (I've been trying to drum up some interest or perhaps an informal meetup on Lean around campus.)

[Thomas Moulin]

The course just changed it was previously a quantum error correction course and is now machine assisted maths

[Thomas Moulin]

About mathlib, I would like to work on the missing linear algebra more specifically on endomorphisms. The thing is when looking up stuff that already exists regarding endormophisms, contrary to matrices there is not a specific folder for them. Some topics are directly inside the linear algebra folder (eigenvalue), some have their own folder (minpoly the website redirects towards the field theory folder but there exists also a minpoly.lean file under the linear algebra/eigensapce folder (a bit confused about that one)), some are inside the matrix directory.
Where should I start for the kernels lemma ? maybe it is not a good idea idk, i just love this theorem lol

[Snir Broshi]

What do you mean by "kernels lemma"?

[Snir Broshi]

And what are you looking for specifically for minimal polynomials or eigenvalues? Have you found something missing that you'd like to work on?

[Thomas Moulin]

The lemme des noyaux the english name for that seems confusing, the wikipedia page doesn't have an english equivalent.
The thing missing I would like to work on is the kernels lemma, as it is indicated on the missing undergraduate in mathlib web page, I was just confused about what should be put where
image.png

[Thomas Moulin]

image.png
example of what confuses me:
LinearAlgebra>Eigenspace>Matrix.lean, Charpoly.lean, Minpoly.lean
and then
LinearAlgebra>Matrix>Charpoly>Minpoly.lean
I feel like I don't understand of stuff should be organised
Maybe there are rules that I missed ?

[Snir Broshi]

Well there's a split between theorems that use or don't use matrices

[Snir Broshi]

Thomas Moulin said:

The lemme des noyaux the english name for that seems confusing, the wikipedia page doesn't have an english equivalent.

Cool, I've never heard of this lemma before! The undergrad list is derived from the French curriculum which explains why it's there, it's strange that other places don't teach it.
If it helps, I've seen online someone mention that the lemma is a special case of the Lasker–Noether theorem, which does exist in Mathlib. Maybe it can help you prove the lemma.

[Thomas Moulin]

Snir Broshi said:

Well there's a split between theorems that use or don't use matrices

Hooo i see, do you know a place that explains this kind of separations ? I tried looking here but didn't find the file structure explained

[Thomas Moulin]

Snir Broshi said:

Thomas Moulin said:

The lemme des noyaux the english name for that seems confusing, the wikipedia page doesn't have an english equivalent.

Cool, I've never heard of this lemma before! The undergrad list is derived from the French curriculum which explains why it's there, it's strange that other places don't teach it.
If it helps, I've seen online someone mention that the lemma is a special case of the Lasker–Noether theorem, which does exist in Mathlib. Maybe it can help you prove the lemma.

Alright thanks! Where do you suggest I start working inside the folder hierarchy ?

[Snir Broshi]

Well first you state some results and maybe prove a few, and place them near similar results.
If the place you found is missing imports that your theorems need, then consider moving it to another file that already has those imports. If you didn't find a file with such imports that also seems related to what you're proving, create a new file and place it in a folder that makes sense.
People make folders when there are multiple files that are related. It's kinda vibe based, and if you're doing something strange then don't worry, reviewers will point you in the right direction in your PR.

[Thomas Moulin]

Should I announce somewhere that I am working on that ? like making an issue or an empty WIP PR, so that people can join and we avoid making twice the same thing

[Snir Broshi]

I'd go for less of an announcement and more of a "hey, I'm planning to work on this, is there something I should know? Were there previous attempts? Is anyone working on this?" in #mathlib4 or #Is there code for X?
I don't think many people watch WIP PRs or issues, OTOH you can make a WIP PR and ask for guidance on stuff occasionally then people can see and work with the current state of your code.
I think it's personal preference, I don't use WIP PRs. It happened once where I made the same thing as someone else, but it worked out great, we took the best of both our solutions (I threw most of mine away).

[Snir Broshi]

Here's my attempt at formalizing the statement of the kernels lemma from Wikipedia, if it helps you getting started:

import Mathlib
open Polynomial

variable {ι K E : Type*} [CommSemiring K] [AddCommMonoid E] [Module K E]
variable (f : Module.End K E) (s : Finset ι) (P : ι → K[X])
variable (h : (s : Set ι).Pairwise <| IsCoprime.onFun P)

theorem kernels_lemma_attempt : (s.prod P |>.smeval f |>.ker) = ⨆ i, (P i |>.smeval f |>.ker) := by
  sorry

[Snir Broshi]

I'm not sure I haven't gotten things wrong, but it's a start I guess

[Thomas Moulin]

Thank you very much for all these answers !