Zulip Chat Archive

Stream: general

Topic: Undergraduate math list


Patrick Massot (May 12 2020 at 19:41):

One the website we have a mathlib overview. Among the problems of this list are:

  • It is outdated and needs constant maintaince (spoiler: I won't propose a magic fix, we only need to care more about this list)
  • It doesn't tell where are all those things, and we all know that navigating mathlib is difficult
  • It doesn't point out missing things, and we have many people who want to start contributing, preferably easy things

Of course the list of missing things is open-ended. But we have a well-known half-specified milestone: covering all of undergraduate mathematics. So we could list missing undergraduate stuff, either in the main list (printed in red) or in a separate list.

Patrick Massot (May 12 2020 at 19:41):

In France we have a standard formatted list of undergraduate topics: the topics that are required for the agrégation, the French national exam for would be high school teachers. It changes slightly from year to year, but here is the 2020 version. It would be a very convenient first approximation, and we could modify it of course. I translated the first section (groups) and formatted it into the yaml file below. Turning that file into a webpage that looks like the mathlib overview but with links and separating missing stuff is a trivial programming exercise. My questions are: should I keep translating this list? Will there be people helping me by filling in links that I missed and editing the YaML file?

Patrick Massot (May 12 2020 at 19:42):

group:
  basic definitions:
    group: 'https://github.com/leanprover-community/lean/blob/master/library/init/algebra/group.lean#L35'
    group morphism: 'https://leanprover-community.github.io/mathlib_docs/algebra/group/hom.html'
    direct product of groups: 'https://leanprover-community.github.io/mathlib_docs/algebra/group/prod.html'
    subgroup: 'https://leanprover-community.github.io/mathlib_docs/group_theory/subgroup.html'
    subgroup generated by a subset: 'https://leanprover-community.github.io/mathlib_docs/group_theory/subgroup.html#group.closure'
    order of an element: 'https://leanprover-community.github.io/mathlib_docs/group_theory/order_of_element.html'
    normal subgroup: 'https://leanprover-community.github.io/mathlib_docs/group_theory/subgroup.html#normal_subgroup'
    quotient group: 'https://leanprover-community.github.io/mathlib_docs/group_theory/quotient_group.html#quotient_group.group'
    group action: 'https://leanprover-community.github.io/mathlib_docs/group_theory/group_action.html#mul_action'
    stabilizer of a point: 'https://leanprover-community.github.io/mathlib_docs/group_theory/group_action.html#mul_action.stabilizer'
    orbit: 'https://leanprover-community.github.io/mathlib_docs/group_theory/group_action.html#mul_action.orbit'
    quotient space: 'https://leanprover-community.github.io/mathlib_docs/group_theory/group_action.html#mul_action.orbit_equiv_quotient_stabilizer'
    class formula: ''
    conjugacy classes: ''
  abelian group:
    cyclic group: ''
    finite type abelian groups: ''
    complex roots of unity: ''
    primitive complex roots of unity: ''
  permutation group:
    permutation group of a type: 'https://leanprover-community.github.io/mathlib_docs/data/equiv/basic.html#equiv.perm'
    decomposition into transpositions: ''
    decomposition into cycles with disjoint support: ''
    signature: 'https://leanprover-community.github.io/mathlib_docs/group_theory/perm/sign.html#equiv.perm.sign'
    alternating group: ''
  classical automorphim groups:
    general linear group: 'https://leanprover-community.github.io/mathlib_docs/linear_algebra/basic.html#linear_map.general_linear_group'
    special linear group: 'https://leanprover-community.github.io/mathlib_docs/linear_algebra/special_linear_group.html'
    orthogonal group: ''
    special orthogonal group: ''
    unitary group: ''
    special unitary group: ''
  representation theory for finite groups:
    representations of abelian groups: ''
    Maschke theorem: ''
    orthogonality of irreducible characters: ''
    Fourier transform for finite abelian groups: ''
    convolution: ''
    examples for groups with a small cardinal: ''

Rob Lewis (May 12 2020 at 19:54):

I've always kind of hated the mathlib overview page (and the theories pages) because they so trivially go out of date. This looks like a step forward at least. With a fixed list of what should be there, it's easier to see when it needs to be updated.

Rob Lewis (May 12 2020 at 19:54):

But really, we need someone to take charge of this list and promise to keep it updated.

Patrick Massot (May 12 2020 at 20:04):

I think the existence of a fixed list would make it much easier. And people keep asking for projects to work on.

Yury G. Kudryashov (May 12 2020 at 20:29):

Some links point to the source code, some point to docs website. Is there any specific reason?

Patrick Massot (May 12 2020 at 21:09):

If I didn't mess up, only the core lib stuff points to code, because it has no doc.

Yury G. Kudryashov (May 12 2020 at 21:12):

https://leanprover-community.github.io/mathlib_docs/core/init/algebra/group.html

Patrick Massot (May 12 2020 at 21:22):

So you can start fixing my list. I'm sure I've also missed stuff that we already have.

Patrick Massot (May 12 2020 at 21:25):

I pushed my file to https://github.com/leanprover-community/leanprover-community.github.io/blob/newsite/data/overview.yaml. It isn't used for anything yet, but everybody can already fix things there.

Patrick Massot (May 12 2020 at 21:26):

Let's make it a test. We have one obvious suboptimal link, and a least a couple of holes that are either already here or trivial to fill. Let's see if we can get contributions there. If yes then I'll translate all the other sections.

Patrick Massot (May 12 2020 at 21:29):

I should also point out that one advantage of this list with precise pointers to the doc (preferably specific items rather that whole pages when it makes sense) is that we can have CI hunting for broken links at every commit. So that page would become outdated only because of additions to mathlib, not because of refactors.

Johan Commelin (May 13 2020 at 06:08):

@Patrick Massot I think this is a very good idea. I'll try my best to contribute, and keep contributing.

Yury G. Kudryashov (May 13 2020 at 06:09):

Should I push or PR?

Yury G. Kudryashov (May 13 2020 at 06:15):

I'd strip the common prefix from all URLs.

Bryan Gin-ge Chen (May 13 2020 at 06:15):

I'd say push unless there's something you want to discuss or have reviewed.

Johan Commelin (May 13 2020 at 06:22):

I think the broken link detector is a must btw.

Yury G. Kudryashov (May 13 2020 at 22:23):

I fixed some URLs and translated 1.1.

Bryan Gin-ge Chen (May 13 2020 at 23:00):

Should we have space for some notes in the YAML in addition to just URLs, in case mathlib's treatment of those topics deserves additional explanation?

Johan Commelin (May 14 2020 at 03:56):

Sounds good. And isn't YAML flexible enough to just drop those notes in?
So you write

  'cyclic_group' : blablaURL
-- or
  'cyclic_group':
    - URL: blablaURL
    - note: '''some note'''

and the script can just figure out which of the two was used?
(Me doesn't know yaml too well.)

Yury G. Kudryashov (May 14 2020 at 03:59):

BTW, why do we need YAML, and not markdown with predictable structure?

Bryan Gin-ge Chen (May 14 2020 at 04:02):

I guess Patrick is thinking of parsing the YAML in Python and building pages from some templates somehow.

Yury G. Kudryashov (May 14 2020 at 04:03):

OK, let's have a YaML file

Yury G. Kudryashov (May 14 2020 at 04:04):

BTW, do we have an undergraduate student speaking French?

Yury G. Kudryashov (May 14 2020 at 04:06):

If yes, I wonder if this student will volunteer to translate the whole document. It's not too much work but I think that Patrick is overqualified for this job.

Yury G. Kudryashov (May 14 2020 at 04:07):

(i.e., he could use this time for something else that an undergraduate can't do)

Yury G. Kudryashov (May 14 2020 at 04:07):

Or I can translate in a comment, and let a student turn it into a list with links.

Patrick Massot (May 14 2020 at 08:10):

Yury G. Kudryashov said:

If yes, I wonder if this student will volunteer to translate the whole document. It's not too much work but I think that Patrick is overqualified for this job.

To be honest I feel I'm overqualified to write format_lean, leancrawler and leanproject, and rewriting the whole website infrastructure. One difference here is an undergrad may actually learn stuff about math and mathlib, so maybe I should dare suggest that @Ryan Lahfa would be perfect for this job.

Patrick Massot (May 14 2020 at 08:12):

Bryan Gin-ge Chen said:

Should we have space for some notes in the YAML in addition to just URLs, in case mathlib's treatment of those topics deserves additional explanation?

How would you like them to be displayed in the end? Actually I don't like this idea. I think this information should be in either in the module docstrings or in the theories folder if it needs to be really long.

Ryan Lahfa (May 14 2020 at 13:30):

Patrick Massot said:

Yury G. Kudryashov said:

If yes, I wonder if this student will volunteer to translate the whole document. It's not too much work but I think that Patrick is overqualified for this job.

To be honest I feel I'm overqualified to write format_lean, leancrawler and leanproject, and rewriting the whole website infrastructure. One difference here is an undergrad may actually learn stuff about math and mathlib, so maybe I should dare suggest that Ryan Lahfa would be perfect for this job.

I definitely can

Ryan Lahfa (May 14 2020 at 13:32):

Though, I don't really enjoy writing YAML and prefer TOML nowadays but that is a taste matter (and endless nights fighting with Ansible…)

ROCKY KAMEN-RUBIO (May 14 2020 at 13:37):

I'm happy to help with French->English translation. You just want 2020 version of the national exam topics linked in the original post right?

Patrick Massot (May 14 2020 at 13:57):

I don't care at all about YaML vs toml, especially if I'm not the one doing the translation. But I have a hard time thinking how the format could be simpler than what I wrote in https://github.com/leanprover-community/leanprover-community.github.io/blob/newsite/data/overview.yaml

Patrick Massot (May 14 2020 at 13:59):

It's great that both of you want to help here. Please coordinate to avoid duplicating efforts. You can either translate without caring about what's in mathlib or do both at the same time (but please don't cheat like Johan was tempted to.

Ryan Lahfa (May 14 2020 at 14:04):

Patrick Massot said:

I don't care at all about YaML vs toml, especially if I'm not the one doing the translation. But I have a hard time thinking how the format could be simpler than what I wrote in https://github.com/leanprover-community/leanprover-community.github.io/blob/newsite/data/overview.yaml

Indeed

Ryan Lahfa (May 14 2020 at 14:07):

Do we agree that real analysis should be in that overview list?

Ryan Lahfa (May 14 2020 at 14:08):

Like "Heine theorem", "continuity", etc.

Johan Commelin (May 14 2020 at 14:22):

I think the plan is to put everything from http://media.devenirenseignant.gouv.fr/file/agreg_externe/59/7/p2020_agreg_ext_maths_1107597.pdf into the YAML file. And then present it as a challenge to mathlib users to make sure that every item has a corresponding entry in mathlib.

Johan Commelin (May 14 2020 at 14:23):

To prevent the cheating, it might be easier to do a "dumb" translation first, without adding links to mathlib.

Patrick Massot (May 14 2020 at 14:27):

Ryan Lahfa said:

Like "Heine theorem", "continuity", etc.

This is all on pages 4 and 5.

Ryan Lahfa (May 14 2020 at 14:40):

Patrick Massot said:

Ryan Lahfa said:

Like "Heine theorem", "continuity", etc.

This is all on pages 4 and 5.

Okay, perfect ; it's clear now in my head

Ryan Lahfa (May 14 2020 at 14:43):

@ROCKY KAMEN-RUBIO What we can do is, I can let you backfill the current English version for links (if there's any), while I rewrite the overview_fr.yaml with french text and copy the current links over, and then, I add as much stuff as I can from the France teaching program, then you can translate it to the English version and get the links I found
We can do some iterations of this algorithm which is somewhat guaranteed to finish in few PRs

Ryan Lahfa (May 14 2020 at 15:04):

Quick question, @Patrick Massot @Yury G. Kudryashov wouldn't we want something like real internationalisation in the future? With something like https://weblate.org/ (they provide free instances for open source) and it's able to do automatic commits for i18n, with various review mechanisms

Patrick Massot (May 14 2020 at 15:05):

What would you want to translate? Here the goal is not to have both a French and and English version

Johan Commelin (May 14 2020 at 15:05):

I personally wouldn't worry about it too much.

Patrick Massot (May 14 2020 at 15:06):

It's simply that the convenient data set I was able to find happens to be in French

Ryan Lahfa (May 14 2020 at 15:06):

Patrick Massot said:

What would you want to translate? Here the goal is not to have both a French and and English version

Ah — Okay, it's a French → English translation only, I thought there was a goal to have a overview_fr.yaml, my apologies

Johan Commelin (May 14 2020 at 15:06):

We just want a long list that is a "certified and stamped" list of things that appear in an undergrad curriculum. And then pointers to mathlib.

Ryan Lahfa (May 14 2020 at 15:06):

Sorry for the confusion, okay, I'm writing it now then

Patrick Massot (May 14 2020 at 15:12):

I can see Ryan totally entered translator mode. He'll have a lot of fun once https://github.com/mpedramfar/Lean-game-maker/pull/12 will be merged. He'll be able to continue the work stated in https://github.com/ImperialCollegeLondon/natural_number_game/pull/83

ROCKY KAMEN-RUBIO (May 14 2020 at 17:38):

Ryan Lahfa said:

ROCKY KAMEN-RUBIO We can split the work in:
— I give you page 5 and later
— I take page < 5

Sounds good! Should we setup a shared doc to have consistent formatting?

Patrick Massot (May 19 2020 at 08:37):

@ROCKY KAMEN-RUBIO and @Ryan Lahfa, are you making any progress here?

ROCKY KAMEN-RUBIO (May 19 2020 at 15:45):

I have a draft I'll post shortly. Just tidying up some formatting

Ryan Lahfa (May 19 2020 at 16:23):

Patrick Massot said:

ROCKY KAMEN-RUBIO and Ryan Lahfa, are you making any progress here?

I have written some, I planned to get a working part of this today/tonight ; do you prefer small PR/improvements or rather a large PR implementing everything for this kind of changes?

Jalex Stark (May 19 2020 at 16:44):

the sooner you post any work, the less duplication of effort there will be, and the faster other people can make small contributions

Johan Commelin (May 19 2020 at 16:52):

Yup, nothing wrong with 37 small PRs!

ROCKY KAMEN-RUBIO (May 19 2020 at 18:34):

Here's my (still somewhat rough) draft
Aggregation_2020.pdf

ROCKY KAMEN-RUBIO (May 19 2020 at 18:35):

I'm still working on some of the grittier formatting. Let me know if anything is conceptually incorrect, or if you have any other suggestions.

Jalex Stark (May 19 2020 at 18:37):

? working hard on formatting a pdf seems wrong, since the final goal will be markdown that lives somewhere in the mathlib docs or the leanprover community website
(more to the point : post source code!)

Bryan Gin-ge Chen (May 19 2020 at 18:46):

Even better: I suggest opening a PR at the website repo which makes additions / edits to https://github.com/leanprover-community/leanprover-community.github.io/blob/newsite/data/overview.yaml

Bryan Gin-ge Chen (May 19 2020 at 18:48):

Patrick Massot said:

In France we have a standard formatted list of undergraduate topics: the topics that are required for the agrégation, the French national exam for would be high school teachers. It changes slightly from year to year, but here is the 2020 version. It would be a very convenient first approximation, and we could modify it of course. I translated the first section (groups) and formatted it into the yaml file below. Turning that file into a webpage that looks like the mathlib overview but with links and separating missing stuff is a trivial programming exercise. My questions are: should I keep translating this list? Will there be people helping me by filling in links that I missed and editing the YaML file?

See this part of the first message in this thread.

ROCKY KAMEN-RUBIO (May 19 2020 at 18:48):

Jalex Stark said:

? working hard on formatting a pdf seems wrong, since the final goal will be markdown that lives somewhere in the mathlib docs or the leanprover community website
(more to the point : post source code!)

I guess by "grittier formatting" I meant things on the level of "clarifying that this is an exponent". I'll post my source code

ROCKY KAMEN-RUBIO (May 19 2020 at 18:49):

Aggregation_2020.tex

ROCKY KAMEN-RUBIO (May 19 2020 at 18:51):

Bryan Gin-ge Chen said:

Patrick Massot said:

In France we have a standard formatted list of undergraduate topics: the topics that are required for the agrégation, the French national exam for would be high school teachers. It changes slightly from year to year, but here is the 2020 version. It would be a very convenient first approximation, and we could modify it of course. I translated the first section (groups) and formatted it into the yaml file below. Turning that file into a webpage that looks like the mathlib overview but with links and separating missing stuff is a trivial programming exercise. My questions are: should I keep translating this list? Will there be people helping me by filling in links that I missed and editing the YaML file?

See this part of the first message in this thread.

Oh I see, don't know how I missed that. I can start putting this into the .yaml file too.

ROCKY KAMEN-RUBIO (May 20 2020 at 04:44):

Ok I added the definitions from sections 5 and on as a PR. I think there are redundancies, and some definitions that could be organized better, but it's a start.
https://github.com/leanprover-community/leanprover-community.github.io/compare/newsite...iceplant:patch-1

Bryan Gin-ge Chen (May 20 2020 at 04:52):

Great! Do you mind opening a PR? It will be easier for us to make comments and suggestions on it that way.

ROCKY KAMEN-RUBIO (May 23 2020 at 03:30):

Bryan Gin-ge Chen said:

Great! Do you mind opening a PR? It will be easier for us to make comments and suggestions on it that way.

I thought I opened a PR but apparently I am still a git noob and only branched. I just opened a PR for real.

Bryan Gin-ge Chen (May 23 2020 at 03:44):

Thank you! Here's the PR link for those who don't happen to be watching the repo: https://github.com/leanprover-community/leanprover-community.github.io/pull/26

ROCKY KAMEN-RUBIO (May 23 2020 at 18:01):

I'm trying to expand links to the real analysis section since I just finished @Patrick's tutorial, but I'm noticing many of the definitions are in an auxiliary file he wrote (like the definition of a convergent sequence) and I'm having trouble finding them in mathlib. Is that because they just don't exist there yet, or am I not looking in the right place?

Jalex Stark (May 23 2020 at 18:04):

if I go to the mathlib docs site and search for "cauchy sequence", i get useful results
https://leanprover-community.github.io/mathlib_docs/

Jalex Stark (May 23 2020 at 18:06):

probably the biggest barrier for you personally contributing here is in "know the words a mathematician might say"

Patrick Massot (May 23 2020 at 18:47):

Rocky, everything which features in the tutorial is in mathlib except for stuff used in the very last file that I haven't found time to PR. However what is in mathlib can be very hard to recognize if you know only about the elementary theory. But other people can fill this. Are you done with the translation?

Patrick Massot (May 23 2020 at 18:48):

And there is no point in trying to put links to mathlib before you resolve all the issues at https://github.com/leanprover-community/leanprover-community.github.io/pull/26

Yury G. Kudryashov (May 23 2020 at 18:53):

Many definitions and theorems about limits in mathlib are formulated in a very general form (e.g. using filters, uniformity structure, or metric_spaces).

ROCKY KAMEN-RUBIO (May 23 2020 at 19:16):

Yury G. Kudryashov said:

Many definitions and theorems about limits in mathlib are formulated in a very general form (e.g. using filters, uniformity structure, or metric_spaces).

That that explains a lot. I'll leave that section to others who understand this better then. Any suggestions on how to better understand these ideas? I'm familiar with filters in Haskell but haven't used them in Lean.

Patrick Massot said:

Rocky, everything which features in the tutorial is in mathlib except for stuff used in the very last file that I haven't found time to PR. However what is in mathlib can be very hard to recognize if you know only about the elementary theory. But other people can fill this. Are you done with the translation?

I finished the translation, did a rudimentary formatting sweep, and submitted a PR. Let me know if there's anything else I can do!

Patrick Stevens (May 23 2020 at 19:42):

Filters are defined in order.filter.basic - they're not the same thing as List.filter : (a -> bool) -> List a -> List a. A filter on a set U is a way of defining what it means for a subset of U to be "large and not small" in whatever sense you need "large" to mean, satisfying by definition certain "large" properties. Namely: U is itself large; a superset of a large set is large; and if you intersect two large sets then you still have a large set (that is what I meant by "not small"). It turns out to be possible to define analysis using filters on the naturals; this is closely linked to Robinson's rather lovely formulation of nonstandard analysis, but it's all very much not how you're initially taught to think about analysis, so don't expect the path to understanding to be quick. I had a quick skim of https://arxiv.org/pdf/1212.5740.pdf and it seemed reasonable

Bryan Gin-ge Chen (May 23 2020 at 19:44):

@Kevin Buzzard has a blogpost on filters here.

Patrick Massot (May 23 2020 at 19:53):

@Patrick Stevens The use of filters in mathlib has nothing to do with non-standard analysis. I think it is very unfortunate that filters can be used in non-standard analysis, since this gives a bad reputation to filters, whereas filters were nice and useful long before this application.

Jalex Stark (May 23 2020 at 20:01):

Some of my friends said that looking at a proof of tychonoff's theorem with filters and one without filters was the key to getting them onto the filter train

Jalex Stark (May 23 2020 at 20:02):

ROCKY KAMEN-RUBIO said:

I finished the translation, did a rudimentary formatting sweep, and submitted a PR. Let me know if there's anything else I can do!

I think patrick already suggested "resolve the issues raised at your PR" as a course of action

ROCKY KAMEN-RUBIO (May 23 2020 at 20:12):

Jalex Stark said:

ROCKY KAMEN-RUBIO said:

I finished the translation, did a rudimentary formatting sweep, and submitted a PR. Let me know if there's anything else I can do!

I think patrick already suggested "resolve the issues raised at your PR" as a course of action

I believe I resolved all the issues that were raised (to the best of my abilities, Ryan brought up some nuance in terminology that I'm not super familiar with). Is that not showing up?

Ryan Lahfa (May 23 2020 at 20:18):

ROCKY KAMEN-RUBIO said:

Jalex Stark said:

ROCKY KAMEN-RUBIO said:

I finished the translation, did a rudimentary formatting sweep, and submitted a PR. Let me know if there's anything else I can do!

I think patrick already suggested "resolve the issues raised at your PR" as a course of action

I believe I resolved all the issues that were raised (to the best of my abilities, Ryan brought up some nuance in terminology that I'm not super familiar with). Is that not showing up?

Let me check

Ryan Lahfa (May 23 2020 at 20:19):

AFAIK, our comments are still there

Ryan Lahfa (May 23 2020 at 20:19):

Some of them are nuance in terminology, but others are just little typos (Euler for instance)

Patrick Massot (May 23 2020 at 20:24):

Rocky, if you don't see the "Outdated" label in yellow as in
image.png
then you probably didn't fix an issue. Once an issue is fixed, there are two options: if you are sure you fixed it, then click the "Resolve conversation" button. Otherwise post a comment saying you tried to fix it but you're not sure

Patrick Massot (May 23 2020 at 20:24):

The picture shows both the oudated label and the "Resolve conversation" button

ROCKY KAMEN-RUBIO (May 23 2020 at 21:24):

I closed most of the issues. @Ryan Lahfa I responded to your two comments that I didn't resolve.

Ryan Lahfa (May 23 2020 at 21:33):

@ROCKY KAMEN-RUBIO Answered to the 2nd comment, the 1st one can be fixed in the next PR

Ryan Lahfa (May 23 2020 at 21:33):

@Bryan Gin-ge Chen Let us know if you like the new PR, so that I can start adding stuff on the top of it

Bryan Gin-ge Chen (May 23 2020 at 21:45):

@ROCKY KAMEN-RUBIO Thanks for all the fixes! @Ryan Lahfa I'll merge it now to let you work on it.

Ryan Lahfa (May 23 2020 at 21:46):

Appreciate it!

Ryan Lahfa (May 23 2020 at 21:53):

So the first thing is this:
https://github.com/leanprover-community/leanprover-community.github.io/pull/27
I'll do a parallel PR for backfilling links wherever I can

Ryan Lahfa (May 23 2020 at 21:54):

Then, maybe we can get feedback from the people in this feed at the same time on capitalization/unicode/should include LaTeX or not/etc of some points.

Ryan Lahfa (May 23 2020 at 23:37):

https://github.com/leanprover-community/leanprover-community.github.io/pull/28

Ryan Lahfa (May 29 2020 at 23:14):

https://github.com/leanprover-community/leanprover-community.github.io/pull/33 here's a PR to generate the overview page
@Bryan Gin-ge Chen @Johan Commelin I might be looking for your feedback if you will :pray:

Ryan Lahfa (May 29 2020 at 23:39):

I rebased https://github.com/leanprover-community/leanprover-community.github.io/pull/28 and we can merge it if we want, I think getting as much links as possible even in small increments/PRs seems a good strategy

Bryan Gin-ge Chen (May 30 2020 at 00:27):

At a first glance the overview page PR looks pretty good. It looks like there's still some discussion occurring around the links. I don't want to merge before getting @Patrick Massot's opinion though.

Johan Commelin (May 30 2020 at 05:42):

Looks good to me! Thanks for all the effort!

Patrick Massot (May 30 2020 at 10:08):

Thanks a lot @Ryan Lahfa . This is not yet what I had in mind, but we are getting closer. I just let a review.

Patrick Massot (May 30 2020 at 10:11):

PS: Ryan, using / in a git branch name is a really bad idea. It interfere with remote/branch syntax

Patrick Massot (May 30 2020 at 10:14):

I merged this PR anyway because we really need people to be able to contribute to the yaml file, and the layout PR also had yaml syntactic fixes (mixing both in the same PR was also not the greatest idea).

Patrick Massot (May 30 2020 at 10:16):

But now I cannot merge https://github.com/leanprover-community/leanprover-community.github.io/pull/28 because of conflicts. @Ryan Lahfa could you fix that really soon? I don't want to steal your commit authorship by fixing things on my side.

Patrick Massot (May 30 2020 at 10:19):

I don't remember whether I wrote this publicly. But I would really really like this list to be ready to be seen on Wednesday. The reason is that I've been asked to give a propaganda talk at IAS on Wednesday.

Patrick Massot (May 30 2020 at 10:21):

So it would be really nice for the community if we could have a overview.yaml spring filling as many links as possible. You don't even need to know any git. You can simply hit the edit button (small pen in the top right corner) to propose new links.

Ryan Lahfa (May 30 2020 at 10:42):

Patrick Massot said:

But now I cannot merge https://github.com/leanprover-community/leanprover-community.github.io/pull/28 because of conflicts. Ryan Lahfa could you fix that really soon? I don't want to steal your commit authorship by fixing things on my side.

Yes, I'll do it

Ryan Lahfa (May 30 2020 at 10:43):

Patrick Massot said:

PS: Ryan, using / in a git branch name is a really bad idea. It interfere with remote/branch syntax

AFAIK, it should not, I have been using it for ≥ 5 years, it just works fine to do remote/xxx/yyy, have you a precise example in mind?

Patrick Massot (May 30 2020 at 10:44):

It prevents you to skip the remote part when you want to use the default remote

Ryan Lahfa (May 30 2020 at 10:47):

Do you mean like git merge xxx/yyy? It'll indeed use local branches rather than origin (or whatever is the default) branches, but I can change it and replace / by -

Ryan Lahfa (May 30 2020 at 10:47):

I answered to some of the comments on the overview generation PR

Ryan Lahfa (May 30 2020 at 10:48):

As I see it, the overview backfilling links PR is fine, and should not require any further rebasing over newsite (?), so it can be merged

Patrick Stevens (May 30 2020 at 10:48):

It's also annoying in general for anyone who wants to do programmatic manipulation of git branches - there's nothing to prevent you naming a branch refs/heads/branchname if you want, but it similarly forces the tool-writer to get their manipulations exactly right. If the user had just not put any slashes in, the problem would be so simple, you could just split on the / character no matter what style of ref you were given

Patrick Stevens (May 30 2020 at 10:49):

(I have strong opinions on this - if / were simply a disallowed character in branch names, the whole system would be so much less complex)

Ryan Lahfa (May 30 2020 at 10:49):

Patrick Stevens said:

It's also annoying in general for anyone who wants to do programmatic manipulation of git branches - there's nothing to prevent you naming a branch refs/heads/branchname if you want, but it similarly forces the tool-writer to get their manipulations exactly right. If the user had just not put any slashes in, the problem would be so simple, you could just split on the / character no matter what style of ref you were given

But anyway, as it is possible, that sounds like sane to me for tool authors to not rely on this kind of behavior and perform exact manipulation, as they would have all the "information"

Ryan Lahfa (May 30 2020 at 10:49):

Patrick Stevens said:

(I have strong opinions on this - if / were simply a disallowed character in branch names, the whole system would be so much less complex)

I don't have a good visual image of how complex the system is due to this, I don't know enough git internals

Ryan Lahfa (May 30 2020 at 10:50):

I'll fix it in my further PRs/branches :)

Patrick Massot (May 30 2020 at 10:50):

Ryan Lahfa said:

As I see it, the overview backfilling links PR is fine, and should not require any further rebasing over newsite (?), so it can be merged

image.png

Patrick Massot (May 30 2020 at 10:50):

Ryan Lahfa said:

Do you mean like git merge xxx/yyy? It'll indeed use local branches rather than origin (or whatever is the default) branches, but I can change it and replace / by -

I mean git fetch

Ryan Lahfa (May 30 2020 at 10:51):

Patrick Massot said:

Ryan Lahfa said:

As I see it, the overview backfilling links PR is fine, and should not require any further rebasing over newsite (?), so it can be merged

image.png

My GitHub UI seems to be outdated/stuck, I'll rebase it again to ensure everything is fine

Ryan Lahfa (May 30 2020 at 10:52):

Done

Ryan Lahfa (May 30 2020 at 10:52):

Patrick Massot said:

Ryan Lahfa said:

Do you mean like git merge xxx/yyy? It'll indeed use local branches rather than origin (or whatever is the default) branches, but I can change it and replace / by -

I mean git fetch

Okay, that's a fair point :-)

Patrick Massot (May 30 2020 at 10:55):

Thanks for rebasing. I merged it. So now everybody can contribute to filling more links.

Ryan Lahfa (May 30 2020 at 10:55):

Also, @Patrick Massot @Bryan Gin-ge Chen wonder if I could get commit access to the repository (w/o master or newsite for example), that'd make a simpler workflow for some PRs which might be edited on the top (e.g. links backfilling)

Patrick Massot (May 30 2020 at 10:56):

Could you try to use some TeX in this yaml file? Mathjax is loaded on all pages of the website. So if the yaml parser doesn't get confused then it should work. And if it does get confused then maybe enclosing stuff in quote would be good enough to unconfuse it.

Ryan Lahfa (May 30 2020 at 10:57):

@Patrick Massot I was definitely going to try this

Ryan Lahfa (May 30 2020 at 10:57):

I can replace the Unicode math by some LaTeX

Ryan Lahfa (May 30 2020 at 10:57):

The result might be ugly though, like if you do inline math in respect to the line height (?), but I'm no expert, we'll see and I'll post about it

Patrick Massot (May 30 2020 at 10:58):

I see that real numbers don't even have a unicode mathbb.

Ryan Lahfa (May 30 2020 at 10:59):

:-)

Ryan Lahfa (May 30 2020 at 10:59):

That's an easy fix s/R/$\mathbb{R}$/g

Patrick Massot (May 30 2020 at 10:59):

About the repo access, I'd be happy to give you write access to branches that are not master or newsite, but I'm not sure this wouldn't mess up CI (if I need to protect branches or something), so I'll let Bryan handle that.

Ryan Lahfa (May 30 2020 at 11:00):

Patrick Massot said:

About the repo access, I'd be happy to give you write access to branches that are not master or newsite, but I'm not sure this wouldn't mess up CI (if I need to protect branches or something), so I'll let Bryan handle that.

Sure thing

Ryan Lahfa (May 30 2020 at 11:01):

@Patrick Massot Also, should we just use complex.xxx for the link syntax

Ryan Lahfa (May 30 2020 at 11:01):

And use mathlib_docs/find/{{ decl }}

Ryan Lahfa (May 30 2020 at 11:01):

Sounds like an easy way to fill links, e.g. https://leanprover-community.github.io/mathlib_docs/find/complex.exists_root for complex.exists_root

Ryan Lahfa (May 30 2020 at 11:02):

(I mean rather the module.statement syntax rather than the folder1/folder2/module.html#statement or whatever)

Patrick Massot (May 30 2020 at 11:06):

The advantage of the current format is you can fill in items while browsing the doc website and copy-pasting partial links

Patrick Massot (May 30 2020 at 11:07):

And also a dot separated format looks like Lean namespacing and we don't have any convenient way to access the fully qualified name of a declaration while staring at the file containing it.

Ryan Lahfa (May 30 2020 at 11:14):

isn't it just whatever the statement of a declaration we're looking at?

Ryan Lahfa (May 30 2020 at 11:14):

@Rob Lewis ^

Ryan Lahfa (May 30 2020 at 11:14):

But alright, I was just finding the process of browsing/copying a bit slow for massive link injection

Ryan Lahfa (May 30 2020 at 11:15):

But that's the computer scientist in me who is talking, pay no heed

Scott Morrison (May 30 2020 at 11:17):

The problem when looking at a declaration is that it can be hard to work out what namespace you're currently in (because so many mathlib files are so long). You can insert a #where to discover the namespace, but this will cause recompilation headaches if you're jumping between many files.

Ryan Lahfa (May 30 2020 at 11:18):

Okay, that's not very usable for browsing docs → injecting them in the YAML file, thanks for the clarification

Rob Lewis (May 30 2020 at 11:20):

Yes, the /find/ page just takes a (complete) identifier. Notice that the docs always print a complete identifier, so if you look at (randomly) docs#std.prec.max_plus you can copy std.prec.max_plus directly. It's trickier to find this browsing the Lean source, but you can keep a file with import all open and just use tab complete.

Rob Lewis (May 30 2020 at 11:21):

It's easy enough to expose the declaration name -> location map from the doc generator if this is useful.

Rob Lewis (May 30 2020 at 11:23):

The benefit to using this over hardcoded links, of course, is that if a declaration is moved to a new file the links won't break. Even more important if you're linking to lines in the source, which are very likely to break. src#std.prec.max_plus will stay up to date.

Ryan Lahfa (May 30 2020 at 11:27):

Maybe what we can do now is to use hardcoded links, then we can do an automatic pass to rewrite them properly using the complete identifier, so we can hit the deadline of the IAS for @Patrick Massot

Ryan Lahfa (May 30 2020 at 11:28):

But decl name → location map would be useful I guess, I don't know if it has to be exposed in the HTML or as a JSON/YAML machine-consumable

Rob Lewis (May 30 2020 at 11:29):

Your links already contain the complete identifier, right? I see things like algebra/pi_instances.html#prod.module. Everything after the # is the complete identifier.

Rob Lewis (May 30 2020 at 11:31):

Ryan Lahfa said:

But decl name → location map would be useful I guess, I don't know if it has to be exposed in the HTML or as a JSON/YAML machine-consumable

It wouldn't change the HTML at all, would just host a file leanprover-community.github.io/mathlib_docs/name_to_loc.json.

Rob Lewis (May 30 2020 at 11:31):

So if the website generator needed this info it could just grab the map there.

Rob Lewis (May 30 2020 at 11:32):

It could include more info too, e.g. the type of the declaration. I think this would be particularly nice for the 100 theorems list, to print the statement on the main page.

Ryan Lahfa (May 30 2020 at 11:46):

Rob Lewis said:

Your links already contain the complete identifier, right? I see things like algebra/pi_instances.html#prod.module. Everything after the # is the complete identifier.

Well, this was something I grabbed from the doc link, so I didn't know if it was complete or not

Ryan Lahfa (May 30 2020 at 11:46):

Sounds good @Rob Lewis — I'll see what I can do, but maybe after IAS to make it cooler

Mario Carneiro (May 30 2020 at 12:07):

Scott Morrison said:

The problem when looking at a declaration is that it can be hard to work out what namespace you're currently in (because so many mathlib files are so long). You can insert a #where to discover the namespace, but this will cause recompilation headaches if you're jumping between many files.

Earlier, someone (Kevin?) suggested that we could have theorem declarations be hoverable same as theorem uses. If the hover contained the full namespaced name, wouldn't that solve the problem?

Patrick Massot (May 30 2020 at 12:11):

Yes

Johan Commelin (May 30 2020 at 13:07):

Can someone (@Patrick Massot @Ryan Lahfa ?) tell me how complete the .yaml now is?
Is it just a matter of filling in the links, or are there also still new sections that need to be added to the .yaml?

Patrick Massot (May 30 2020 at 13:08):

Filling the links would be awesome

Patrick Massot (May 30 2020 at 13:09):

We don't plan to add sections soon. At some point we'll probably want to add more advanced sections, maybe in another file.

Johan Commelin (May 30 2020 at 13:09):

Which years does this cover? Is this like 1st and 2nd year of French math education?

Johan Commelin (May 30 2020 at 13:09):

How should I interpret this file?

Johan Commelin (May 30 2020 at 13:11):

Can we add
http://media.devenirenseignant.gouv.fr/file/agreg_externe/59/7/p2020_agreg_ext_maths_1107597.pdf
to the top of the file, in a comment?

Johan Commelin (May 30 2020 at 13:11):

Is this file already rendered somewhere on a public facing website?

Patrick Massot (May 30 2020 at 13:12):

There is a semi-hidden temporary rendering at https://leanprover-community.github.io/overview.html, but really you should ignore that and just fill in

Johan Commelin (May 30 2020 at 13:23):

What is the correct link for complementary subspaces: https://leanprover-community.github.io/mathlib_docs/linear_algebra/projection.html ? Do we have a statement that says that you can choose such a subspace? (@Yury G. Kudryashov)

Patrick Massot (May 30 2020 at 13:25):

Hmm, https://leanprover-community.github.io/mathlib_docs/order/bounded_lattice.html#is_compl might be a bit too abstract...

Johan Commelin (May 30 2020 at 13:26):

Exactly

Patrick Massot (May 30 2020 at 13:29):

It's still useful information that this is how it's said in mathlib. And we can always add more context in https://leanprover-community.github.io/theories/linear_algebra.html

Yury G. Kudryashov (May 30 2020 at 13:33):

Do we allow multiple links per item?

Yury G. Kudryashov (May 30 2020 at 13:33):

https://leanprover-community.github.io/mathlib_docs/linear_algebra/basis.html#submodule.exists_is_compl states that a complementary subspace exists.

Yury G. Kudryashov (May 30 2020 at 13:34):

See also https://leanprover-community.github.io/mathlib_docs/analysis/normed_space/complemented.html for Banach space version (closed complementary subspaces).

Patrick Massot (May 30 2020 at 13:37):

There is no issue putting several links per item in the yaml file, but that would be hard to render if we want to keep it compact (where each listed item is a link to something).

Johan Commelin (May 30 2020 at 13:37):

We still don't have Cayley–Hamilton

Johan Commelin (May 30 2020 at 13:37):

We could link to the first item, and append little link markers for the further links

Patrick Massot (May 30 2020 at 13:37):

Yes, this is one of the goal of this list: highlighting glaring holes (although this is not how I intend to use it on Wednesday...).

Johan Commelin (May 30 2020 at 13:39):

https://github.com/leanprover-community/leanprover-community.github.io/pull/36 is what I've found for section 1.

Yury G. Kudryashov (May 30 2020 at 13:40):

Should we show formalized and not yet formalized items on different pages?

Patrick Massot (May 30 2020 at 13:41):

Yes, I think they should be on different pages

Johan Commelin (May 30 2020 at 13:41):

Maybe just an option at the top

Johan Commelin (May 30 2020 at 13:41):

Where you can toggle what you want to see.

Johan Commelin (May 30 2020 at 13:41):

With a bit of CSS classes that should be trivial

Patrick Massot (May 30 2020 at 13:42):

True, but we also want to browse the TODO list, without seeing what is done

Johan Commelin (May 30 2020 at 13:46):

That's what I'm saying, right?

Johan Commelin (May 30 2020 at 13:46):

Two radio buttons should be able to provide that.

Johan Commelin (May 30 2020 at 13:46):

Done: on/off     TODO: on/off

Patrick Massot (May 30 2020 at 13:50):

Oh ok, right. Feel free to implement, or hope Ryan will do it.

Patrick Massot (May 30 2020 at 14:01):

Johan Commelin said:

https://github.com/leanprover-community/leanprover-community.github.io/pull/36 is what I've found for section 1.

Merged, thanks!

Ryan Lahfa (May 30 2020 at 14:08):

Johan Commelin said:

Done: on/off     TODO: on/off

Sounds good

Ryan Lahfa (May 30 2020 at 14:11):

I'm doing it now

Johan Commelin (May 30 2020 at 14:27):

Coprime elements: we have coprime ideals (ideal.is_coprime) but not specifically coprime elements. To do or not to do?

Ryan Lahfa (May 30 2020 at 14:30):

I guess it's "alright"

Johan Commelin (May 30 2020 at 14:40):

@Patrick Massot Does the "boss" have an opinion? :wink:

Yury G. Kudryashov (May 30 2020 at 14:45):

ideal.is_coprime is a definition of coprime elements that uses ideals.

Johan Commelin (May 30 2020 at 14:47):

Ooh, that's an ugly name in that case

Johan Commelin (May 30 2020 at 14:48):

Divisibility in commutative integral rings what does this mean? What's an integral ring?

Kevin Buzzard (May 30 2020 at 14:50):

I guess for a general ring one can make sense of coprimality of two elements by just asking (a)+(b)=R(a)+(b)=R, but then XX and YY would not be coprime in C[X,Y]\mathbb{C}[X,Y].

Johan Commelin (May 30 2020 at 14:53):

What the hack is a Rupture fields:?

Kevin Buzzard (May 30 2020 at 14:54):

splitting field?

Johan Commelin (May 30 2020 at 14:54):

Nope, that's the next item

Johan Commelin (May 30 2020 at 14:55):

https://github.com/leanprover-community/leanprover-community.github.io/pull/37 here's a bunch of links for section 3 (@Patrick Massot)

Chris Hughes (May 30 2020 at 14:55):

It's just the field when you adjoin one root, but not necessarily all of them

Johan Commelin (May 30 2020 at 14:55):

So we have that, right?

Chris Hughes (May 30 2020 at 14:55):

Yes

Alex J. Best (May 30 2020 at 14:55):

https://fr.wikipedia.org/wiki/Corps_de_rupture

Johan Commelin (May 30 2020 at 14:56):

Derived polynomials: # Should this be "Polynomial derivative"? @Ryan Lahfa

Ryan Lahfa (May 30 2020 at 14:56):

@Johan Commelin Yes, it's really PP' when PP is a polynomial IIRC

Ryan Lahfa (May 30 2020 at 14:56):

as a formal polynomial

Reid Barton (May 30 2020 at 14:56):

https://en.wikipedia.org/wiki/Rupture_field

Ryan Lahfa (May 30 2020 at 14:56):

I was going to link it :D

Reid Barton (May 30 2020 at 14:57):

I definitely assumed this was a mistranslation

Ryan Lahfa (May 30 2020 at 14:57):

I double checked those because it looked fishy to me but Wikipedia proved me wrong

Johan Commelin (May 30 2020 at 14:57):

TIL

Ryan Lahfa (May 30 2020 at 14:57):

But really, sometimes, in France, there seems to be many structures which are not "directly" available in English

Ryan Lahfa (May 30 2020 at 14:57):

Also, our convergence is not the good one :-°

Ryan Lahfa (May 30 2020 at 14:59):

We call a limit, something which is rather limit by different values limxaxaf(x)\lim_{x \to a \atop x \neq a} f(x) (for example)

Ryan Lahfa (May 30 2020 at 14:59):

But it does not matter

Johan Commelin (May 30 2020 at 14:59):

I've pushed those two fixes

Ryan Lahfa (May 30 2020 at 15:02):

I have the desired feature

Ryan Lahfa (May 30 2020 at 15:02):

Will push it

Johan Commelin (May 30 2020 at 15:04):

Ryan Lahfa said:

I have the desired feature

You mean the radio buttons?

Ryan Lahfa (May 30 2020 at 15:04):

Yes

Ryan Lahfa (May 30 2020 at 15:04):

https://github.com/leanprover-community/leanprover-community.github.io/pull/38

Ryan Lahfa (May 30 2020 at 15:05):

Awesome PRs @Johan Commelin

Ryan Lahfa (May 30 2020 at 15:05):

We should try to use LaTeX for titles

Ryan Lahfa (May 30 2020 at 15:06):

Like "something something $\Q[X]$ something" if we have the macro for, or just $\mathbb{Q}$

Ryan Lahfa (May 30 2020 at 15:07):

Screen-Capture_select-area_20200530170650.png

Ryan Lahfa (May 30 2020 at 15:07):

LaTeX is working just fine

Ryan Lahfa (May 30 2020 at 15:07):

Will do a PR to add some examples

Ryan Lahfa (May 30 2020 at 15:07):

of course, we don't have the macro \Q

Ryan Lahfa (May 30 2020 at 15:07):

should we add some macros to our MathJax setup?

Johan Commelin (May 30 2020 at 15:07):

You could add some common macros to the top of the rendered page.

Ryan Lahfa (May 30 2020 at 15:08):

Alright, I'll do it

Ryan Lahfa (May 30 2020 at 15:08):

Shouldn't I do this in templates/_base.html ?

Johan Commelin (May 30 2020 at 15:08):

Je ne sais pas

Ryan Lahfa (May 30 2020 at 15:08):

I'll try locally, if it works fine, I'll let as-is and @Patrick Massot will do the ultimate call

Ryan Lahfa (May 30 2020 at 15:08):

:D

Ryan Lahfa (May 30 2020 at 15:12):

Does not work, so I'll put it in the base

Patrick Massot (May 30 2020 at 15:20):

I'm sorry I was away. Are there still things to discuss, or did you settle everything?

Ryan Lahfa (May 30 2020 at 15:20):

https://github.com/leanprover-community/leanprover-community.github.io/pull/39

Ryan Lahfa (May 30 2020 at 15:21):

@Patrick Massot You can take a look to 39 & 38 and see if it's okay for you

Patrick Massot (May 30 2020 at 15:21):

I think we can add a couple of LaTeX macros in _base.html.

Ryan Lahfa (May 30 2020 at 15:21):

39 implements the LaTeX macros in _base

Ryan Lahfa (May 30 2020 at 15:21):

I didn't go too far, I just added R, Q, Z, C, N

Ryan Lahfa (May 30 2020 at 15:22):

We could add GL, L, class{n} (continuity classes), S(R^d), etc. Depends.

Johan Commelin (May 30 2020 at 15:22):

@Patrick Massot By now, my PR should be uncontroversial.

Johan Commelin (May 30 2020 at 15:23):

I think GL, SL, etc are fine. But I wouldn't go overboard with the macros.

Ryan Lahfa (May 30 2020 at 15:23):

I do mathrm{GL}, etc. for them

Ryan Lahfa (May 30 2020 at 15:23):

You can see it in 39

Johan Commelin (May 30 2020 at 15:23):

Maybe the rule of three applies? If you need it more then 3 times, a macro should be fine.

Ryan Lahfa (May 30 2020 at 15:23):

GL(n, R), GL(n, C)…

Patrick Massot (May 30 2020 at 15:23):

Are those 3 PRs compatible?

Ryan Lahfa (May 30 2020 at 15:23):

O(n, 2), O(n, 3)…

Ryan Lahfa (May 30 2020 at 15:23):

@Patrick Massot Please merge Johan's ones first

Ryan Lahfa (May 30 2020 at 15:24):

Then I'll do the rebase magic for whatever happens

Ryan Lahfa (May 30 2020 at 15:24):

I'm pretty sure there are no to very few conflicts

Ryan Lahfa (May 30 2020 at 15:25):

(we're close to have everything in rings, wow!)

Johan Commelin (May 30 2020 at 15:25):

@Patrick Massot One second

Johan Commelin (May 30 2020 at 15:25):

Ryan spotted an issue in my PR

Ryan Lahfa (May 30 2020 at 15:25):

@Johan Commelin it's not that important, I'm fixing it in my PR

Ryan Lahfa (May 30 2020 at 15:26):

If you don't do it, that'll just break newsite temporarily (before merging mine)

Johan Commelin (May 30 2020 at 15:27):

@Patrick Massot Ok, you can merge now

Patrick Massot (May 30 2020 at 15:27):

I reviewed Johan's PR

Patrick Massot (May 30 2020 at 15:28):

But I could merge it since my comments are only about empty items

Ryan Lahfa (May 30 2020 at 15:28):

Nevermind my comments

Ryan Lahfa (May 30 2020 at 15:28):

Yes, I think we can merge it

Johan Commelin (May 30 2020 at 15:28):

Also, I need to go now

Patrick Massot (May 30 2020 at 15:30):

Thanks Johan, I merged it.

Ryan Lahfa (May 30 2020 at 15:30):

Fixing the conflicts

Ryan Lahfa (May 30 2020 at 15:33):

Conflicts resolved, @Patrick Massot

Ryan Lahfa (May 30 2020 at 15:35):

I'll experiment for the "show inline elements for the last depth level"

Patrick Massot (May 30 2020 at 15:38):

Great!

Ryan Lahfa (May 30 2020 at 15:38):

@Patrick Massot style question, should we do titlecase for every title?

Patrick Massot (May 30 2020 at 15:38):

I merged the switch one and this created conflict in the macro one

Ryan Lahfa (May 30 2020 at 15:38):

I'll fix the macro one

Patrick Massot (May 30 2020 at 15:39):

About titlecase, let's do whatever is convenient in the yaml, and we can add a jinja filter if we want to change it on the website

Ryan Lahfa (May 30 2020 at 15:40):

At the make_site phase, we can just give title.titlecase() if we want, it was really just should we do it or not?

Patrick Massot (May 30 2020 at 15:40):

The title of the page should change too. I think we can use "Undergraduate mathematics in mathlib".

Ryan Lahfa (May 30 2020 at 15:40):

https://github.com/leanprover-community/leanprover-community.github.io/pull/40 for deepest level

Ryan Lahfa (May 30 2020 at 15:41):

@Patrick Massot conflicts resolved on the latex one

Ryan Lahfa (May 30 2020 at 15:42):

"Done undergraduate mathematics in Lean"
:-)

screencapture-leanprover-community-github-io-overview-html-2020-05-30-17_42_06.png

Patrick Massot (May 30 2020 at 15:44):

We try to checkout your PR 40 it doesn't seem to work

Patrick Massot (May 30 2020 at 15:44):

Does it work on your end?

Ryan Lahfa (May 30 2020 at 15:44):

Patrick Massot said:

We try to checkout your PR 40 it doesn't seem to work

Maybe I misunderstood what do you mean by inline elements, is it like the latest nodes are not accordion, right?

Ryan Lahfa (May 30 2020 at 15:45):

(Remaining undergrad maths)
screencapture-leanprover-community-github-io-overview-html-2020-05-30-17_43_22-2.png screencapture-leanprover-community-github-io-overview-html-2020-05-30-17_43_22.png

Patrick Massot (May 30 2020 at 15:46):

I want the deepest level to be a single paragraph, with words separated by commas. As in the original document

Patrick Massot (May 30 2020 at 15:46):

On your screenshot, everything under "Bilinear" would be on the same line

Ryan Lahfa (May 30 2020 at 15:47):

Oh okay, makes sense, and all "mathematical statements" would be <a /> to the docs, right?

Patrick Massot (May 30 2020 at 15:48):

And there would be no "See it in mathlib documentation" anywhere. Instead of use card containing

vector space
See it in mathlib documentation

and a huge card linear map..., there would be

vector space, linear map...

Ryan Lahfa (May 30 2020 at 15:48):

I see

Ryan Lahfa (May 30 2020 at 15:49):

I'm doing it

Ryan Lahfa (May 30 2020 at 15:49):

I should have the prototype in minutes

Patrick Massot (May 30 2020 at 15:49):

Thank you very much

Ryan Lahfa (May 30 2020 at 15:50):

@Patrick Massot Just a quick question

Patrick Massot (May 30 2020 at 15:50):

Yes?

Ryan Lahfa (May 30 2020 at 15:50):

What do you do about

xxx:
    yyy: 
    zzz: 
    ttt:
        aaa: 
   uuu: 

Ryan Lahfa (May 30 2020 at 15:51):

do you show in the xxx card:
yyy, zzz
then the ttt accordion
then uuu?

Patrick Massot (May 30 2020 at 15:52):

We probably need to simplify the nesting. I think there should be only two levels of accordions.

Ryan Lahfa (May 30 2020 at 15:52):

Agreed

Patrick Massot (May 30 2020 at 15:52):

Do you have a specific example?

Ryan Lahfa (May 30 2020 at 15:52):

Take linear algebra

Ryan Lahfa (May 30 2020 at 15:52):

Linear algebra:
  vector space: 'algebra/module.html#vector_space'
  linear map: 'algebra/module.html#linear_map'
  product of vector spaces: 'algebra/pi_instances.html#prod.module'
  vector subspace: 'algebra/module.html#subspace'
  range of a linear map: 'linear_algebra/basic.html#linear_map.range'
  kernel of a linear map: 'linear_algebra/basic.html#linear_map.ker'
  quotient space: 'linear_algebra/basic.html#submodule.quotient'
  sum of subspaces: 'linear_algebra/basic.html#submodule.complete_lattice'
  direct sum: ''
  complement subspace: ''
  linear independent: 'linear_algebra/basis.html#linear_independent'
  generating sets: ''
  bases: ''
  algebra of endomorphisms of a vector space: ''
  general linear group: 'linear_algebra/basic.html#linear_map.general_linear_group'
  invariant subspace of an endomorphism: ''
  eigenvalue: ''
  eigenvector: ''
  linear representation: ''
  irreducible representation: ''
  finite dimensional representations:
    examples: ''
    Schur's lemma: ''
  finite-dimensional vector spaces:
    finite-dimensional vector spaces: 'linear_algebra/finite_dimensional.html#finite_dimensional'
    existence of bases: 'linear_algebra/basis.html#exists_is_basis'
    canonical isomorphism with K^n: 'linear_algebra/basis.html#module_equiv_finsupp'
    complementary subspaces: 'linear_algebra/basis.html#submodule.exists_is_compl'
    rank of a linear map: ''
    rank of a set of vectors: ''
    dual vector space: 'linear_algebra/dual.html#module.dual'
    rank of a system of linear equations: ''
    transpose of a linear map: ''
    dual basis: 'linear_algebra/dual.html#is_basis.dual_basis'
    bidual: 'linear_algebra/dual.html#vector_space.eval_equiv'
    orthogonality: ''
  multilinear:
    multilinear map: 'linear_algebra/multilinear.html#multilinear_map'
    determinant of vectors: ''
    determinant of endomorphisms: ''
    special linear group: ''
    orientation of a R-valued vector space: ''
  matrices:
    commutative ring valued matrices: 'data/matrix/basic.html#matrix'
    field valued matrices: 'data/matrix/basic.html#matrix'
    elementary operations on matrices' rows: ''
    elementary operations on matrices' columns: ''
    determinant: 'linear_algebra/determinant.html#matrix.det'
    invertibility: 'linear_algebra/nonsingular_inverse.html#matrix.nonsing_inv'
    rank of a matrix: ''
    matrix representation of a linear map: 'linear_algebra/matrix.html#linear_map.to_matrix'
    coordinates change: ''
    Gauss' pivot: ''
    row-reduced matrices: ''
  endomorphism invariant subspaces: ''
  kernel lemma: ''
  characteristic polynomial: ''
  endomorphism polynomials: ''
  cancelling polynomials: ''
  minimal polynomial: ''
  Cayley-Hamilton theorem: ''

Ryan Lahfa (May 30 2020 at 15:53):

necessarily, I need a way to determine when to stop the inline display for leaves

Ryan Lahfa (May 30 2020 at 15:53):

I think I can work out some prototype but just want to warn about the strange result it might give

Patrick Massot (May 30 2020 at 15:54):

Here I think we are actually missing nesting. The issue is that some stuff is dumped at level 2 but should be level 3 (ie leaves).

Ryan Lahfa (May 30 2020 at 15:55):

I think too, I didn't work on the organization and wanted to get something out ASAP

Patrick Massot (May 30 2020 at 15:56):

The end is clearly missing a heading, something like 'endomorphism polynomials'

Ryan Lahfa (May 30 2020 at 15:56):

Anyway, I'll implement the following solution:
When I encounter a leaf, I just show it inline with <a /> and add a , if I'm not the last node of the current iterator (doable in Jinja magic)
When I encounter an internal node, I create an accordion
That should work

Ryan Lahfa (May 30 2020 at 15:56):

Patrick Massot said:

The end is clearly missing a heading, something like 'endomorphism polynomials'

We already have endomorphism polynomials, but you have this annoying issue
If you do a heading
Then you have to repeat it in order to link to the concept

Ryan Lahfa (May 30 2020 at 15:57):

Like, endomorphism polynomials have a lot of things around, but are themselves a specific kind of polynomials… I don't know how to solve "this"

Patrick Massot (May 30 2020 at 15:57):

I don't think this is a big issue

Ryan Lahfa (May 30 2020 at 15:58):

Okay

Patrick Massot (May 30 2020 at 15:58):

You can let people with more math experience going over the yaml file to sort this out

Ryan Lahfa (May 30 2020 at 15:59):

screencapture-localhost-8000-overview-html-2020-05-30-17_59_00.png

Ryan Lahfa (May 30 2020 at 15:59):

@Patrick Massot Yes, definitely, I don't want to fight this :) — I'm still too green

Ryan Lahfa (May 30 2020 at 15:59):

Here's a prototype

Ryan Lahfa (May 30 2020 at 16:00):

Do you want I do something before I commit this?

Patrick Massot (May 30 2020 at 16:00):

I think it looks much better. But there is still the issue that inner card should extend horizontally to match outer ones

Ryan Lahfa (May 30 2020 at 16:02):

Screen-Capture_select-area_20200530180156.png
do you mean something like this ?

Ryan Lahfa (May 30 2020 at 16:02):

because all cards applied padding on their stuff, so when I nest them, obviously…

Ryan Lahfa (May 30 2020 at 16:03):

but I don't think that's a bad thing per se, that gives space and looks not that bad on mobile AFAIK

Ryan Lahfa (May 30 2020 at 16:04):

we can reduce padding in the inner cards I guess

Patrick Massot (May 30 2020 at 16:08):

No, I mean no space at all on sides of inner cards.

Patrick Massot (May 30 2020 at 16:09):

Also I'd prefer to keep a white background. It looks weird to have this all grey background only on this webpage of the website

Ryan Lahfa (May 30 2020 at 16:12):

Okay for bg color

Ryan Lahfa (May 30 2020 at 16:13):

For the space, I'll try something, you'll let me know, worst case, you can edit the PR or guide me again

Ryan Lahfa (May 30 2020 at 16:13):

Should have something in 10 minutes hopefully

Patrick Massot (May 30 2020 at 16:14):

Also, I'm not the only one deciding stuff here. If everybody likes those margins I'll have them.

Ryan Lahfa (May 30 2020 at 16:15):

Then we should ping them for their advice, @Bryan Gin-ge Chen @Rob Lewis @Kevin Buzzard @Yury G. Kudryashov @Mario Carneiro @Scott Morrison

Patrick Massot (May 30 2020 at 16:18):

You should have waited to get a prototype incorporating everything (including switches and updated page title)

Ryan Lahfa (May 30 2020 at 16:19):

Why?

Patrick Massot (May 30 2020 at 16:19):

Because this way they don't have to read all messages, they can look at the result

Patrick Massot (May 30 2020 at 16:19):

Those are busy people

Ryan Lahfa (May 30 2020 at 16:19):

You're right

Ryan Lahfa (May 30 2020 at 16:21):

Apologies

Patrick Massot (May 30 2020 at 16:23):

Don't worry

Ryan Lahfa (May 30 2020 at 16:24):

It's now online on the inline branch, @Patrick Massot

Ryan Lahfa (May 30 2020 at 16:24):

It is also rebased over newsite, I'll just verify & repull just in case

Kevin Buzzard (May 30 2020 at 16:24):

Did somebody call?

Kevin Buzzard (May 30 2020 at 16:25):

I am just having a break from marking, what should I look at?

Kevin Buzzard (May 30 2020 at 16:25):

Only 80 algebraic geometry questions to go :D

Ryan Lahfa (May 30 2020 at 16:26):

I'm getting full page screenshots, if you don't want to do make_site on the branch

Ryan Lahfa (May 30 2020 at 16:27):

In the order: complete (todo & done), done, todo
screencapture-file-home-raito-dev-projects-Lean-leanprover-community-github-io-build-overview-html-2020-05-30-18_26_24.png screencapture-file-home-raito-dev-projects-Lean-leanprover-community-github-io-build-overview-html-2020-05-30-18_26_15.png screencapture-file-home-raito-dev-projects-Lean-leanprover-community-github-io-build-overview-html-2020-05-30-18_25_46.png

Ryan Lahfa (May 30 2020 at 16:27):

Let us know what you think of the design and what would you want to see

Ryan Lahfa (May 30 2020 at 16:28):

https://github.com/leanprover-community/leanprover-community.github.io/pull/40

Patrick Massot (May 30 2020 at 16:28):

There is something funny going on with "Affine and Euclidian Geoemtry (finite dimensional only)" (besides the typo and the restriction)

Ryan Lahfa (May 30 2020 at 16:28):

The PR is there for the ones who want to try it live

Ryan Lahfa (May 30 2020 at 16:28):

@Patrick Massot YAML stuff most likely

Ryan Lahfa (May 30 2020 at 16:29):

Can fix it in a future PR

Patrick Massot (May 30 2020 at 16:30):

I'd like the accordion to be folded when you open the page, so that people can navigate quickly. And also the todo switch should be off by default, so that people first get the information about what is there and where.

Patrick Massot (May 30 2020 at 16:31):

And I still don't like the horizontal margins :stuck_out_tongue:

Patrick Massot (May 30 2020 at 16:31):

But otherwise it really starts looking like what I dreamed of.

Ryan Lahfa (May 30 2020 at 16:31):

Patrick Massot said:

I'd like the accordion to be folded when you open the page, so that people can navigate quickly. And also the todo switch should be off by default, so that people first get the information about what is there and where.

  • Default switch to off is easy for TODO
  • Folded accordions is easy too

Can add them, right now, should I go for it?

Ryan Lahfa (May 30 2020 at 16:32):

Patrick Massot said:

And I still don't like the horizontal margins :stuck_out_tongue:

I will have to wait the vote from the people

Patrick Massot (May 30 2020 at 16:32):

yes, please

Mario Carneiro (May 30 2020 at 16:32):

those screenshots are massive and zulip doesn't let me zoom in easily. could you show a representative sample?

Patrick Massot (May 30 2020 at 16:32):

You'll have more votes when I'll merge the PR and we'll see it live

Ryan Lahfa (May 30 2020 at 16:32):

@Mario Carneiro You can load them in your browser or enable pan & zoom to review them easily

Ryan Lahfa (May 30 2020 at 16:32):

But yes, let's merge the PR @Patrick Massot

Patrick Massot (May 30 2020 at 16:32):

when I click on them it zooms

Ryan Lahfa (May 30 2020 at 16:32):

Let me just get the latest changes you want

Patrick Massot (May 30 2020 at 16:32):

Did you fixed the two defaults?

Patrick Massot (May 30 2020 at 16:32):

Yes, let's do that

Ryan Lahfa (May 30 2020 at 16:33):

I'm doing it, only one left

Mario Carneiro (May 30 2020 at 16:33):

with pan & zoom the frame doesn't change shape so I'm peering through a very slim vertical window

Mario Carneiro (May 30 2020 at 16:34):

zulip's implementation really needs work

Patrick Massot (May 30 2020 at 16:34):

Mario, you should hold on for 5 minutes

Ryan Lahfa (May 30 2020 at 16:34):

Just open the link in the browser

Mario Carneiro (May 30 2020 at 16:35):

what is being reviewed?

Mario Carneiro (May 30 2020 at 16:35):

the margins?

Ryan Lahfa (May 30 2020 at 16:35):

@Mario Carneiro the looks mostly

Mario Carneiro (May 30 2020 at 16:35):

the spacing is all over the place

Mario Carneiro (May 30 2020 at 16:36):

there is 0px spacing between cards but significant (20px?) margins on left and right and at the bottom of a group

Ryan Lahfa (May 30 2020 at 16:36):

here we go for the defaults

Mario Carneiro (May 30 2020 at 16:36):

also there is no spacing after the text and before the cards

Ryan Lahfa (May 30 2020 at 16:37):

+1 @ spacing pre/post cards

Ryan Lahfa (May 30 2020 at 16:37):

the indentation "spacing" is by default

Mario Carneiro (May 30 2020 at 16:37):

What's wrong with a simple bullet list?

Ryan Lahfa (May 30 2020 at 16:37):

it's not an accordion (?)

Ryan Lahfa (May 30 2020 at 16:37):

you can fold/unfold those cards

Ryan Lahfa (May 30 2020 at 16:38):

@Patrick Massot wants to remove horizontal space on cards I think (if I understood well, I won't speak in its place)

Mario Carneiro (May 30 2020 at 16:38):

I'm not sure why this particular list is getting web-designed

Patrick Massot (May 30 2020 at 16:38):

I don't understand why it doesn't look like https://getbootstrap.com/docs/4.4/components/collapse/#accordion-example

Mario Carneiro (May 30 2020 at 16:38):

I would have just chucked some markdown on a page

Patrick Massot (May 30 2020 at 16:38):

Mario, this list is too big to be unfolded by default

Ryan Lahfa (May 30 2020 at 16:38):

@Patrick Massot I can take a look why

Ryan Lahfa (May 30 2020 at 16:38):

It might be a class missing

Mario Carneiro (May 30 2020 at 16:39):

I've seen mile long bullet lists before

Patrick Massot (May 30 2020 at 16:39):

Mario didn't need CSS in metamath...

Ryan Lahfa (May 30 2020 at 16:39):

Screen-Capture_select-area_20200530183933.png

Ryan Lahfa (May 30 2020 at 16:39):

that was it

Ryan Lahfa (May 30 2020 at 16:39):

but it broke the toggle button

Patrick Massot (May 30 2020 at 16:40):

I still think the inner list should extend horizontally to fill the container (and there should be no leaf next to them, but this is a yaml content issue)

Mario Carneiro (May 30 2020 at 16:41):

Patrick Massot said:

Mario didn't need CSS in metamath...

Interesting that you mention that, just this week we had a conversation about upgrading our HTML validator and the new one yells at us for using <FONT> tags

Ryan Lahfa (May 30 2020 at 16:42):

@Patrick Massot I pushed the fix for accordions

Ryan Lahfa (May 30 2020 at 16:42):

The thing now is that due to this kind of styling

Ryan Lahfa (May 30 2020 at 16:43):

When I hide todo sections, Bootstrap cannot put the border-bottom, because it's in display: hidden and the selector is like "apply the bottom border on the last element in the DOM"

Ryan Lahfa (May 30 2020 at 16:43):

I'm not sure I see easy workarounds

Ryan Lahfa (May 30 2020 at 16:44):

I'll have to manually force-style the previous element in the section, I'm not sure

Ryan Lahfa (May 30 2020 at 16:44):

Anyway, if we can get this PR merged, we can get more improvements later, @Patrick Massot is this okay with you?

Ryan Lahfa (May 30 2020 at 16:45):

:tada:

Patrick Massot (May 30 2020 at 16:46):

Yes, I think this will help people discussing it. Everybody will be able to play with it. Hopefully this will also increase motivation for working on the yaml file.

Patrick Massot (May 30 2020 at 16:46):

Everybody, we are discussing https://leanprover-community.github.io/overview.html

Patrick Massot (May 30 2020 at 16:47):

This is currently live but without any link pointing towards it.

Ryan Lahfa (May 30 2020 at 16:47):

this bottomless stuff is making me crazy

Ryan Lahfa (May 30 2020 at 16:47):

Oops @Patrick Massot

Ryan Lahfa (May 30 2020 at 16:47):

I'll fix it…

Patrick Massot (May 30 2020 at 16:47):

No

Patrick Massot (May 30 2020 at 16:47):

Don't fix it

Patrick Massot (May 30 2020 at 16:47):

It's not ready for links

Kevin Buzzard (May 30 2020 at 16:47):

https://mathlib_docs/algebra/char_p.html#frobenius isn't a valid URL

Patrick Massot (May 30 2020 at 16:48):

I very carefully checked there was no link to it

Kevin Buzzard (May 30 2020 at 16:48):

Why does Fields have fields as a subthing?

Patrick Massot (May 30 2020 at 16:48):

We need at least one pass over the whole yaml file before linking to this webpage

Ryan Lahfa (May 30 2020 at 16:48):

I meant the fact that mathlib_docs are not pointing correctly is a bug

Kevin Buzzard (May 30 2020 at 16:48):

Does "todo" mean "we need to add a link" or "we need to formalise this"?

Ryan Lahfa (May 30 2020 at 16:48):

@Kevin Buzzard It means both currently

Patrick Massot (May 30 2020 at 16:48):

It currently means either of these

Patrick Massot (May 30 2020 at 16:49):

Fields has fields as a subthing because the big one should read "Field theory"

Ryan Lahfa (May 30 2020 at 16:49):

@Patrick Massot https://github.com/leanprover-community/leanprover-community.github.io/pull/41

Kevin Buzzard (May 30 2020 at 16:49):

So "Distributions on Rd" is not LaTeX'ed up, presumably you know this

Ryan Lahfa (May 30 2020 at 16:49):

It'll fix the mathlib links

Ryan Lahfa (May 30 2020 at 16:49):

@Kevin Buzzard Yes, LaTeX-ification is open to improvements :-)

Patrick Massot (May 30 2020 at 16:50):

Kevin, it wouldn't take more time to fix it on github than to write it here

Kevin Buzzard (May 30 2020 at 16:50):

but of course in general it's a really nice resource.

Kevin Buzzard (May 30 2020 at 16:50):

Yeah but I need to go

Patrick Massot (May 30 2020 at 16:50):

https://github.com/leanprover-community/leanprover-community.github.io/blob/newsite/data/overview.yaml

Johan Commelin (May 30 2020 at 16:50):

There are commas at the and of the lists. Is that intended?

Ryan Lahfa (May 30 2020 at 16:51):

Unfortunately

Ryan Lahfa (May 30 2020 at 16:51):

When the next element is hidden

Ryan Lahfa (May 30 2020 at 16:51):

I don't do adjustements to make the comma disappear

Kevin Buzzard (May 30 2020 at 16:51):

\"Usual\" functions in single variable real analysis

Johan Commelin (May 30 2020 at 16:51):

Ok

Patrick Massot (May 30 2020 at 16:51):

If this is all too painful we can still make a different webpage with the todoes

Ryan Lahfa (May 30 2020 at 16:51):

Kevin Buzzard said:

\"Usual\" functions in single variable real analysis

That's an easy fix, \ should be dropped in the YAML, it can be edited online

Kevin Buzzard (May 30 2020 at 16:52):

I will take a very good look at this on Tues when my deadlines are over

Kevin Buzzard (May 30 2020 at 16:52):

There is of course a lot of overlap with https://leanprover-community.github.io/mathlib-overview.html

Ryan Lahfa (May 30 2020 at 16:52):

Patrick Massot said:

If this is all too painful we can still make a different webpage with the todoes

I don't think that'd be hard, but it just require that I think about the problem seriously and not implement workarounds on the top of workarounds

Johan Commelin (May 30 2020 at 16:52):

We could add "Expand all / Collapse all"

Ryan Lahfa (May 30 2020 at 16:52):

Johan Commelin said:

We could add "Expand all / Collapse all"

That's easy to do

Johan Commelin (May 30 2020 at 16:52):

Kevin Buzzard said:

There is of course a lot of overlap with https://leanprover-community.github.io/mathlib-overview.html

Yup, but that list was ad hoc. This one has an official "stamp" from French education...

Ryan Lahfa (May 30 2020 at 16:53):

Can add it but not right now, I'm hungry

Ryan Lahfa (May 30 2020 at 16:53):

Johan Commelin said:

Kevin Buzzard said:

There is of course a lot of overlap with https://leanprover-community.github.io/mathlib-overview.html

Yup, but that list was ad hoc. This one has an official "stamp" from French education...

And ours has links !

Kevin Buzzard (May 30 2020 at 16:53):

Is it somehow possible to make that mathlib-overview page have the same format I wonder? Do we even want that though, or is the simpler formatting of the overview page better perhaps?

Kevin Buzzard (May 30 2020 at 16:53):

For the overview page there is no particular "goal" -- here we have a very well-defined and, in my opinion, extremely exciting, goal.

Johan Commelin (May 30 2020 at 16:53):

I think that eventually the two lists should be merged

Johan Commelin (May 30 2020 at 16:54):

And we could generate different pages from the same source .yaml file

Ryan Lahfa (May 30 2020 at 16:54):

Definitely possible

Kevin Buzzard (May 30 2020 at 16:56):

Is it possible to add (not right now, but at some point) more stuff? For example at Imperial they learn Jordan Canonical Form

Ryan Lahfa (May 30 2020 at 16:56):

It might be already there implicitly as the french name of "reduction techniques"

Ryan Lahfa (May 30 2020 at 16:57):

I don't recall if Jordan is part of agrég

Kevin Buzzard (May 30 2020 at 16:57):

I am 100% sure there will one random thing on our curriculum which is not on this list, that's what I'm saying basically

Patrick Massot (May 30 2020 at 16:57):

Sure, all this is possible. We can add a page with more advanced stuff, or add more sections

Kevin Buzzard (May 30 2020 at 16:57):

or on Cambridge's curriculum or whatever

Ryan Lahfa (May 30 2020 at 16:57):

FWIW, https://laurent.claessens-donadello.eu/pdf/lefrido.pdf should represent a decent part of the agrég

Patrick Massot (May 30 2020 at 16:57):

I'm pretty sure Jordan is there somewhere, maybe implicitly

Ryan Lahfa (May 30 2020 at 16:57):

But it's French

Johan Commelin (May 30 2020 at 16:57):

I think the next step would be to add tags in the list:

Linear Algebra:
  Matrices:
    Inverse:
      link: 'link/to/docs.html#inverse'
      tag: [agreg, icl]

Ryan Lahfa (May 30 2020 at 16:58):

Jordan is 9.13

Kevin Buzzard (May 30 2020 at 16:58):

OK I'm going back to the treadmill. It looks really nice. I don't really have a feeling for what it will look like on Wednesday when it's complete, but hopefully it looks respectable.

Ryan Lahfa (May 30 2020 at 16:58):

we have it Screen-Capture_select-area_20200530185822.png

Ryan Lahfa (May 30 2020 at 16:58):

Johan Commelin said:

I think the next step would be to add tags in the list:

Linear Algebra:
  Matrices:
    Inverse:
      link: 'link/to/docs.html#inverse'
      tag: [agreg, icl]

it requires just minor adjustement in the Python code, but we can very much support it

Patrick Massot (May 30 2020 at 16:59):

No Johan, the next step is to finish the first pass on the yaml linkifying

Ryan Lahfa (May 30 2020 at 16:59):

:DDDDDD

Johan Commelin (May 30 2020 at 16:59):

Ok, sure. I meant the next next step

Johan Commelin (May 30 2020 at 16:59):

Like, after your IAS talk

Patrick Massot (May 30 2020 at 17:01):

Ok, I'll have a go at Section 6: Single variable real analysis.

Bryan Gin-ge Chen (May 30 2020 at 17:04):

@Ryan Lahfa I've given you write access to the repo. Also, the CI now builds all branches (except master and oldsite), and deploys only happen for newsite.

Patrick Massot (May 30 2020 at 17:07):

Oh crap, the very first item I picked is hard. Topology on R...

Patrick Massot (May 30 2020 at 17:07):

R gets its topology as a uniform space

Yury G. Kudryashov (May 30 2020 at 17:11):

Metric space?

Patrick Massot (May 30 2020 at 17:12):

Yes

Patrick Massot (May 30 2020 at 17:12):

I linked to real.metric_space

Patrick Massot (May 30 2020 at 17:14):

Oh we still have underlined links in the API docs :sad:

Patrick Massot (May 30 2020 at 17:16):

Another tricky one: cluster point of a sequence. Of course we have that as a special case of filter stuff, but do we have a specific definition? If not then I'll let this blank

Bryan Gin-ge Chen (May 30 2020 at 17:18):

The underlined links will hopefully be addressed by doc-gen#20. @Ryan Lahfa, are you still around? :smile:

Patrick Massot (May 30 2020 at 17:20):

I think he's having dinner.

Patrick Massot (May 30 2020 at 17:20):

But I don't understand how a young nerd can have dinner away from his keyboard.

Ryan Lahfa (May 30 2020 at 17:22):

Patrick Massot said:

But I don't understand how a young nerd can have dinner away from his keyboard.

That's because my kitchen is not yet integrated!

Ryan Lahfa (May 30 2020 at 17:22):

Bryan Gin-ge Chen said:

The underlined links will hopefully be addressed by doc-gen#20. Ryan Lahfa, are you still around? :smile:

I'm around, I still need to do something which is good for everyone :D

Ryan Lahfa (May 30 2020 at 17:22):

I can try to move it forward today

Ryan Lahfa (May 30 2020 at 17:26):

By curiosity, do we even have distributions in Lean?

Patrick Massot (May 30 2020 at 17:29):

Distributions in the sense of Schwartz?

Patrick Massot (May 30 2020 at 17:30):

We don't.

Patrick Massot (May 30 2020 at 17:32):

@Sebastien Gouezel or @Yury G. Kudryashov do you know whether we have the description of connected subsets of R? The closest I can find is https://leanprover-community.github.io/mathlib_docs/topology/algebra/ordered.html#is_preconnected_iff_forall_Icc_subset

Yury G. Kudryashov (May 30 2020 at 17:33):

We don't. We have is_preconnected_iff_forall_Icc_subset and is_preconnected_I??.

Yury G. Kudryashov (May 30 2020 at 17:35):

How would you formulate real.is_(pre)connected_iff to make it useful?

Patrick Massot (May 30 2020 at 17:38):

I think we could at least say connected iff convex

Patrick Massot (May 30 2020 at 17:39):

Do you know whether we have convergent numerical series. I know about has_sum, but this is a stronger notion. I know we can state "partial sums converge", but do we actually have a def?

Patrick Massot (May 30 2020 at 17:40):

It's dinner time. See you later

Yury G. Kudryashov (May 30 2020 at 17:42):

has_sum uses tendsto (λ n, ∑ i in range n, a i) at_top (nhds s).

Yury G. Kudryashov (May 30 2020 at 17:46):

is_preconnected_iff_convex is is_preconnected_iff_forall_Icc_subset.trans convex_real_iff.symm (no, one of them has x≤y)

Patrick Massot (May 30 2020 at 17:58):

There are two different has_sum then

Patrick Massot (May 30 2020 at 17:58):

Where is yours?

Yury G. Kudryashov (May 30 2020 at 18:00):

Sorry, I meant that the file about has_sum uses this tendsto when talking about normal series convergence.

Yury G. Kudryashov (May 30 2020 at 18:00):

I should read my messages before sending them.

Patrick Massot (May 30 2020 at 18:02):

Yes there are things like https://leanprover-community.github.io/mathlib_docs/topology/algebra/infinite_sum.html#has_sum_iff_tendsto_nat_of_summable

Patrick Massot (May 30 2020 at 18:02):

But we still miss a def here

Paul van Wamelen (May 30 2020 at 18:28):

How do I help edit this on github? (without submitting a PR from a fork?)

Patrick Massot (May 30 2020 at 18:35):

https://github.com/leanprover-community/leanprover-community.github.io/blob/newsite/data/overview.yaml

Patrick Massot (May 30 2020 at 18:36):

Do you see the little pen button on the top-right corner?

Patrick Massot (May 30 2020 at 18:36):

(I'm asking because I admin rights on this repo, so I'm not 100% sure what is visible by everybody)

Patrick Massot (May 30 2020 at 18:37):

Please don't edit Section 6 before I say I'm done with it, otherwise we may duplicate efforts.

Paul van Wamelen (May 30 2020 at 18:42):

I see the pen, but because I don't have write permissions it will still create a fork, But I guess that is fine. Can I help with just the styling and some of the English? Top level titles should be all capitals (except for articles and short conjuctions). Next level should at least start with a capital. Others all lower case?

Paul van Wamelen (May 30 2020 at 18:44):

I don't see where to edit this, but want to mention: "This page tracks usual mathematical theories that are or not are in mathlib currently" should be "This page tracks usual mathematical theories that are or are not in mathlib currently"

Patrick Massot (May 30 2020 at 18:46):

Sorry I misunderstood. Technically it does create a fork, but nothing happens on your hard-drive.

Patrick Massot (May 30 2020 at 18:47):

The answer to your second question is: https://github.com/leanprover-community/leanprover-community.github.io/blob/newsite/templates/overview.html

Patrick Massot (May 30 2020 at 18:47):

Fixes to the English and styling are welcome of course

Paul van Wamelen (May 30 2020 at 18:54):

Did a VERY small PR just to see how it works...

Patrick Massot (May 30 2020 at 19:02):

Merged!

Patrick Massot (May 30 2020 at 19:09):

I need reviewers for https://github.com/leanprover-community/leanprover-community.github.io/pull/44, especially @Sebastien Gouezel In this PR I also discuss my general ideas about how to work on these links.

Patrick Massot (May 30 2020 at 19:17):

I should add that this PR took me a lot more time that I anticipated, but I also learned stuff about mathlib (some items were good surprises whose existence in mathlib was unknown to me).

Sebastien Gouezel (May 30 2020 at 19:33):

I am not sure I can see where the threshold is to say we have something. For instance, we don't have a definition of absolutely converging series, but we have the theorem

lemma summable_of_summable_norm {f : ι  α} (hf : summable (λa, f a)) : summable f :=
summable_of_norm_bounded _ hf (assume i, le_refl _)

And I don't think we should (ever) define absolutely converging series, since it is just summable (λa, ∥f a∥), and the interesting bit is the above theorem. Does this mean that we will never consider this item as done in mathlib?

Patrick Massot (May 30 2020 at 19:40):

As I wrote in the PR, there will always be borderline case. If we think something will never be added then it's a good indication something is wrong. We should then either reformulate the line (or even remove it in extreme cases) or link to something close. In this case, I would agree with you if we had converging series instead of summable families.

Patrick Massot (May 30 2020 at 19:41):

I mean I would fill this item with a version of this lemma involving converging series

Sebastien Gouezel (May 30 2020 at 19:44):

But this lemma is stronger than the version for converging series, with

lemma has_sum.tendsto_sum_nat {f :   α} (h : has_sum f a) :
  tendsto (λn:,  i in range n, f i) at_top (𝓝 a)

(in infinite_sum.lean). To me, it only highlights the fact that this curriculum is not optimized for higher-level applications, not a deficiency in mathlib.

Patrick Massot (May 30 2020 at 19:47):

Don't you think we should still have a predicate saying that a series converge? And then people will look for the weaker statement (although its proof will use the stronger one)

Sebastien Gouezel (May 30 2020 at 19:51):

You mean, give a name to the fact that the partial sums tend to to some limit? I don't really have an opinion on this: it wouldn't hurt but it wouldn't be very useful either, except to say that we have all undergrad maths.

Kevin Buzzard (May 30 2020 at 19:53):

Alternatively we could just not fuss and point to something like summable_of_summable_norm and leave it to people to figure out what we mean.

Kevin Buzzard (May 30 2020 at 19:54):

One could similarly argue that we'll never have group homomorphisms because we only have monoid homomorphisms

Patrick Massot (May 30 2020 at 19:54):

Sure, we can use this link, but the question of converging series still stansd

Sebastien Gouezel (May 30 2020 at 19:57):

Same question for positive series. We have a good deal on ennreal and nnreal-valued series in topology/instances/ennreal.lean (notably that an ennreal-valued series always has a sum, that an nnreal-valued one converges if and only if the sum of the ennreal-valued coe is not infinite, and consequences for real-valued series whose terms are all nonnegative. What more could you add?

Patrick Massot (May 30 2020 at 20:02):

Of course for positive series there is nothing to add, they converge only when they are summable

Patrick Massot (May 30 2020 at 20:03):

Does anyone know the English translation of "Réduction des endomorphismes"?

Johan Commelin (May 30 2020 at 20:04):

Context? Analysis?

Patrick Massot (May 30 2020 at 20:08):

It's the grab bag where you put the study of eigenvalues, eigenvectors, trigonalization, Jordan normal form etc.

Patrick Massot (May 30 2020 at 20:09):

Also, given a matrix A, how would you call a polynomial P such that P(A) = 0?

Patrick Massot (May 30 2020 at 20:09):

The yaml file calls it a cancelling polynomial but it sounds fishy to me

Bryan Gin-ge Chen (May 30 2020 at 20:10):

I learned it as the characteristic polynomial.

Johan Commelin (May 30 2020 at 20:12):

I don't know of a name for such polynomials... but knowing that the minimal polynomial divides them is the only interesting property that they have, right?

Alex J. Best (May 30 2020 at 20:12):

Patrick Massot said:

Also, given a matrix A, how would you call a polynomial P such that P(A) = 0?

You mean any polynomial with that property? We have minimal polynomial for the smallest one and characteristic for det(x-A) but otherwise no name for this.

Patrick Massot (May 30 2020 at 20:12):

Yes any polynomial

Bryan Gin-ge Chen (May 30 2020 at 20:13):

Right, I misread. I agree with Alex.

Patrick Massot (May 30 2020 at 20:13):

It feels completely crazy that you don't have a name for this. I need to rethink everything I know about linear algebra to try to express it without this word.

Patrick Massot (May 30 2020 at 20:14):

What about "Réduction des endomorphismes"?

Patrick Massot (May 30 2020 at 20:14):

Does anyone has a translation?

Patrick Massot (May 30 2020 at 20:15):

I need a header for the following list:

    eigenvalue: ''
    eigenvector: ''
    diagonalization: ''
    trigonalization: ''
    endomorphism invariant subspaces: ''
    characteristic subspaces: ''
    kernel lemma: ''
    Dunford decomposition: ''
    Jordan normal form: ''

Bryan Gin-ge Chen (May 30 2020 at 20:15):

Patrick Massot said:

What about "Réduction des endomorphismes"?

Finite-dimensional spectral theory?

Patrick Massot (May 30 2020 at 20:15):

By the way, the translation "kernel lemma" also sounds fishy

Alex J. Best (May 30 2020 at 20:15):

Patrick Massot said:

It feels completely crazy that you don't have a name for this. I need to rethink everything I know about linear algebra to try to express it without this word.

If I had to make one up annihilating polynomial sounds more natural.

Johan Commelin (May 30 2020 at 20:16):

Patrick Massot said:

By the way, the translation "kernel lemma" also sounds fishy

What does it mean?

Alex J. Best (May 30 2020 at 20:16):

Hmm it seems this term is used https://www.maths.ed.ac.uk/~tl/minimal.pdf

Patrick Massot (May 30 2020 at 20:16):

https://fr.wikipedia.org/wiki/Lemme_des_noyaux

Johan Commelin (May 30 2020 at 20:17):

Nope... the only other place on earth where such a lemma exists is in Catalan...

Patrick Massot (May 30 2020 at 20:17):

annihilating polynomial is the direct translation of the French name, I like it

Patrick Massot (May 30 2020 at 20:17):

Seriously, Johan, didn't you study linear algebra?

Johan Commelin (May 30 2020 at 20:18):

Not really... actually. I skipped all the lectures.

Bryan Gin-ge Chen (May 30 2020 at 20:18):

Hmm, a comment on this math stackexchange page suggests "primary decomposition": https://math.stackexchange.com/questions/3077162/name-for-the-kernel-lemma

Patrick Massot (May 30 2020 at 20:21):

So we need to prove this in mathlib. Then people will see this strange name "kernels lemma" and click the link to start learning linear algebra properly.

Patrick Massot (May 30 2020 at 20:23):

I see there is a "unitary ring" line. Do we plan to have non-unital rings in mathib at some point?

Johan Commelin (May 30 2020 at 20:25):

I wouldn't know the axioms... mul_assoc? But not has_one?

Patrick Massot (May 30 2020 at 20:26):

https://en.wikipedia.org/wiki/Ring_(mathematics)#Multiplicative_identity:_mandatory_vs._optional

Johan Commelin (May 30 2020 at 20:26):

I guess the answer to your question is no.

Paul van Wamelen (May 30 2020 at 20:27):

I submitted another PR

Johan Commelin (May 30 2020 at 20:28):

We have noncommutative rings in mathlib... isn't that good enough?

Patrick Massot (May 30 2020 at 20:29):

Crap, this PR is super conflicting what I was doing

Paul van Wamelen (May 30 2020 at 20:31):

I can try and "hand merge" it... Gimme a sec.

Patrick Massot (May 30 2020 at 20:32):

There is no conflict on GitHub. It conflicts my open PR and my local modifications. But it's ok, I'll handle it.

Patrick Massot (May 30 2020 at 20:32):

Let's do both actually: I'll my merge my PR and you'll fix yours

Patrick Massot (May 30 2020 at 20:33):

And then I'll fix conflicts with my local changes

Patrick Massot (May 30 2020 at 20:33):

Done. Now you have conflicts

Kevin Buzzard (May 30 2020 at 20:39):

https://fr.wikipedia.org/wiki/D%C3%A9composition_de_Dunford -- this is the first time I've seen the French choose to name some lemma after someone who isn't French, when there was a perfectly good French option (décomposition de Jordan-Chevalley)

Patrick Massot (May 30 2020 at 20:40):

And how do you say "réduction des endomorphismes"?

Reid Barton (May 30 2020 at 20:41):

Is this "structure theory of endomorphisms"?

Reid Barton (May 30 2020 at 20:41):

I guess that's kind of a mixed metaphor

Paul van Wamelen (May 30 2020 at 20:45):

I think I cleared the conflicts

Patrick Massot (May 30 2020 at 20:47):

Awesome.

Ryan Lahfa (May 30 2020 at 20:53):

Patrick Massot said:

It feels completely crazy that you don't have a name for this. I need to rethink everything I know about linear algebra to try to express it without this word.

My whole problem, I even warned about it before :D

Ryan Lahfa (May 30 2020 at 20:54):

Hahahaha, this thread has really turned into how does you say X in english :'D

Kenny Lau (May 30 2020 at 20:55):

what a surprise, a second language is not just the first language plus a dictionary

Scott Morrison (May 30 2020 at 20:57):

I think we'll eventually want non-unital rings, sadly. For example you might want continuous functions vanishing at infinity on a locally compact space as a non-unital algebra, to state the version of Stone-Weierstrass for locally compact spaces.

Patrick Massot (May 30 2020 at 20:58):

I just pushed some beginning of structure cleanup, but I need to go. Everybody should feel free to work on this file, I won't touch it in the next 10 hours.

Ryan Lahfa (May 30 2020 at 21:02):

Kenny Lau said:

what a surprise, a second language is not just the first language plus a dictionary

But it's surprising for cancelling/annihilating polynomials to not have any equivalent, like while I was learning linear algebra, this term was pronounced like 30 times per day during exercises

Ryan Lahfa (May 30 2020 at 21:02):

And same goes for many terms I guess

Alex J. Best (May 30 2020 at 21:06):

I think we just got away with let PP be a polynomial s.t. P(M)=0P(M) = 0, as its not really longer to say the full definition in this case!

Ryan Lahfa (May 30 2020 at 21:14):

Alex J. Best said:

I think we just got away with let PP be a polynomial s.t. P(M)=0P(M) = 0, as its not really longer to say the full definition in this case!

Yes but sometimes you want to say things like
"Method to compute exp(M)\exp(M) when you have a PP such that P(M)=0P(M) = 0"
vs
"Method to compute exp(M)\exp(M) using an annhilating polynomial"

Ryan Lahfa (May 30 2020 at 21:15):

Anyway, I'm getting sidetracked… :D

Kevin Buzzard (May 30 2020 at 21:26):

Hecke algebras are something which will be within reach soon, and they're rings without 1

Johan Commelin (Jun 01 2020 at 09:01):

#5 is about affine spaces. I'm kicking #2816 on the merge queue. Once it lands, we can fill out this section. @Joseph Myers please let us know if you would like to contribute.

Johan Commelin (Jun 01 2020 at 09:02):

@Oliver Nash and/or @Anne Baanen Would you mind filling out #4 on bilinear and quadratic forms?

Johan Commelin (Jun 01 2020 at 09:03):

If any of you doesn't have time/energy/interest in contributing, just say so. No hard feelings.

Johan Commelin (Jun 01 2020 at 09:06):

#7 is on single variable complex analysis, and it's going to make us look ridiculous...

Johan Commelin (Jun 01 2020 at 09:08):

I'll start on #8. Topology now.

Patrick Massot (Jun 01 2020 at 09:09):

Maybe it would make more sense to work on an algebraic section since I would have an easier time doing topology than algebra

Johan Commelin (Jun 01 2020 at 09:12):

The first item is interesting. We don't have metric_space.to_topological_space I guess. So what do we do? metric_space.to_uniform_space?

Patrick Massot (Jun 01 2020 at 09:15):

I found rather link a lemma saying something is open if it contains an open ball around each point, or something like that

Johan Commelin (Jun 01 2020 at 09:16):

Aha, makes sense

Johan Commelin (Jun 01 2020 at 09:17):

The remaining sections are:

#09. Differential Calculus
#10. Integral Calculus
#11. Probability Theory
#12. Distribution calculus
#13. Numerical Analysis

I fear that the last 3 will stay empty.

Patrick Massot (Jun 01 2020 at 09:18):

Don't we have at least the definition of a probability measure?

Johan Commelin (Jun 01 2020 at 09:19):

pmf ­– Probability mass function

Johan Commelin (Jun 01 2020 at 09:19):

But otherwise, not much, I think

Oliver Nash (Jun 01 2020 at 09:24):

Johan Commelin said:

Oliver Nash and/or Anne Baanen Would you mind filling out #4 on bilinear and quadratic forms?

I would be delighted to fill this out. I'll try and find time this evening though it might not happen till tomorrow.

Patrick Massot (Jun 01 2020 at 09:24):

Don't hesitate to reorder and slightly reword stuff if it makes more sense.

Oliver Nash (Jun 01 2020 at 09:24):

Thanks, will do. Needless to say I'm happy for @Anne Baanen to do this too / instead.

Patrick Massot (Jun 01 2020 at 09:25):

Also keep in mind the structure is not yet fully compliant. We want to have exactly three levels: main heading, sub heading, leaf containing a link.

Oliver Nash (Jun 01 2020 at 09:25):

Understood, I will stick to a three-level structure.

Johan Commelin (Jun 01 2020 at 09:26):

Thanks for helping!

Oliver Nash (Jun 01 2020 at 09:26):

My pleasure!

Johan Commelin (Jun 01 2020 at 09:33):

https://github.com/leanprover-community/leanprover-community.github.io/pull/48 fills links in basic topology (there's a lot left for the experts :wink:)

Johan Commelin (Jun 01 2020 at 09:35):

Note: affine spaces have been merged

Patrick Massot (Jun 01 2020 at 09:36):

Ok, I merged but indeed we have several more links to add to this section. I'll do it right now

Patrick Massot (Jun 01 2020 at 09:38):

Each time I type leanproject up in mathlib, elan downloads something... :grinning:

Patrick Massot (Jun 01 2020 at 10:09):

Why can't I find that a real normed space is finite-dimensional iff the unit ball is compact? Is it really missing?

Patrick Massot (Jun 01 2020 at 10:15):

I've updated the metric topology section.

Sebastien Gouezel (Jun 01 2020 at 10:24):

The useful implication is there (finite_dimensional.proper). The useless implication has been done by a student of Kevin, if I recall correctly, but it never made it into mathlib.

Kevin Buzzard (Jun 01 2020 at 10:25):

https://github.com/LAC1213/compact_unit_ball

Patrick Massot (Jun 01 2020 at 10:28):

Ok, so I can't really tick that one off. Too bad this project never went to mathlib...

Ryan Lahfa (Jun 01 2020 at 10:34):

Patrick Massot said:

Ok, so I can't really tick that one off. Too bad this project never went to mathlib...

If there was a license, this could be salvaged

Patrick Massot (Jun 01 2020 at 10:34):

I'm pretty sure you can discuss this with the author. That would be a nice little project.

Patrick Massot (Jun 01 2020 at 10:35):

Of course turning this into something PRable means work.

Patrick Massot (Jun 01 2020 at 10:35):

But it would be a nice way to get familiar with both linear algebra and topology in mathlib.

Sebastien Gouezel (Jun 01 2020 at 10:40):

If I remember correctly, there is the useless assumption that the field is complete in this project, but this is not crazy to have this assumption.

David Wärn (Jun 01 2020 at 10:57):

Shouldn't this argument be phrased using docs#riesz_lemma ?

Patrick Massot (Jun 01 2020 at 11:09):

Indeed it looks like someone started this road but gave up.

Patrick Massot (Jun 01 2020 at 11:10):

It seems to be Jean. @Jean Lo what is the status of this?

Joseph Myers (Jun 01 2020 at 11:47):

What I defined for affine spaces is very minimal at present, so there won't be much from that list (on the Euclidean side, I suppose #2865 provides at least "Angles of vectors"). It's not yet PRed, but I do have the result that (not necessarily bijective) isometries between Euclidean affine spaces are affine maps that preserve the inner product (the list wants rather more about isometries than that, however).

Johan Commelin (Jun 01 2020 at 11:58):

@Joseph Myers Sure... but all small bits help.

Patrick Massot (Jun 01 2020 at 12:13):

Joseph, did you coordinate with https://leanprover-community.github.io/mathlib_docs/analysis/normed_space/mazur_ulam.html?

Johan Commelin (Jun 01 2020 at 12:25):

Is "C is algebraically closed" somewhere on the agreg list?

Patrick Massot (Jun 01 2020 at 13:52):

I hope so

Patrick Massot (Jun 01 2020 at 13:53):

https://github.com/leanprover-community/leanprover-community.github.io/blob/newsite/data/overview.yaml#L183

Joseph Myers (Jun 01 2020 at 15:13):

@Patrick Massot No, I just wrote a separate proof (for Euclidean spaces, the (easy) result isn't limited to bijective isometries, and the "preserves inner product" part is something useful for describing the effect of an isometry (from a finite-dimensional space to itself) on coordinates, once a frame has been chosen, as the combination of an orthogonal matrix and a translation).

Yury G. Kudryashov (Jun 01 2020 at 15:15):

Actually, you don't need a Euclidean space here. Only a normed_add_torsor over a normed_vector_space with strictly convex balls.

Yury G. Kudryashov (Jun 01 2020 at 15:20):

Actually you can prove the following fact. Let f be an isometry, and its codomain is a normed_add_torsor R E such that 0 < r → dist x y = r → dist x z = r → r < dist x (2 * y - z). Then f is affine.

Johan Commelin (Jun 01 2020 at 15:22):

Patrick Massot said:

https://github.com/leanprover-community/leanprover-community.github.io/blob/newsite/data/overview.yaml#L183

I've never heard of this name before...

Joseph Myers (Jun 01 2020 at 15:24):

Feel free to add these more general results! I think for isometries of Euclidean spaces there should be a function mapping f (such that isometry f) to an affine_map (for whatever type classes that include the case of Euclidean spaces), and a proof that the corresponding linear_map preserves the inner product, but I'm not particularly concerned with how we get there.

Yury G. Kudryashov (Jun 01 2020 at 15:27):

BTW, do you prove that for an affine isometry the corresponding linear_map is an isometry as well?

Ryan Lahfa (Jun 01 2020 at 15:28):

Johan Commelin said:

Patrick Massot said:

https://github.com/leanprover-community/leanprover-community.github.io/blob/newsite/data/overview.yaml#L183

I've never heard of this name before...

https://fr.wikipedia.org/wiki/Th%C3%A9or%C3%A8me_fondamental_de_l%27alg%C3%A8bre
That's the name we give it, maybe we love too much to give names to theorem.
I even heard that the fact that the continuous image of a compact is a compact is called Weierstrass' theorem :D in France…

Yury G. Kudryashov (Jun 01 2020 at 15:29):

English Wikipedia never mentions this name, just "Fundamental theorem of algebra"

Ryan Lahfa (Jun 01 2020 at 15:30):

That's an invitation to change the name into "fundamental theorem of algebra" I believe

Yury G. Kudryashov (Jun 01 2020 at 16:08):

https://github.com/leanprover-community/leanprover-community.github.io/commit/bebb1e9cafaee64414639bc9714f09d9b124ca0f

Patrick Massot (Jun 01 2020 at 16:25):

Some algebraists will hate you Yury. I know more than one that is really pissed off when an analysis theorem is called the "fundamental theorem of algebra".

Kevin Buzzard (Jun 01 2020 at 16:27):

It's because algebra := polynomials and matrices in 1800 or something, right?

Yury G. Kudryashov (Jun 01 2020 at 17:00):

@Patrick Massot Is there a title that is both widely recognizable (in English) and won't make algebraists hate me?

Johan Commelin (Jun 01 2020 at 17:02):

The algebraists should be happy that they have opportunity to invade the territory of the analysts!
Geometers don't even have a "fundamental theorem".... look at them :stuck_out_tongue_wink:

Patrick Massot (Jun 01 2020 at 17:55):

The title could be "C\mathbb C is algebraically closed"...

Johan Commelin (Jun 01 2020 at 17:56):

Such a boring theorem name... you've been influenced too much by mathlib naming conventions.

Patrick Massot (Jun 01 2020 at 17:58):

I can see you don't know what this theorem is called in mathlib...

Johan Commelin (Jun 01 2020 at 17:58):

polynomial.complex_exists_root?

Johan Commelin (Jun 01 2020 at 17:58):

That's just because we don't have class algebraically_closed (K : Type*) [field K] yet.

Johan Commelin (Jun 01 2020 at 17:59):

Otherwise it would be complex.algebraically_closed.

Joseph Myers (Jun 01 2020 at 20:01):

@Yury G. Kudryashov I didn't prove that particular result that the corresponding linear_map is an isometry, but it's a straightforward consequence of the other facts in this area.

Yury G. Kudryashov (Jun 01 2020 at 21:33):

E.g., from #2907

Joseph Myers (Jun 02 2020 at 01:09):

Actually it's true more generally than that, for the map (at a particular base point) on vectors induced by any isometry between two normed_add_torsors. Does this belong in mathlib?

import analysis.normed_space.add_torsor
import topology.metric_space.isometry

variables (V1 : Type*) {P1 : Type*} [normed_group V1] [metric_space P1] [normed_add_torsor V1 P1]
variables (V2 : Type*) {P2 : Type*} [normed_group V2] [metric_space P2] [normed_add_torsor V2 P2]

/-- The map on vectors corresponding to a map from P1 to P2, at a base
point p. -/
def vector_map_of_point_map (f : P1  P2) (p : P1) : V1  V2 := λ v, f (v + p) - f p

/-- The map described by `vector_map_of_point_map` is an isometry if
the original map is one. -/
lemma isometry_vector_map_of_point_map {f : P1  P2} (h : isometry f) (p : P1) :
  isometry (vector_map_of_point_map V1 V2 f p) :=
begin
  rw isometry_emetric_iff_metric at *,
  unfold vector_map_of_point_map,
  intros x y,
  rw [dist_eq_norm, dist_eq_norm, add_torsor.vsub_sub_vsub_right_cancel],
  convert h (x + p) (y + p),
  { rw add_torsor.dist_eq_norm V2 },
  { rw [add_torsor.dist_eq_norm V1, add_torsor.vsub_vadd_eq_vsub_sub, add_torsor.vadd_vsub] }
end

Johan Commelin (Jun 02 2020 at 04:42):

@Joseph Myers I think it does, but I wouldn't make a new definition. (Or at least, don't use the definition in the lemma. Rather, take any random map g : V1 → V2 and the hypothesis hg : \forall v, g v = f (v +ᵥ p) -ᵥ f p. In this way, the lemma will also be applicable to maps that aren't definitionally a vector_map_of_point_map. My intuition says that is what will happen in practice.

Yury G. Kudryashov (Jun 02 2020 at 05:04):

Note that with #2907 you can represent your map as a composition of known isometries, and get the proof from isometry.comp.

Yury G. Kudryashov (Jun 02 2020 at 05:05):

Probably we should stop hijacking Patrick's thread.

Johan Commelin (Jun 02 2020 at 08:54):

@Ryan Lahfa There's something wrong with the statement-todo and statement-done classes. Currently cards are also getting these classes, but not in an intuitive way.

Johan Commelin (Jun 02 2020 at 08:54):

I think a card should only be marked statement-done if all of its children are completely done.

Johan Commelin (Jun 02 2020 at 08:54):

Otherwise our todo-list is much too optimistic.

Johan Commelin (Jun 02 2020 at 08:57):

image.png
This doesn't really look as I would expect. The todo toggle seems to be inverted...

Johan Commelin (Jun 02 2020 at 08:57):

I'm seeing todo's but the toggle is off, and when I switch it on, the items that are not links go away

Ryan Lahfa (Jun 02 2020 at 09:20):

Johan Commelin said:

Ryan Lahfa There's something wrong with the statement-todo and statement-done classes. Currently cards are also getting these classes, but not in an intuitive way.

There might be a bug

Ryan Lahfa (Jun 02 2020 at 09:21):

I'll look into it

Johan Commelin (Jun 02 2020 at 09:21):

Thanks!

Johan Commelin (Jun 02 2020 at 09:21):

Alternative: strip out the classes and generate two files...

Ryan Lahfa (Jun 02 2020 at 09:21):

Johan Commelin said:

I'm seeing todo's but the toggle is off, and when I switch it on, the items that are not links go away

I think it's also due to the fact you don't want to show parts when they are empty (e.g. all children are todos), but I'm not sure, I'll look at it again

Ryan Lahfa (Jun 02 2020 at 09:22):

Hahahaha

Johan Commelin (Jun 02 2020 at 09:22):

Let's just make sure that the list works for the IAS talk, and then we can add the fancy buttons afterwards.

Ryan Lahfa (Jun 02 2020 at 09:23):

Agreed ; if I don't find a trivial solution quickly enough, I'll send directly a PR to produce two files, sounds good?

Kevin Buzzard (Jun 02 2020 at 09:47):

So I'm having a look at the current state of this (the yaml file). For "direct sum" (line 12) we have the unnamed instance direct_sum.semimodule. This is an "external direct sum". From the context of the list it looks like an internal direct sum though, i.e. a sum of two submodules within a big module, where the submodules happen to have trivial intersection. Should we just not care and link to the external direct sum? And can one link to an unnamed instance name?

Johan Commelin (Jun 02 2020 at 09:48):

Internal direct sum = sup in the lattice semimodule _ _??

Kevin Buzzard (Jun 02 2020 at 09:48):

It's no different to internal sum though

Johan Commelin (Jun 02 2020 at 09:50):

internal direct sum is an awkard notion, where you want to know that things are orthogonal, and then take a sup.

Kevin Buzzard (Jun 02 2020 at 09:51):

I remember learning this as an UG too. I think the idea is that abstract direct sum of two vector spaces is supposed to be too difficuilt, and this internal direct sum -- if V and W are subspaces of some large vector space X and V and W intersect trivially, then the space spanned by V and W satisfies the universal property of the abstact direct sum -- was taught first.

Johan Commelin (Jun 02 2020 at 09:51):

We just totalise the function...

Johan Commelin (Jun 02 2020 at 09:51):

And define it for non-othogonal submodules as well

Patrick Massot (Jun 02 2020 at 09:58):

The idea is to find a good entry point for people that may not know much about formalization, but want to use this notion. Sometimes the best entry point for a definition is actually a lemma saying that some funny mathliby way of doing stuff is giving you the expected behavior.

Kevin Buzzard (Jun 02 2020 at 10:16):

https://github.com/leanprover-community/leanprover-community.github.io/pull/50 bilinear and quadratic forms

Patrick Massot (Jun 02 2020 at 10:18):

Merged!

Patrick Massot (Jun 02 2020 at 10:18):

But I'll probably need to fix structure

Kevin Buzzard (Jun 02 2020 at 10:19):

Did I do something wrong? Let me know now because I'm about to start on affine spaces

Kevin Buzzard (Jun 02 2020 at 10:19):

And I didn't know how to check if the links work.

Kevin Buzzard (Jun 02 2020 at 10:19):

(e.g. I might have missed a namespace)

Patrick Massot (Jun 02 2020 at 10:22):

Patrick Massot said:

Don't hesitate to reorder and slightly reword stuff if it makes more sense.

Also keep in mind the structure is not yet fully compliant. We want to have exactly three levels: main heading, sub heading, leaf containing a link.

Patrick Massot (Jun 02 2020 at 10:22):

Hold on for two minutes

Patrick Massot (Jun 02 2020 at 10:26):

You can have a look at https://github.com/leanprover-community/leanprover-community.github.io/commit/90a877595a2bc219ac0642d1f9d6fae477f15972

Patrick Massot (Jun 02 2020 at 10:27):

That's what I call "fixing structure", following the guidelines quoted above.

Kevin Buzzard (Jun 02 2020 at 10:27):

I see, so actually changing the structure of the yaml to be a bit more sane

Kevin Buzzard (Jun 02 2020 at 10:28):

keep precisely the same leaves but we can move them around a bit

Patrick Massot (Jun 02 2020 at 10:28):

Yes. Actually I'm pretty disappointed by the source document. I thought it was more structured.

Kevin Buzzard (Jun 02 2020 at 10:28):

it probably wasn't written by a computer scientist!

Johan Commelin (Jun 02 2020 at 10:28):

https://github.com/leanprover-community/leanprover-community.github.io/commit/90a877595a2bc219ac0642d1f9d6fae477f15972#diff-25c153ec778dc59bca8f669ad98bcad4R241
Should that be cross product?

Patrick Massot (Jun 02 2020 at 10:29):

Sometimes I even change leaves a bit (and I added Jordan normal form). But the main point is that leaves should be at level 3.

Patrick Massot (Jun 02 2020 at 10:29):

https://en.wikipedia.org/wiki/Triple_product

Patrick Massot (Jun 02 2020 at 10:29):

Oh, the preceding line is a wrong translation

Patrick Massot (Jun 02 2020 at 10:30):

"vector product" means cross product

Johan Commelin (Jun 02 2020 at 10:30):

I'm learning new stuff everyday...

Patrick Massot (Jun 02 2020 at 10:30):

But we call it "produit vectoriel" in French.

Kevin Buzzard (Jun 02 2020 at 10:30):

We don't have any of these crazy things which assume finite-dimensionality (or in this case 3-dimensionality)

Patrick Massot (Jun 02 2020 at 10:30):

The triple product thins is about computing determinants using the Euclidean structure

Kevin Buzzard (Jun 02 2020 at 10:30):

3 is overrated

Patrick Massot (Jun 02 2020 at 10:31):

That's why I named this section "low dimensions"

Kevin Buzzard (Jun 02 2020 at 10:31):

why not just call it n-ary product and link to det :-)

Patrick Massot (Jun 02 2020 at 10:31):

The fact that you can compute determinants using the Euclidean structure has some content

Patrick Massot (Jun 02 2020 at 10:32):

But I wouldn't say this has super high priority, unless you specifically work towards low-hanging fruits in this list

Ryan Lahfa (Jun 02 2020 at 10:45):

Kevin Buzzard said:

We don't have any of these crazy things which assume finite-dimensionality (or in this case 3-dimensionality)

That's for people who does physics

Patrick Massot (Jun 02 2020 at 10:51):

I thought physics was all about dimension 4.

Kevin Buzzard (Jun 02 2020 at 10:55):

I thought 10?

Ryan Lahfa (Jun 02 2020 at 11:07):

Sometimes they forget about time and wrapped dimensions, :-°

Johan Commelin (Jun 02 2020 at 13:15):

@Yury G. Kudryashov Didn't you do stuff on Grönwell in mathlib at some point? I can't find it.

Yury G. Kudryashov (Jun 02 2020 at 13:16):

https://leanprover-community.github.io/mathlib_docs/analysis/ODE/gronwall.html

Johan Commelin (Jun 02 2020 at 13:17):

Aah, I made a typo...

Johan Commelin (Jun 02 2020 at 13:18):

Thanks!

Johan Commelin (Jun 02 2020 at 13:21):

We don't really have a definition of a sigma algebra :expressionless:

Yury G. Kudryashov (Jun 02 2020 at 13:22):

We have [measurable α]

Johan Commelin (Jun 02 2020 at 13:24):

Yup... it's just that the name isn't recognisable

Johan Commelin (Jun 02 2020 at 13:30):

I've filled in a couple more links in analysis and measure theory. The part on integration I didn't really touch... I've never used that part of the library.

Sebastien Gouezel (Jun 02 2020 at 13:35):

A sigma algebra is exactly an instance of measurable_space α

Johan Commelin (Jun 02 2020 at 13:40):

It's just that the list has 'measureable spaces' and 'sigma algebras' as seperate items :expressionless:

Reid Barton (Jun 02 2020 at 13:42):

We also have measurable spaces https://github.com/leanprover-community/mathlib/blob/master/src/measure_theory/category/Meas.lean#L31 :upside_down:

Gabriel Ebner (Jun 02 2020 at 13:43):

What is the difference between a measurable space and a set with a sigma algebra?

Reid Barton (Jun 02 2020 at 13:46):

Those are the same, the issue is that (by analogy with group, etc.) the structure measurable_space is named after the bundled concept, when it actually is the unbundled one. Same with topological_space.

Johan Commelin (Jun 02 2020 at 13:51):

We really need this automated "rename declarations" bot, that will just go through the entire source to rename things while I sleep.

Patrick Massot (Jun 02 2020 at 13:55):

Thanks Johan. Some items are wrong and a lot are missing but it still helps. I'll merge it and improve it.

Reid Barton (Jun 02 2020 at 13:56):

FWIW I'm not suggesting renaming the mathlib definitions, just explaining why they don't exactly align with the math names: basically because we don't really use the bundled objects so we have just one name for both "measurable space" and "sigma-algebra".

Patrick Massot (Jun 02 2020 at 14:02):

I think the module docstring of https://leanprover-community.github.io/mathlib_docs/measure_theory/measure_space.html could be easier to read...

Sebastien Gouezel (Jun 02 2020 at 14:09):

Ah, this is a docstring from the ancient times!

Patrick Massot (Jun 02 2020 at 14:09):

Sébastien, do you know whether counting measures are hidden somewhere?

Patrick Massot (Jun 02 2020 at 14:10):

And non-discrete probability measures?

Sebastien Gouezel (Jun 02 2020 at 14:33):

The counting measure is in measure_space.lean

/-- Counting measure on any measurable space. -/
def count : measure α := sum dirac

Johan Commelin (Jun 02 2020 at 14:37):

Patrick Massot said:

Thanks Johan. Some items are wrong and a lot are missing but it still helps. I'll merge it and improve it.

Sorry for the mistakes

Patrick Massot (Jun 02 2020 at 14:39):

Oh, I should have checked here before pushing, I missed Sébastien's message.

Johan Commelin (Jun 02 2020 at 14:41):

You can push again... it's free.

Patrick Massot (Jun 02 2020 at 14:42):

Done

Patrick Massot (Jun 02 2020 at 14:42):

@Sebastien Gouezel would you mind going over https://github.com/leanprover-community/leanprover-community.github.io/blob/c2631dcdfe279ebe5869eb62e6289a6e7d426681/data/overview.yaml#L505-L585 to tell us if we missed stuff?

Sebastien Gouezel (Jun 02 2020 at 14:47):

Monotone convergence is lintegral_supr_ae in integration.lean.

Sebastien Gouezel (Jun 02 2020 at 14:48):

Fatou is lintegral_liminf_le in integration.lean.

Sebastien Gouezel (Jun 02 2020 at 14:49):

By the way, just before Fatou there are the two lines

-- for some reason the next proof fails without changing the priority of this instance
local attribute [instance, priority 1000] classical.prop_decidable

It won't be a surprise to anyone that, with current awesome Lean, they can be safely removed.

Patrick Massot (Jun 02 2020 at 14:51):

I just skipped that file because it seems to be all about the mysterious ∫⁻. Isn't there a version for actual integrals?

Sebastien Gouezel (Jun 02 2020 at 14:57):

The usual textbook versions of these theorems are for nonnegative functions that are allowed to take the value ++\infty, so they really talk about the ∫⁻. I just checked in Rudin, for instance, and both monotone convergence and Fatou's lemma are just given in this version.

Patrick Massot (Jun 02 2020 at 14:59):

Thanks. We really need some md file describing how to navigate that part of mathlib.

Johan Commelin (Jun 02 2020 at 15:00):

Well, a yaml file is a good first start (-;

Patrick Massot (Jun 02 2020 at 15:01):

The YaML file doesn't explain what this crazy ∫⁻ symbol means

Patrick Massot (Jun 02 2020 at 15:03):

Sébastien, since you're clearly not working on this referee report, would you mind handling Section 9?

Patrick Massot (Jun 02 2020 at 15:03):

https://github.com/leanprover-community/leanprover-community.github.io/edit/newsite/data/overview.yaml

Sebastien Gouezel (Jun 02 2020 at 15:03):

I got through the interesting part of the paper, now it's the boring technical part, so any excuse for procrastination is good. I'll have a look.

Patrick Massot (Jun 02 2020 at 15:05):

At this stage you can write to the editor: I think the theorem is interesting and the new ideas are nice, now I'm waiting for the formalization of the technical details.

Sebastien Gouezel (Jun 02 2020 at 15:13):

People still need to get their paper published in a reasonable amount of time, especially if they're young. I could do this when I refer papers whose authors are all tenured :)

Johan Commelin (Jun 02 2020 at 15:14):

If that catches on, you'll find authors scrambling for getting a phd student or postdoc as coauthor

Patrick Massot (Jun 03 2020 at 18:14):

@Ryan Lahfa since you didn't fix the bugs quickly enough for my talk, I went ahead and split the display into two files. I also added a link.

Patrick Massot (Jun 03 2020 at 18:15):

I also cleaned up the remaining sections so that the structure should be consistent now. I'm convinced there are still missing links, but people should now track them by comparing https://leanprover-community.github.io/undergrad_todo.html with what they think is in mathlib.

Sebastien Gouezel (Jun 03 2020 at 18:42):

Patrick Massot said:

Ryan Lahfa since you didn't fix the bugs quickly enough for my talk, I went ahead and split the display into two files. I also added a link.

How did the talk go, by the way?

Johan Commelin (Jun 03 2020 at 18:43):

It's at 1200 tonight

Johan Commelin (Jun 03 2020 at 18:43):

So around 1215, Patrick is going to demo Zulip, and we should all be making silly jokes

Gabriel Ebner (Jun 03 2020 at 18:43):

I'm sorry the widgets didn't make it in time for the talk, but the vscode extension still has some rough edges and Ed is a bit busy at the moment.

Gabriel Ebner (Jun 03 2020 at 18:44):

@Johan Commelin Which timezone?

Johan Commelin (Jun 03 2020 at 18:46):

Midnight in Amsterdam, Paris, Berlin

Johan Commelin (Jun 03 2020 at 18:46):

I think it's 1800 Princeton time

Gabriel Ebner (Jun 03 2020 at 18:47):

So in 3 hours, i.e. 24:00? I was confused by the 12.

Patrick Massot (Jun 03 2020 at 18:47):

It's getting dangerously close.

Reid Barton (Jun 03 2020 at 18:47):

I see 5:30 pm on the IAS website which I assume is US/Eastern

Patrick Massot (Jun 03 2020 at 18:47):

Yes, 3 hours

Patrick Massot (Jun 03 2020 at 18:47):

5:30 is the beginning of discussions, but the talk starts half an hour later.

Patrick Massot (Jun 03 2020 at 18:47):

It's a crazy format.

Reid Barton (Jun 03 2020 at 18:48):

Interesting idea to discuss the talk before it happens

Patrick Massot (Jun 03 2020 at 18:48):

I replaces a very informal seminar featuring wine and cheese.

Patrick Massot (Jun 03 2020 at 18:48):

Before the talk peoples are randomly distributed in Zoom rooms with 6 participants.

Patrick Massot (Jun 03 2020 at 18:49):

Then there is the talk and then general discussion.

Kevin Buzzard (Jun 03 2020 at 20:23):

We had this with my OWLS talk and it worked really well, but we did it after not before.

Patrick Massot (Jun 04 2020 at 00:21):

The talk went fine, discussion just stopped (almost two hours after the talk stopped).

Johan Commelin (Jun 04 2020 at 14:55):

#2946 Eisenstein criterion (thanks @Chris Hughes :tada: ) is on the merge queue.

Johan Commelin (Jun 04 2020 at 14:55):

So we can update this yaml in a moment (-;

Johan Commelin (Jun 04 2020 at 15:28):

@Patrick Massot @Bryan Gin-ge Chen What do you think of hosting things like overview.yaml in mathlib? Then PRs that add new stuff can also add it to that file directly.

Johan Commelin (Jun 04 2020 at 15:29):

(And it makes it easier for a reviewer to say: Hey, please update that file as well.)

Patrick Massot (Jun 04 2020 at 15:40):

Of course I don't have anything against that. I don't know what would be the best strategy. Maybe the website CI could simply download the file from mathlib before running the site building script.

Bryan Gin-ge Chen (Jun 04 2020 at 15:41):

I think it's probably a good idea. Moving overview.yaml to mathlib will change an informal dependency (we have to remember to make changes in two repos) to a technical one (rebuilding the website will require wget from mathlib github as Patrick says).

Johan Commelin (Jun 04 2020 at 15:41):

Yup, that's the kind of thing I was meaning

Johan Commelin (Jun 04 2020 at 15:41):

Same applies to 100.yaml

Johan Commelin (Jun 04 2020 at 15:41):

And stacks.yaml, when we ever get there (-;

Patrick Massot (Jun 04 2020 at 15:42):

The case of 100.yaml is slightly different because it also lists stuff from outside mathlib

Johan Commelin (Jun 04 2020 at 15:43):

But only very little right? Even archive/ is in the mathlib repo

Johan Commelin (Jun 04 2020 at 15:43):

So it's only CH that is outside, I think.

Patrick Massot (Jun 04 2020 at 15:44):

We also have more polishing work to be done on this list stuff. We only have the minimal version. We need to get a better idea about interaction between this list and https://leanprover-community.github.io/mathlib-overview.html.

Patrick Massot (Jun 04 2020 at 15:45):

One option is to rename overview.yaml into undergrad.yaml, create a file advanced_topics.yaml for everything else, and start by porting whatever is list in the overview page but not in the undergrad page to this new file.

Patrick Massot (Jun 04 2020 at 15:46):

The border between undergrad and the rest is pretty blurry, but I think it's interesting anyway.

Patrick Massot (Jun 04 2020 at 15:46):

Because it allows to also have https://leanprover-community.github.io/undergrad_todo.html which would not make sense with an open ended scope.

Patrick Massot (Jun 04 2020 at 15:47):

Also note that I don't have anything against resurrecting the switches gathering stuff and todo stuff on the same page, but they were simply too buggy for now.

Johan Commelin (Jun 04 2020 at 15:49):

Yup, no worries.

Johan Commelin (Jun 04 2020 at 15:49):

I think the switches are more user friendly (when they work correctly). But separate pages is developer friendly, and that's also worth something :rofl:

Patrick Massot (Jun 04 2020 at 15:54):

Yesterday I also modified Ryan's python code at https://github.com/leanprover-community/leanprover-community.github.io/blob/newsite/make_site.py#L134 in a way that would probably make it easier to fix the bugs. In defense of Ryan's code, I need to say that he worked on a badly specified issue. It wasn't clear in the beginning what kind of structure we wanted to support. The idea that we want exactly three levels (topic, subtopic, item) emerged while working on the list. This is now fully enforced in the YaML file (unless I missed something) and this should make everything easier (including CSS styling).

Patrick Massot (Jun 05 2020 at 21:45):

Another call to contributions: now that the list is visible on the website, it would be nice to write the little piece of CI that checks that urls don't break (and are correct to start with). One needs to be careful since having a successful http request is not enough to guarantee that the anchor is there: requesting https://leanprover-community.github.io/mathlib_docs/topology/basic.html#poincare_conjecture will not give you any http error.

Johan Commelin (Oct 05 2021 at 14:26):

I think it is time to go through https://leanprover-community.github.io/undergrad_todo.html again, to check if some stuff has been done already. Here's a first set of remarks/questions. I think there is more.

Linear algebra

  • @Sebastien Gouezel Didn't you do Gaussian elimination
  • Is the matrix exponential now a consequence of some very general exponential in Banach algebras or something?
  • The special linear group is done, I think

Group theory

  • Maschke is done a PR exists for this: #9398

Ring theory

  • Algebra over a commutative ring. @Patrick Massot do you mean something that docs#algebra doesn't provide?
  • rational fraction fields with one indeterminate over a field: #9563

Bilinear and Quadratic Forms Over a Vector Space

  • real classification --- is this something else than Sylvester's inertia? Because we have that

Bryan Gin-ge Chen (Oct 05 2021 at 14:39):

#9398 by @Scott Morrison addresses Maschke.

Sebastien Gouezel (Oct 05 2021 at 14:41):

There are many flavors of gaussian elimination. The most classical one is where you are only allowed operations on the rows of a matrix, but where you need sometimes to exchange two rows, if there is a zero at the bad place. I did another version where I don't exchange two rows, but where I do operations on rows and columns. I am not sure it qualifies as gaussian elimination (although it is just as good in practice, and in fact better for what I wanted to do (docs#measure_theory.measure.map_linear_map_add_haar_eq_smul_add_haar) since it avoids the discussion of rows exchanges).

Patrick Massot (Oct 05 2021 at 14:44):

I agree this list needs cleaning (probably also remove a couple of meaningless items and fix some translations mistakes). The reason why algebra is not crossed out is I guess we waited to have non associative algebras (or even non-unital?). I don't know what is the current status.

Johan Commelin (Oct 05 2021 at 14:44):

@Eric Wieser @Oliver Nash we have non assoc rings now? How about algebras?

Patrick Massot (Oct 05 2021 at 14:46):

About Maschke, do we have the usual statement (involving sums of irreducible representations) now?

Oliver Nash (Oct 05 2021 at 14:46):

Yes, though it's not quite as pretty as it might be. E.g., we have docs#non_assoc_semiring but no non_assoc_ring.

Patrick Massot (Oct 05 2021 at 14:48):

The question about algebra is: do we have a structure that cover both the docs#algebra and docs#lie_algebra?

Oliver Nash (Oct 05 2021 at 14:50):

Johan Commelin said:

Eric Wieser Oliver Nash we have non assoc rings now? How about algebras?

Also since our bundled algebra class is (unfortunately) still stuck in the (unital) associative world, the following is how to declare a non-assoc algebra:

variables (R A : Type*) [comm_semiring R] [non_assoc_semiring A]
variables [module R A] [is_scalar_tower R A A] [smul_comm_class R A A]

Patrick Massot (Oct 05 2021 at 14:50):

About matrix exponential, I guess we are missing some glue, but maybe I'm wrong. @Anatole Dedecker ?

Patrick Massot (Oct 05 2021 at 14:51):

Oliver, this has a unit, right? It doesn't happen so often for Lie algebras.

Oliver Nash (Oct 05 2021 at 14:51):

Yes, that has a unit. There is a flavour without a unit. You just write non_unital_non_assoc_semiring A.

Yury G. Kudryashov (Oct 05 2021 at 14:51):

I have a definition of exp that works in any Banach algebra.

Yury G. Kudryashov (Oct 05 2021 at 14:51):

I mean, in a local branch.

Yury G. Kudryashov (Oct 05 2021 at 14:51):

And defined using analytic functions.

Yury G. Kudryashov (Oct 05 2021 at 14:52):

I think that eventually we should replace complex.exp and real.exp with this definition but it's not PR-ready yet.

Yury G. Kudryashov (Oct 05 2021 at 14:52):

(and I don't have a migration path yet).

Patrick Massot (Oct 05 2021 at 14:53):

Yury, we already have https://github.com/leanprover-community/mathlib/blob/ef139bd08ff414f0f6354461d26274c18a6c405d/src/analysis/normed_space/exponential.lean

Yury G. Kudryashov (Oct 05 2021 at 14:54):

Indeed. Then just ignore my comments.

Patrick Massot (Oct 05 2021 at 14:55):

Actually it probably requires no glue. We should check that type class inference is happy to provide this on real or complex valued matrices and selected one declaration to link.

Patrick Massot (Oct 05 2021 at 14:56):

And I agree it would be nice to replace the elementary versions, but clearly mathlib is going in the opposite direction (removing calculus from proofs about exponential to untangle calculus and measure theory).

Oliver Nash (Oct 05 2021 at 14:56):

Patrick Massot said:

The question about algebra is: do we have a structure that cover both the docs#algebra and docs#lie_algebra?

Sort of. Since Lie algebras use the has_bracket typeclass and rings use the has_mul typeclass, it's not quite so simple. I believe the only place where we connect these two worlds is in the construction of the free Lie algebra as a quotient of the free non-unital, non-associative algebra.

E.g., here a has_mul is turned into a has_bracket: https://github.com/leanprover-community/mathlib/blob/5926f103c66a17a60eafc1aaec387d9db85a21ad/src/algebra/lie/free.lean#L115

Sebastien Gouezel (Oct 05 2021 at 14:57):

Patrick Massot said:

And I agree it would be nice to replace the elementary versions, but clearly mathlib is going in the opposite direction (removing calculus from proofs about exponential to untangle calculus and measure theory).

Apparently this should still be possible, using the bare definition of analytic functions and of the exponential (which does not require anything on derivatives) to define the power function, prove its basic properties, and then import it into measure theory.

Patrick Massot (Oct 05 2021 at 14:59):

And we managed to put several discussions in the same thread, it looks like we're back to the gitter days...

Eric Wieser (Oct 05 2021 at 14:59):

Ah, but unlike gitter we can move messages between threads if needed :) (edit: done, hope I didn't tread on anyone's toes)

Yury G. Kudryashov (Oct 05 2021 at 15:55):

I have a proof that exp in a normed algebra does not depend on the base field (at least if the base field is a normed algebra over rat).

Anatole Dedecker (Oct 07 2021 at 19:08):

I'm a bit late to the party, but the only thing lacking for matrix exponential is a normed algebra instance on matrices (I remember searching for it and not finding it). @Yury G. Kudryashov is docs#exp_eq_exp_of_field_extension similar to what you did ?

Eric Wieser (Oct 07 2021 at 19:13):

There's a PR open that adds a norm of some kind to matrices, right?

Eric Wieser (Oct 07 2021 at 19:13):

Just not the normed_algebra instance

Yury G. Kudryashov (Oct 08 2021 at 02:28):

Why do you need the char_p assumption?

Yury G. Kudryashov (Oct 08 2021 at 02:29):

I mean, can't you say "let p be the characteristic of K" in the proof?

Yury G. Kudryashov (Oct 08 2021 at 02:29):

I assumed that both fields are normed algebras over rat.

Yury G. Kudryashov (Oct 08 2021 at 02:30):

And made no assumptions like is_scalar_tower.

Anatole Dedecker (Oct 08 2021 at 09:39):

Yury G. Kudryashov said:

I mean, can't you say "let p be the characteristic of K" in the proof?

You are right, that is just an artifact of the original version I did. I'll PR a change soon.

Anatole Dedecker (Oct 08 2021 at 09:40):

Do you think it is possible to completely hide the base field ?

Patrick Massot (Dec 14 2021 at 20:58):

This is my periodic message about the missing undergrad math list. I think there is a lot of cleanup to do. Some people have important propaganda talks to deliver in mid-January and it would be nice to have an undergrad list sprint before then. Today I created two new wiki pages: trivial targets and low hanging fruits. The border between those categories is a bit fuzzy but I think the first list could be wiped out in one week. And both lists could be handled in one month if we manage to get some community dynamics here. Feel free to edit those wiki pages to claim items. I think that anyone having access to mathlib branches can edit them. You can also post messages here of course.

Patrick Massot (Dec 14 2021 at 20:59):

Of course if you feel more ambitious, the big targets list still exists.

Heather Macbeth (Dec 14 2021 at 21:02):

@Patrick Massot Regarding the classical groups, what we have in mathlib currently is

  • matrix and endomorphism GL
  • matrix SL (we should correct your wiki which says it's missing) but not endomorphism SL
  • matrix O and U but not endomorphism O and U (they will be unlocked soon by @Frédéric Dupuis' work on the adjoint)
  • neither matrix nor endomorphism SO, SU

So the currently accessible targets are endomorphism SL and matrix SO, SU. Do you agree?

Eric Wieser (Dec 14 2021 at 21:03):

Those new pages are great @Patrick Massot!

Patrick Massot (Dec 14 2021 at 21:03):

As explained in the wiki pages, some of the "trivial targets" are simply waiting for declaration names that already exist.

Patrick Massot (Dec 14 2021 at 21:04):

And indeed some stuff already exist for classical groups. The satisfactory situation would be to have, for each case, the matrix version, the endomorphism version and a group isomorphism when a suitable basis is given.

Heather Macbeth (Dec 14 2021 at 21:06):

My point is that endomorphism O, U, SO and SU are not actually trivial targets.

Patrick Massot (Dec 14 2021 at 21:07):

What is non-trivial?

Heather Macbeth (Dec 14 2021 at 21:07):

Defining the adjoint endomorphism, that's what @Frédéric Dupuis is working on but it needs all the new work on conjugate-linear maps.

Eric Wieser (Dec 14 2021 at 21:07):

Is it worth having a dedicated zulip stream for the undergrad math list?

Patrick Massot (Dec 14 2021 at 21:09):

Oh, I thought we already had adjoints!

Yaël Dillies (Dec 14 2021 at 21:09):

Maybe not the undergrad maths list per say, but for short easy projects?

Patrick Massot (Dec 14 2021 at 21:10):

I was tricked by the existence of docs#is_self_adjoint

Heather Macbeth (Dec 14 2021 at 21:10):

We have the adjoint (=conjugate-transpose) for matrices, docs#matrix.star_ring, but not yet for endomorphisms.

Patrick Massot (Dec 14 2021 at 21:10):

But there is a loophole, you can define self-adjoint whithout adjoint.

Yaël Dillies (Dec 14 2021 at 21:11):

Note that continuity of convex functions is tackled by someone somewhere already, but I can't find it now... Maybe a branch?

Patrick Massot (Dec 14 2021 at 21:11):

Eric Wieser said:

Is it worth having a dedicated zulip stream for the undergrad math list?

Maybe. We can also create topics in the maths or general stream.

Heather Macbeth (Dec 14 2021 at 21:12):

Yaël Dillies said:

Note that continuity of convex functions is tackled by someone somewhere already, but I can't find it now... Maybe a branch?

By @Malo Jaffré maybe?

Patrick Massot (Dec 14 2021 at 21:12):

Continuity of convex functions should be a nice exercise, especially since it's in the one-variable section.

Patrick Massot (Dec 14 2021 at 21:15):

Heather, feel free to edit the wiki page with details about the status of classical groups.

Heather Macbeth (Dec 14 2021 at 21:17):

I just did, please check the diff and see if you agree.

Heather Macbeth (Dec 14 2021 at 21:18):

Couple more points: I don't think we can define and diagonalize "normal endomorphisms" until we have the adjoint. So I'd like to remove that from "trivial targets" also (it's definitely on my to-do list once we have it). OK?

Yaël Dillies (Dec 14 2021 at 21:18):

Heather Macbeth said:

Yaël Dillies said:

Note that continuity of convex functions is tackled by someone somewhere already, but I can't find it now... Maybe a branch?

By Malo Jaffré maybe?

I think so, yeah

Patrick Massot (Dec 14 2021 at 21:19):

Heather Macbeth said:

I just did, please check the diff and see if you agree.

It's fine except you modified a section header, making it more difficult to locate the item on the undergrad todo page.

Heather Macbeth (Dec 14 2021 at 21:22):

simultaneous diagonalization of two real quadratic forms, with one positive-definite: This should very easily follow from what we already have.

I think the difficulty here is in expressing "two separate real quadratic forms" -- this is related to the mess with our various definitions of bilin_form, sesq_form, inner_product_space, etc, which have been causing @Moritz so many headaches. I think it is only fair to call it a "trivial target" if you or another expert will write up a sketch in Lean for the proposed formulation.

Heather Macbeth (Dec 14 2021 at 21:25):

piecewise CkC^k functions

Wasn't there some subtlety in how to define these (so again, not a "trivial target" in the sense that a casual user could knock it off easily)? I think @Yury G. Kudryashov had an idea for how this should be done.

Patrick Massot (Dec 14 2021 at 21:28):

Feel free to move stuff from the first list to the second one (and add comments).

Heather Macbeth (Dec 14 2021 at 21:30):

Also: In a sense, we have the classification of elements of O(2,R)O(2, \mathbb{R}), since we have the classification of real-linear isometries of C\mathbb{C}. Does this count?

Heather Macbeth (Dec 14 2021 at 21:30):

docs#linear_isometry_complex

Patrick Massot (Dec 14 2021 at 21:32):

It would be nicer to deduce from this a result that is explicitly about R2\mathbb{R}^2.

Heather Macbeth (Dec 14 2021 at 21:35):

It would be nice, but I'm not sure about how to formulate it. Do you want to say that a choice of inner product and of orientation on on a real 2d vector space VV together determine an almost-complex structure, and then say that an orientation-preserving linear isometry of VV is a complex rotation for that almost-complex structure? Or do you have something more co-ordinate based in mind?

Patrick Massot (Dec 14 2021 at 21:41):

Good question. I guess the simplest way to claim that item is a coordinate version.

Joseph Myers (Dec 14 2021 at 22:10):

I expect some form of that statement about orientation-preserving linear isometries corresponding to rotations in the complex numbers to come up as part of defining oriented angles. (We have quite a lot of API for isometries in the complex numbers and for complex.arg that it seems to make sense to reuse as part of defining oriented angles rather than duplicating, provided the resulting API for oriented angles is properly proved independent of choice of basis and can be used without caring about how complex numbers might have been used in its definition. So after #10737 I'm thinking of showing that (in positive dimension) there exist a basis (and an orthonormal basis, in the inner product space case) corresponding to a given orientation, then proving whatever's needed about mapping along basis.isometry_euclidean_of_orthonormal and complex.isometry_euclidean.symm to set up oriented angles and justify the definition.)

Heather Macbeth (Dec 14 2021 at 22:11):

This seems like the principled way to do it.

Yury G. Kudryashov (Dec 14 2021 at 23:42):

About piecewise CkC^k functions. There are at least two useful notions here: an abstract property of being a CkC^k-smooth function, and a way of defining piecewise functions from some data (intervals and formulas on these intervals).

Yury G. Kudryashov (Dec 15 2021 at 00:16):

If we want to formalize approximation methods for ODEs (Euler, Runge–Kutta) as approximations to a solution on the whole interval (not a discrete set of pts), then it may be useful to have a way to define piecewise functions from some recursion formulas.

Johan Commelin (Dec 15 2021 at 06:23):

I suggest that if you make a PR that deals with item(s) on this list, we should label it with a undergrad label.

Johan Commelin (Dec 15 2021 at 06:26):

I will try to PR a definition (+ basic API) of matrix.rank later today.

Johan Commelin (Dec 15 2021 at 19:07):

#10826

Malo Jaffré (Dec 16 2021 at 09:28):

Heather Macbeth said:

Yaël Dillies said:

Note that continuity of convex functions is tackled by someone somewhere already, but I can't find it now... Maybe a branch?

By Malo Jaffré maybe?

Yes, I will try to cleanup and PR the one-dimensional version next week

Johan Commelin (Dec 18 2021 at 06:32):

I was away from home for two days. But rank of a matrix should now be done.

Johan Commelin (Dec 18 2021 at 06:33):

@Yury G. Kudryashov what is the status of matrix exponentials? Doesn't that follow from some abstract generic theory that is already done?

Yury G. Kudryashov (Dec 18 2021 at 09:36):

It does but possibly we need some glue code. @Anatole Dedecker is the right person to ask about this file.

Johan Commelin (Dec 18 2021 at 10:16):

I've started a thread about the cross product here: https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/cross.20product

Yury G. Kudryashov (Dec 18 2021 at 19:27):

Should we add definitions like these?

def has_jump_discontinuity {α β : Type*} [linear_order α] [topological_space α] [topological_space β] (f : α  β) (a : α) :=
 b c, tendsto f (𝓝[<] a) (𝓝 b)  tendsto f (𝓝[>] a) (𝓝 c)  b  c

def has_removable_discontinuity {α β : Type*} [topological-space α] [topological_space β] (f : α  β) (a : α) :=
 b  f a, tendsto f (𝓝[] a) (𝓝 b)

Yury G. Kudryashov (Dec 18 2021 at 19:28):

(I'm grading a 1st year calculus exam, my problem asks about the type of discontinuity of a function)

Yury G. Kudryashov (Dec 20 2021 at 12:49):

I've started calculus-defs in branch#YK-calculus-defs. I don't know whether we want to have it somewhere in mathlib.

Kevin Buzzard (Dec 20 2021 at 13:28):

"I've got a ton of exams to mark and am in the middle of several projects, so I started another one because I don't want to mark the exams" ;-)

Yaël Dillies (Dec 20 2021 at 13:29):

Sounds like experience, Kevin!

Johan Commelin (Dec 20 2021 at 13:41):

Johan Commelin said:

what is the status of matrix exponentials? Doesn't that follow from some abstract generic theory that is already done?

@Anatole Dedecker what do you think about :this:

Anatole Dedecker (Dec 20 2021 at 15:13):

The only missing thing is a docs#normed_algebra instance for matrices. I could work on that but I don't know which norm we want on matrices. To me there are at least two sensible possibilities :

  • the operator norm, which we could get by pulling back along linear_map.to_continuous_linear_map \comp matrix.to_lin'
  • the Hilbert-Schmidt norm, induced by the usual inner product A,B:=Tr(AB)\langle A, B\rangle := \mathrm{Tr}(A^\intercal B) (aka docs#matrix.dot_product)

Johan Commelin (Dec 20 2021 at 15:14):

So maybe we don't make it an instance, but provide two defs?

Anatole Dedecker (Dec 20 2021 at 15:15):

(Note that we have docs#matrix.normed_space as a def, but this isn't an algebra norm)

Anatole Dedecker (Dec 20 2021 at 15:25):

Johan Commelin said:

So maybe we don't make it an instance, but provide two defs?

That makes sense to me. And then I guess lemmas that are specifically about matrix exponential (there are none yet, but maybe they will come) should just have a normed_algebra assumption so you can use them with whatever norm you made a local instance of ?

Eric Wieser (Dec 20 2021 at 15:27):

Don't we already have a norm on matrices?

Eric Wieser (Dec 20 2021 at 15:27):

I thought that was PR'd a few weeks ago. Maybe docs#matrix.normed_group? nevermind, that's mentioned above

Yury G. Kudryashov (Dec 20 2021 at 15:30):

Can we have multiple defs that reuse the same topological_space (or even uniform_space) structure?

Yury G. Kudryashov (Dec 20 2021 at 15:31):

Then matrix exponent can be defined as tsum that uses pi topological space structure, and proofs can use (localized) normed_group + complete_space instances for proofs.

Yury G. Kudryashov (Dec 20 2021 at 15:31):

Kevin Buzzard said:

"I've got a ton of exams to mark and am in the middle of several projects, so I started another one because I don't want to mark the exams" ;-)

Exactly!

Eric Wieser (Dec 20 2021 at 15:32):

Are there algebras where the tsum exponential approach works but the norm exponential approach doesn't, or vice versa?

Jireh Loreaux (Dec 20 2021 at 15:33):

I was just discussing this with @Frédéric Dupuis. I think it makes sense not to impose a global instance as Johan suggested. There are lots of norms on matrices. And for example, when the entries lie in a C^*-algebra, you can even get a C^*-norm, but it's not exactly a "standard one" unless you develop the theory of Hilbert C^*-modules.

Yury G. Kudryashov (Dec 20 2021 at 15:54):

@Eric Wieser E.g., for matrices the norm approach "doesn't work" because we don't want to have a global instance.

Eric Wieser (Dec 20 2021 at 16:04):

I ask in the context of an exponential on the exterior and clifford algebras, where usually I see it used as "well the Taylor expansion obviously converges for this x I care about" without any real claim as to whether it is a total function

Tomas Skrivan (Dec 20 2021 at 16:53):

I'm not following this discussion too closely but I think some basic numerical analysis could be nice undergrad topic. ODE solvers, polynomial approximation, numerical integration, root finding etc. Once mathlib gets ported to Lean 4 I could actually use these theorem to properly formalize numerical library I'm working on.

Patrick Massot (Dec 20 2021 at 17:01):

Tomas, there is indeed some numerical analysis in the full list but I didn't put any of it in my short term targets because we currently don't have anything. So this is not part of what I would encourage people to work one, but everybody is free to work on anything.

Eric Wieser (Apr 19 2022 at 15:18):

Johan Commelin said:

Yury G. Kudryashov what is the status of matrix exponentials? Doesn't that follow from some abstract generic theory that is already done?

I've made a first pass of this in #13520, which has grown quite a dependency tree

Eric Wieser (May 05 2022 at 17:35):

30 PRs later, the branches of that tree have been pruned; it's ready for review!

Eric Wieser (May 05 2022 at 17:36):

I've left det (exp _ _ A) = exp _ _ (trace A) as an exercise for some poor undergrad to pick up

Reid Barton (May 05 2022 at 18:26):

By the way, I can kind of understand making the field argument of exp explicit (even though it seems unnecessary with an adjusted definition) but why is the algebra argument explicit? Isn't it just the type of A?

Eric Wieser (May 05 2022 at 18:28):

Yes, I agree we should remove that argument

Eric Wieser (May 06 2022 at 08:48):

Done in #13986

Eric Wieser (May 09 2022 at 06:50):

What exactly is meant by "endomorphism" in the "endomorphism exponential" entry? docs#module.End (which has no norm yet)? V →L[K] V (docs#continuous_linear_map)?

Anatole Dedecker (May 09 2022 at 07:11):

The latter I would say

Eric Wieser (May 09 2022 at 07:14):

https://github.com/leanprover-community/mathlib/wiki/Undergrad-TODO-trivial-targets#exponential suggests something about finite dimensions, making me suspect the former

Eric Wieser (May 09 2022 at 07:16):

Which would essentially just be a case of inducing a norm via docs#linear_map.continuous_of_finite_dimensional

Anatole Dedecker (May 09 2022 at 07:24):

Oh yeah maybe

Frédéric Dupuis (May 09 2022 at 15:24):

In the finite dimensional case, shouldn't it already just work, since now we don't need an actual norm, but only the right topology?

Frédéric Dupuis (May 09 2022 at 15:25):

(Or do we not have a topology either?)

Eric Wieser (May 09 2022 at 16:08):

No topology either

Eric Wieser (May 09 2022 at 16:09):

But even if we had the topology, we wouldn't be able to use docs#exp_add without the norm too

Eric Wieser (May 09 2022 at 16:10):

We also don't have the topology on continuous maps when only a topology is available on the (co)domains

Eric Wieser (May 09 2022 at 16:12):

(cc @Jason KY. who had some thoughts on discord about that)

Frédéric Dupuis (May 09 2022 at 16:13):

In that case I think we should just declare victory on that undergrad math list bullet point, because it's very likely to just stay that way.

Eric Wieser (May 09 2022 at 16:15):

I'm not sure I agree; inducing the operator norm in the way I describe above sounds fairly straightforward

Eric Wieser (May 09 2022 at 16:15):

So I think it's place on the "trivial targets" list is justified

Eric Wieser (May 09 2022 at 16:16):

A warmup task for the position in Orsay perhaps ;)

Frédéric Dupuis (May 09 2022 at 16:18):

But do we want to do this? It makes sense to say that we simply don't put a default topology on linear_map because there are too many choices, in which case it's very reasonable to say that "endomorphism exponential" refers to continuous linear maps.

Jason KY. (May 09 2022 at 16:19):

Eric Wieser said:

(cc Jason KY. who had some thoughts on discord about that)

I'll copy what I wrote on discord here (the question is how to generalize the topology on the space of bounded linear operators between normed spaces to TVS. No promise what I've written is at all correct):

Since the space of operators is also a topological vector space it suffices to give a basis of open sets at 0. I think since this basis for the topology induced by the norm is given by Bϵ(0)={T(B1)ϵB1}B_\epsilon(0) = \{T(B_1) \le \epsilon B_1\} we can do the similar for the not norm case. So since bounded is defined in general for all TVS (Yael pointed out this is the von Nuemann boundedness which we have), maybe a compatible basis at 0 is all sets of the form {T(U)V}\{T(U) \le V\} for bounded open neighborhood U,VU, V of 0 in XX and YY resp.

Eric Wieser (May 09 2022 at 16:23):

Frédéric Dupuis said:

But do we want to do this? It makes sense to say that we simply don't put a default topology on linear_map because there are too many choices, in which case it's very reasonable to say that "endomorphism exponential" refers to continuous linear maps.

Are there more choices for the topology on linear_map than there are for continuous_linear_map?

Eric Wieser (May 09 2022 at 16:23):

Jason, I'm going to extract that post and my comments to a new thread since I've probably just confused things here - but thanks for the paste (edit; done)

Frédéric Dupuis (May 09 2022 at 16:24):

In the infinite-dimensional case there's a whole bunch of them; for continuous_linear_map we've picked one.

Frédéric Dupuis (May 09 2022 at 16:25):

So I guess what you would want to do is put the operator norm on it in the finite-dimensional case, and have no topology otherwise?

Frédéric Dupuis (May 09 2022 at 16:26):

I see, yes that would make sense.

Eric Wieser (May 09 2022 at 16:27):

We already have a norm only for the finite case for docs#pi.normed_group, so I think "no instance for infinite things" is not too weird a situation

Peter Scholze (May 09 2022 at 17:36):

As an undergrad, I once started a course on functional analysis given by Jens Franke (he's famous for work in number theory, but started his career as a functional analyst). In the first lecture, he introduced the seven topologies on the dual space...

(Shameless advertisement: In condensed math, the space of linear maps between two condensed vector spaces is canonically itself a condensed vector space.)

Colleen Robles (May 13 2023 at 17:05):

I'll supervise an undergraduate project on Lean later this summer. Am I correct in understanding that we should use Lean 3 (rather than Lean 4)? And
https://leanprover-community.github.io/undergrad_todo.html
is the right place to look for potential project ideas? Anything else I should be aware of or think about?

Kevin Buzzard (May 13 2023 at 17:18):

Right now the community is in a transition period, so your question is a little difficult to answer. I would say that the big advantage of Lean 3 over Lean 4 is that there are more learning resources, and the big advantage of Lean 4 over Lean 3 is that by the end of 2023 Lean 3 will be dead as the transition becomes complete.

I would say that the undergraduate todo list is not a great place to look without some discussions with the community. The problem with that list is that it does not do a good job of explaining that some things are on that list because the community wants them done in a specific way, and it may need a Lean expert to do them. Also targetting mathlib is really complicated right now again because of the ongoing porting process. This is a temporary issue, but there is also a more long-term issue that in general students tend to want to work on projects for just one summer and then quit at a certain skill level, whereas contributing to mathlib requires what one might call "expert level code", and many students I supervise never reach expert level in the 8 or so weeks I work with them, and then when the project is over they don't go back to it. This makes contributing to mathlib almost impossible for these people.

I would say that you would be better off making a project which depends on mathlib (either 3 or 4, depending on how brave you are) and then just formalising what the heck you want, and who cares if it's in mathlib or not. I've supervised plenty of projects formalising stuff which is already in mathlib; students who don't know much about Lean when they begin will probably find that by the end of the summer many of the proofs in mathlib are still incomprehensible, but that they can also write their own proofs of things (possibly even things which are in mathlib) which are much easier to read. Mathlib is written in a rather obfuscated style, for better or worse.

Eric Wieser (May 13 2023 at 17:51):

whereas contributing to mathlib requires what one might call "expert level code", and many students I supervise never reach expert level in the 8 or so weeks I work with them, and then when the project is over they don't go back to it.

Note that this isn't necessarily an argument against _trying_ to contribute to mathlib. Sometimes these abandoned PRs contain useful results that someone else needs, and then that someone else does the cleanup the students never got around to

Matthew Ballard (May 13 2023 at 18:35):

Hi Colleen. If you want to play it safe, then Lean 3 is a good choice. But your students may naturally be pulled toward Lean 4 given the existing momentum. If using Lean 4 is an option, use of Mathlib 3 or Mathlib 4 can depend pretty strongly on the project itself and which projects are in focus. For example, most of Combinatorics has been ported (or is almost there) whereas Analysis is about 1/3 ported. You can poke around at https://leanprover-community.github.io/mathlib-port-status/ to see which files have made it into ML4 so far.


Last updated: Dec 20 2023 at 11:08 UTC