Zulip Chat Archive

Stream: general

Topic: Undergraduate math list


view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip 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: ''

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip Yury G. Kudryashov (May 12 2020 at 21:12):

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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Yury G. Kudryashov (May 13 2020 at 06:09):

Should I push or PR?

view this post on Zulip Yury G. Kudryashov (May 13 2020 at 06:15):

I'd strip the common prefix from all URLs.

view this post on Zulip 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.

view this post on Zulip Johan Commelin (May 13 2020 at 06:22):

I think the broken link detector is a must btw.

view this post on Zulip Yury G. Kudryashov (May 13 2020 at 22:23):

I fixed some URLs and translated 1.1.

view this post on Zulip 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?

view this post on Zulip 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.)

view this post on Zulip Yury G. Kudryashov (May 14 2020 at 03:59):

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

view this post on Zulip 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.

view this post on Zulip Yury G. Kudryashov (May 14 2020 at 04:03):

OK, let's have a YaML file

view this post on Zulip Yury G. Kudryashov (May 14 2020 at 04:04):

BTW, do we have an undergraduate student speaking French?

view this post on Zulip 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.

view this post on Zulip 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)

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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…)

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Ryan Lahfa (May 14 2020 at 14:07):

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

view this post on Zulip Ryan Lahfa (May 14 2020 at 14:08):

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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Patrick Massot (May 14 2020 at 14:27):

Ryan Lahfa said:

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

This is all on pages 4 and 5.

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Johan Commelin (May 14 2020 at 15:05):

I personally wouldn't worry about it too much.

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Ryan Lahfa (May 14 2020 at 15:06):

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

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip Patrick Massot (May 19 2020 at 08:37):

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

view this post on Zulip ROCKY KAMEN-RUBIO (May 19 2020 at 15:45):

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

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip Johan Commelin (May 19 2020 at 16:52):

Yup, nothing wrong with 37 small PRs!

view this post on Zulip ROCKY KAMEN-RUBIO (May 19 2020 at 18:34):

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

view this post on Zulip 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.

view this post on Zulip 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!)

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip ROCKY KAMEN-RUBIO (May 19 2020 at 18:49):

Aggregation_2020.tex

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip 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/

view this post on Zulip 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"

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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).

view this post on Zulip 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!

view this post on Zulip 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

view this post on Zulip Bryan Gin-ge Chen (May 23 2020 at 19:44):

@Kevin Buzzard has a blogpost on filters here.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip Ryan Lahfa (May 23 2020 at 20:19):

AFAIK, our comments are still there

view this post on Zulip Ryan Lahfa (May 23 2020 at 20:19):

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

view this post on Zulip 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

view this post on Zulip Patrick Massot (May 23 2020 at 20:24):

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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Ryan Lahfa (May 23 2020 at 21:46):

Appreciate it!

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Ryan Lahfa (May 23 2020 at 23:37):

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

view this post on Zulip 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:

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Johan Commelin (May 30 2020 at 05:42):

Looks good to me! Thanks for all the effort!

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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).

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip Patrick Massot (May 30 2020 at 10:44):

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

view this post on Zulip 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 -

view this post on Zulip Ryan Lahfa (May 30 2020 at 10:47):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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)

view this post on Zulip 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"

view this post on Zulip 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

view this post on Zulip Ryan Lahfa (May 30 2020 at 10:50):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Ryan Lahfa (May 30 2020 at 10:52):

Done

view this post on Zulip 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 :-)

view this post on Zulip Patrick Massot (May 30 2020 at 10:55):

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

view this post on Zulip 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)

view this post on Zulip 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.

view this post on Zulip Ryan Lahfa (May 30 2020 at 10:57):

@Patrick Massot I was definitely going to try this

view this post on Zulip Ryan Lahfa (May 30 2020 at 10:57):

I can replace the Unicode math by some LaTeX

view this post on Zulip 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

view this post on Zulip Patrick Massot (May 30 2020 at 10:58):

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

view this post on Zulip Ryan Lahfa (May 30 2020 at 10:59):

:-)

view this post on Zulip Ryan Lahfa (May 30 2020 at 10:59):

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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Ryan Lahfa (May 30 2020 at 11:01):

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

view this post on Zulip Ryan Lahfa (May 30 2020 at 11:01):

And use mathlib_docs/find/{{ decl }}

view this post on Zulip 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

view this post on Zulip 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)

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Ryan Lahfa (May 30 2020 at 11:14):

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

view this post on Zulip Ryan Lahfa (May 30 2020 at 11:14):

@Rob Lewis ^

view this post on Zulip 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

view this post on Zulip Ryan Lahfa (May 30 2020 at 11:15):

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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Rob Lewis (May 30 2020 at 11:31):

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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip Patrick Massot (May 30 2020 at 12:11):

Yes

view this post on Zulip 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?

view this post on Zulip Patrick Massot (May 30 2020 at 13:08):

Filling the links would be awesome

view this post on Zulip 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.

view this post on Zulip Johan Commelin (May 30 2020 at 13:09):

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

view this post on Zulip Johan Commelin (May 30 2020 at 13:09):

How should I interpret this file?

view this post on Zulip 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?

view this post on Zulip Johan Commelin (May 30 2020 at 13:11):

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

view this post on Zulip 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

view this post on Zulip 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)

view this post on Zulip 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...

view this post on Zulip Johan Commelin (May 30 2020 at 13:26):

Exactly

view this post on Zulip 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

view this post on Zulip Yury G. Kudryashov (May 30 2020 at 13:33):

Do we allow multiple links per item?

view this post on Zulip 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.

view this post on Zulip 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).

view this post on Zulip 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).

view this post on Zulip Johan Commelin (May 30 2020 at 13:37):

We still don't have Cayley–Hamilton

view this post on Zulip Johan Commelin (May 30 2020 at 13:37):

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

view this post on Zulip 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...).

view this post on Zulip 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.

view this post on Zulip Yury G. Kudryashov (May 30 2020 at 13:40):

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

view this post on Zulip Patrick Massot (May 30 2020 at 13:41):

Yes, I think they should be on different pages

view this post on Zulip Johan Commelin (May 30 2020 at 13:41):

Maybe just an option at the top

view this post on Zulip Johan Commelin (May 30 2020 at 13:41):

Where you can toggle what you want to see.

view this post on Zulip Johan Commelin (May 30 2020 at 13:41):

With a bit of CSS classes that should be trivial

view this post on Zulip Patrick Massot (May 30 2020 at 13:42):

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

view this post on Zulip Johan Commelin (May 30 2020 at 13:46):

That's what I'm saying, right?

view this post on Zulip Johan Commelin (May 30 2020 at 13:46):

Two radio buttons should be able to provide that.

view this post on Zulip Johan Commelin (May 30 2020 at 13:46):

Done: on/off     TODO: on/off

view this post on Zulip Patrick Massot (May 30 2020 at 13:50):

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

view this post on Zulip 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!

view this post on Zulip Ryan Lahfa (May 30 2020 at 14:08):

Johan Commelin said:

Done: on/off     TODO: on/off

Sounds good

view this post on Zulip Ryan Lahfa (May 30 2020 at 14:11):

I'm doing it now

view this post on Zulip 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?

view this post on Zulip Ryan Lahfa (May 30 2020 at 14:30):

I guess it's "alright"

view this post on Zulip Johan Commelin (May 30 2020 at 14:40):

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

view this post on Zulip Yury G. Kudryashov (May 30 2020 at 14:45):

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

view this post on Zulip Johan Commelin (May 30 2020 at 14:47):

Ooh, that's an ugly name in that case

view this post on Zulip Johan Commelin (May 30 2020 at 14:48):

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

view this post on Zulip 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].

view this post on Zulip Johan Commelin (May 30 2020 at 14:53):

What the hack is a Rupture fields:?

view this post on Zulip Kevin Buzzard (May 30 2020 at 14:54):

splitting field?

view this post on Zulip Johan Commelin (May 30 2020 at 14:54):

Nope, that's the next item

view this post on Zulip 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)

view this post on Zulip Chris Hughes (May 30 2020 at 14:55):

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

view this post on Zulip Johan Commelin (May 30 2020 at 14:55):

So we have that, right?

view this post on Zulip Chris Hughes (May 30 2020 at 14:55):

Yes

view this post on Zulip Alex J. Best (May 30 2020 at 14:55):

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

view this post on Zulip Johan Commelin (May 30 2020 at 14:56):

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

view this post on Zulip Ryan Lahfa (May 30 2020 at 14:56):

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

view this post on Zulip Ryan Lahfa (May 30 2020 at 14:56):

as a formal polynomial

view this post on Zulip Reid Barton (May 30 2020 at 14:56):

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

view this post on Zulip Ryan Lahfa (May 30 2020 at 14:56):

I was going to link it :D

view this post on Zulip Reid Barton (May 30 2020 at 14:57):

I definitely assumed this was a mistranslation

view this post on Zulip Ryan Lahfa (May 30 2020 at 14:57):

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

view this post on Zulip Johan Commelin (May 30 2020 at 14:57):

TIL

view this post on Zulip 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

view this post on Zulip Ryan Lahfa (May 30 2020 at 14:57):

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

view this post on Zulip 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)

view this post on Zulip Ryan Lahfa (May 30 2020 at 14:59):

But it does not matter

view this post on Zulip Johan Commelin (May 30 2020 at 14:59):

I've pushed those two fixes

view this post on Zulip Ryan Lahfa (May 30 2020 at 15:02):

I have the desired feature

view this post on Zulip Ryan Lahfa (May 30 2020 at 15:02):

Will push it

view this post on Zulip Johan Commelin (May 30 2020 at 15:04):

Ryan Lahfa said:

I have the desired feature

You mean the radio buttons?

view this post on Zulip Ryan Lahfa (May 30 2020 at 15:04):

Yes

view this post on Zulip Ryan Lahfa (May 30 2020 at 15:04):

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

view this post on Zulip Ryan Lahfa (May 30 2020 at 15:05):

Awesome PRs @Johan Commelin

view this post on Zulip Ryan Lahfa (May 30 2020 at 15:05):

We should try to use LaTeX for titles

view this post on Zulip Ryan Lahfa (May 30 2020 at 15:06):

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

view this post on Zulip Ryan Lahfa (May 30 2020 at 15:07):

Screen-Capture_select-area_20200530170650.png

view this post on Zulip Ryan Lahfa (May 30 2020 at 15:07):

LaTeX is working just fine

view this post on Zulip Ryan Lahfa (May 30 2020 at 15:07):

Will do a PR to add some examples

view this post on Zulip Ryan Lahfa (May 30 2020 at 15:07):

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

view this post on Zulip Ryan Lahfa (May 30 2020 at 15:07):

should we add some macros to our MathJax setup?

view this post on Zulip Johan Commelin (May 30 2020 at 15:07):

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

view this post on Zulip Ryan Lahfa (May 30 2020 at 15:08):

Alright, I'll do it

view this post on Zulip Ryan Lahfa (May 30 2020 at 15:08):

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

view this post on Zulip Johan Commelin (May 30 2020 at 15:08):

Je ne sais pas

view this post on Zulip 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

view this post on Zulip Ryan Lahfa (May 30 2020 at 15:08):

:D

view this post on Zulip Ryan Lahfa (May 30 2020 at 15:12):

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

view this post on Zulip 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?

view this post on Zulip Ryan Lahfa (May 30 2020 at 15:20):

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

view this post on Zulip 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

view this post on Zulip Patrick Massot (May 30 2020 at 15:21):

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

view this post on Zulip Ryan Lahfa (May 30 2020 at 15:21):

39 implements the LaTeX macros in _base

view this post on Zulip Ryan Lahfa (May 30 2020 at 15:21):

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

view this post on Zulip Ryan Lahfa (May 30 2020 at 15:22):

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

view this post on Zulip Johan Commelin (May 30 2020 at 15:22):

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

view this post on Zulip Johan Commelin (May 30 2020 at 15:23):

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

view this post on Zulip Ryan Lahfa (May 30 2020 at 15:23):

I do mathrm{GL}, etc. for them

view this post on Zulip Ryan Lahfa (May 30 2020 at 15:23):

You can see it in 39

view this post on Zulip 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.

view this post on Zulip Ryan Lahfa (May 30 2020 at 15:23):

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

view this post on Zulip Patrick Massot (May 30 2020 at 15:23):

Are those 3 PRs compatible?

view this post on Zulip Ryan Lahfa (May 30 2020 at 15:23):

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

view this post on Zulip Ryan Lahfa (May 30 2020 at 15:23):

@Patrick Massot Please merge Johan's ones first

view this post on Zulip Ryan Lahfa (May 30 2020 at 15:24):

Then I'll do the rebase magic for whatever happens

view this post on Zulip Ryan Lahfa (May 30 2020 at 15:24):

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

view this post on Zulip Ryan Lahfa (May 30 2020 at 15:25):

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

view this post on Zulip Johan Commelin (May 30 2020 at 15:25):

@Patrick Massot One second

view this post on Zulip Johan Commelin (May 30 2020 at 15:25):

Ryan spotted an issue in my PR

view this post on Zulip Ryan Lahfa (May 30 2020 at 15:25):

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

view this post on Zulip Ryan Lahfa (May 30 2020 at 15:26):

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

view this post on Zulip Johan Commelin (May 30 2020 at 15:27):

@Patrick Massot Ok, you can merge now

view this post on Zulip Patrick Massot (May 30 2020 at 15:27):

I reviewed Johan's PR

view this post on Zulip Patrick Massot (May 30 2020 at 15:28):

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

view this post on Zulip Ryan Lahfa (May 30 2020 at 15:28):

Nevermind my comments

view this post on Zulip Ryan Lahfa (May 30 2020 at 15:28):

Yes, I think we can merge it

view this post on Zulip Johan Commelin (May 30 2020 at 15:28):

Also, I need to go now

view this post on Zulip Patrick Massot (May 30 2020 at 15:30):

Thanks Johan, I merged it.

view this post on Zulip Ryan Lahfa (May 30 2020 at 15:30):

Fixing the conflicts

view this post on Zulip Ryan Lahfa (May 30 2020 at 15:33):

Conflicts resolved, @Patrick Massot

view this post on Zulip Ryan Lahfa (May 30 2020 at 15:35):

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

view this post on Zulip Patrick Massot (May 30 2020 at 15:38):

Great!

view this post on Zulip Ryan Lahfa (May 30 2020 at 15:38):

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

view this post on Zulip Patrick Massot (May 30 2020 at 15:38):

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

view this post on Zulip Ryan Lahfa (May 30 2020 at 15:38):

I'll fix the macro one

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip 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".

view this post on Zulip Ryan Lahfa (May 30 2020 at 15:40):

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

view this post on Zulip Ryan Lahfa (May 30 2020 at 15:41):

@Patrick Massot conflicts resolved on the latex one

view this post on Zulip 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

view this post on Zulip Patrick Massot (May 30 2020 at 15:44):

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

view this post on Zulip Patrick Massot (May 30 2020 at 15:44):

Does it work on your end?

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Patrick Massot (May 30 2020 at 15:46):

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

view this post on Zulip Ryan Lahfa (May 30 2020 at 15:47):

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

view this post on Zulip 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...

view this post on Zulip Ryan Lahfa (May 30 2020 at 15:48):

I see

view this post on Zulip Ryan Lahfa (May 30 2020 at 15:49):

I'm doing it

view this post on Zulip Ryan Lahfa (May 30 2020 at 15:49):

I should have the prototype in minutes

view this post on Zulip Patrick Massot (May 30 2020 at 15:49):

Thank you very much

view this post on Zulip Ryan Lahfa (May 30 2020 at 15:50):

@Patrick Massot Just a quick question

view this post on Zulip Patrick Massot (May 30 2020 at 15:50):

Yes?

view this post on Zulip Ryan Lahfa (May 30 2020 at 15:50):

What do you do about

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

view this post on Zulip Ryan Lahfa (May 30 2020 at 15:51):

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

view this post on Zulip 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.

view this post on Zulip Ryan Lahfa (May 30 2020 at 15:52):

Agreed

view this post on Zulip Patrick Massot (May 30 2020 at 15:52):

Do you have a specific example?

view this post on Zulip Ryan Lahfa (May 30 2020 at 15:52):

Take linear algebra

view this post on Zulip 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: ''

view this post on Zulip Ryan Lahfa (May 30 2020 at 15:53):

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

view this post on Zulip 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

view this post on Zulip 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).

view this post on Zulip 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

view this post on Zulip Patrick Massot (May 30 2020 at 15:56):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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"

view this post on Zulip Patrick Massot (May 30 2020 at 15:57):

I don't think this is a big issue

view this post on Zulip Ryan Lahfa (May 30 2020 at 15:58):

Okay

view this post on Zulip 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

view this post on Zulip Ryan Lahfa (May 30 2020 at 15:59):

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

view this post on Zulip Ryan Lahfa (May 30 2020 at 15:59):

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

view this post on Zulip Ryan Lahfa (May 30 2020 at 15:59):

Here's a prototype

view this post on Zulip Ryan Lahfa (May 30 2020 at 16:00):

Do you want I do something before I commit this?

view this post on Zulip 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

view this post on Zulip Ryan Lahfa (May 30 2020 at 16:02):

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

view this post on Zulip Ryan Lahfa (May 30 2020 at 16:02):

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

view this post on Zulip 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

view this post on Zulip Ryan Lahfa (May 30 2020 at 16:04):

we can reduce padding in the inner cards I guess

view this post on Zulip Patrick Massot (May 30 2020 at 16:08):

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

view this post on Zulip 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

view this post on Zulip Ryan Lahfa (May 30 2020 at 16:12):

Okay for bg color

view this post on Zulip 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

view this post on Zulip Ryan Lahfa (May 30 2020 at 16:13):

Should have something in 10 minutes hopefully

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Patrick Massot (May 30 2020 at 16:18):

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

view this post on Zulip Ryan Lahfa (May 30 2020 at 16:19):

Why?

view this post on Zulip 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

view this post on Zulip Patrick Massot (May 30 2020 at 16:19):

Those are busy people

view this post on Zulip Ryan Lahfa (May 30 2020 at 16:19):

You're right

view this post on Zulip Ryan Lahfa (May 30 2020 at 16:21):

Apologies

view this post on Zulip Patrick Massot (May 30 2020 at 16:23):

Don't worry

view this post on Zulip Ryan Lahfa (May 30 2020 at 16:24):

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

view this post on Zulip Ryan Lahfa (May 30 2020 at 16:24):

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

view this post on Zulip Kevin Buzzard (May 30 2020 at 16:24):

Did somebody call?

view this post on Zulip Kevin Buzzard (May 30 2020 at 16:25):

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

view this post on Zulip Kevin Buzzard (May 30 2020 at 16:25):

Only 80 algebraic geometry questions to go :D

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Ryan Lahfa (May 30 2020 at 16:27):

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

view this post on Zulip Ryan Lahfa (May 30 2020 at 16:28):

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

view this post on Zulip 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)

view this post on Zulip Ryan Lahfa (May 30 2020 at 16:28):

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

view this post on Zulip Ryan Lahfa (May 30 2020 at 16:28):

@Patrick Massot YAML stuff most likely

view this post on Zulip Ryan Lahfa (May 30 2020 at 16:29):

Can fix it in a future PR

view this post on Zulip 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.

view this post on Zulip Patrick Massot (May 30 2020 at 16:31):

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

view this post on Zulip Patrick Massot (May 30 2020 at 16:31):

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

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip Patrick Massot (May 30 2020 at 16:32):

yes, please

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Ryan Lahfa (May 30 2020 at 16:32):

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

view this post on Zulip Patrick Massot (May 30 2020 at 16:32):

when I click on them it zooms

view this post on Zulip Ryan Lahfa (May 30 2020 at 16:32):

Let me just get the latest changes you want

view this post on Zulip Patrick Massot (May 30 2020 at 16:32):

Did you fixed the two defaults?

view this post on Zulip Patrick Massot (May 30 2020 at 16:32):

Yes, let's do that

view this post on Zulip Ryan Lahfa (May 30 2020 at 16:33):

I'm doing it, only one left

view this post on Zulip 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

view this post on Zulip Mario Carneiro (May 30 2020 at 16:34):

zulip's implementation really needs work

view this post on Zulip Patrick Massot (May 30 2020 at 16:34):

Mario, you should hold on for 5 minutes

view this post on Zulip Ryan Lahfa (May 30 2020 at 16:34):

Just open the link in the browser

view this post on Zulip Mario Carneiro (May 30 2020 at 16:35):

what is being reviewed?

view this post on Zulip Mario Carneiro (May 30 2020 at 16:35):

the margins?

view this post on Zulip Ryan Lahfa (May 30 2020 at 16:35):

@Mario Carneiro the looks mostly

view this post on Zulip Mario Carneiro (May 30 2020 at 16:35):

the spacing is all over the place

view this post on Zulip 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

view this post on Zulip Ryan Lahfa (May 30 2020 at 16:36):

here we go for the defaults

view this post on Zulip Mario Carneiro (May 30 2020 at 16:36):

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

view this post on Zulip Ryan Lahfa (May 30 2020 at 16:37):

+1 @ spacing pre/post cards

view this post on Zulip Ryan Lahfa (May 30 2020 at 16:37):

the indentation "spacing" is by default

view this post on Zulip Mario Carneiro (May 30 2020 at 16:37):

What's wrong with a simple bullet list?

view this post on Zulip Ryan Lahfa (May 30 2020 at 16:37):

it's not an accordion (?)

view this post on Zulip Ryan Lahfa (May 30 2020 at 16:37):

you can fold/unfold those cards

view this post on Zulip 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)

view this post on Zulip Mario Carneiro (May 30 2020 at 16:38):

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

view this post on Zulip 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

view this post on Zulip Mario Carneiro (May 30 2020 at 16:38):

I would have just chucked some markdown on a page

view this post on Zulip Patrick Massot (May 30 2020 at 16:38):

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

view this post on Zulip Ryan Lahfa (May 30 2020 at 16:38):

@Patrick Massot I can take a look why

view this post on Zulip Ryan Lahfa (May 30 2020 at 16:38):

It might be a class missing

view this post on Zulip Mario Carneiro (May 30 2020 at 16:39):

I've seen mile long bullet lists before

view this post on Zulip Patrick Massot (May 30 2020 at 16:39):

Mario didn't need CSS in metamath...

view this post on Zulip Ryan Lahfa (May 30 2020 at 16:39):

Screen-Capture_select-area_20200530183933.png

view this post on Zulip Ryan Lahfa (May 30 2020 at 16:39):

that was it

view this post on Zulip Ryan Lahfa (May 30 2020 at 16:39):

but it broke the toggle button

view this post on Zulip 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)

view this post on Zulip 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

view this post on Zulip Ryan Lahfa (May 30 2020 at 16:42):

@Patrick Massot I pushed the fix for accordions

view this post on Zulip Ryan Lahfa (May 30 2020 at 16:42):

The thing now is that due to this kind of styling

view this post on Zulip 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"

view this post on Zulip Ryan Lahfa (May 30 2020 at 16:43):

I'm not sure I see easy workarounds

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip Ryan Lahfa (May 30 2020 at 16:45):

:tada:

view this post on Zulip 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.

view this post on Zulip Patrick Massot (May 30 2020 at 16:46):

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

view this post on Zulip Patrick Massot (May 30 2020 at 16:47):

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

view this post on Zulip Ryan Lahfa (May 30 2020 at 16:47):

this bottomless stuff is making me crazy

view this post on Zulip Ryan Lahfa (May 30 2020 at 16:47):

Oops @Patrick Massot

view this post on Zulip Ryan Lahfa (May 30 2020 at 16:47):

I'll fix it…

view this post on Zulip Patrick Massot (May 30 2020 at 16:47):

No

view this post on Zulip Patrick Massot (May 30 2020 at 16:47):

Don't fix it

view this post on Zulip Patrick Massot (May 30 2020 at 16:47):

It's not ready for links

view this post on Zulip Kevin Buzzard (May 30 2020 at 16:47):

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

view this post on Zulip Patrick Massot (May 30 2020 at 16:48):

I very carefully checked there was no link to it

view this post on Zulip Kevin Buzzard (May 30 2020 at 16:48):

Why does Fields have fields as a subthing?

view this post on Zulip Patrick Massot (May 30 2020 at 16:48):

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

view this post on Zulip Ryan Lahfa (May 30 2020 at 16:48):

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

view this post on Zulip Kevin Buzzard (May 30 2020 at 16:48):

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

view this post on Zulip Ryan Lahfa (May 30 2020 at 16:48):

@Kevin Buzzard It means both currently

view this post on Zulip Patrick Massot (May 30 2020 at 16:48):

It currently means either of these

view this post on Zulip Patrick Massot (May 30 2020 at 16:49):

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

view this post on Zulip Ryan Lahfa (May 30 2020 at 16:49):

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

view this post on Zulip Kevin Buzzard (May 30 2020 at 16:49):

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

view this post on Zulip Ryan Lahfa (May 30 2020 at 16:49):

It'll fix the mathlib links

view this post on Zulip Ryan Lahfa (May 30 2020 at 16:49):

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

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (May 30 2020 at 16:50):

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

view this post on Zulip Kevin Buzzard (May 30 2020 at 16:50):

Yeah but I need to go

view this post on Zulip Patrick Massot (May 30 2020 at 16:50):

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

view this post on Zulip Johan Commelin (May 30 2020 at 16:50):

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

view this post on Zulip Ryan Lahfa (May 30 2020 at 16:51):

Unfortunately

view this post on Zulip Ryan Lahfa (May 30 2020 at 16:51):

When the next element is hidden

view this post on Zulip Ryan Lahfa (May 30 2020 at 16:51):

I don't do adjustements to make the comma disappear

view this post on Zulip Kevin Buzzard (May 30 2020 at 16:51):

\"Usual\" functions in single variable real analysis

view this post on Zulip Johan Commelin (May 30 2020 at 16:51):

Ok

view this post on Zulip Patrick Massot (May 30 2020 at 16:51):

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

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (May 30 2020 at 16:52):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Johan Commelin (May 30 2020 at 16:52):

We could add "Expand all / Collapse all"

view this post on Zulip Ryan Lahfa (May 30 2020 at 16:52):

Johan Commelin said:

We could add "Expand all / Collapse all"

That's easy to do

view this post on Zulip 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...

view this post on Zulip Ryan Lahfa (May 30 2020 at 16:53):

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

view this post on Zulip 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 !

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip Johan Commelin (May 30 2020 at 16:53):

I think that eventually the two lists should be merged

view this post on Zulip Johan Commelin (May 30 2020 at 16:54):

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

view this post on Zulip Ryan Lahfa (May 30 2020 at 16:54):

Definitely possible

view this post on Zulip 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

view this post on Zulip Ryan Lahfa (May 30 2020 at 16:56):

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

view this post on Zulip Ryan Lahfa (May 30 2020 at 16:57):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (May 30 2020 at 16:57):

or on Cambridge's curriculum or whatever

view this post on Zulip 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

view this post on Zulip Patrick Massot (May 30 2020 at 16:57):

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

view this post on Zulip Ryan Lahfa (May 30 2020 at 16:57):

But it's French

view this post on Zulip 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]

view this post on Zulip Ryan Lahfa (May 30 2020 at 16:58):

Jordan is 9.13

view this post on Zulip 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.

view this post on Zulip Ryan Lahfa (May 30 2020 at 16:58):

we have it Screen-Capture_select-area_20200530185822.png

view this post on Zulip 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

view this post on Zulip Patrick Massot (May 30 2020 at 16:59):

No Johan, the next step is to finish the first pass on the yaml linkifying

view this post on Zulip Ryan Lahfa (May 30 2020 at 16:59):

:DDDDDD

view this post on Zulip Johan Commelin (May 30 2020 at 16:59):

Ok, sure. I meant the next next step

view this post on Zulip Johan Commelin (May 30 2020 at 16:59):

Like, after your IAS talk

view this post on Zulip Patrick Massot (May 30 2020 at 17:01):

Ok, I'll have a go at Section 6: Single variable real analysis.

view this post on Zulip 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.

view this post on Zulip Patrick Massot (May 30 2020 at 17:07):

Oh crap, the very first item I picked is hard. Topology on R...

view this post on Zulip Patrick Massot (May 30 2020 at 17:07):

R gets its topology as a uniform space

view this post on Zulip Yury G. Kudryashov (May 30 2020 at 17:11):

Metric space?

view this post on Zulip Patrick Massot (May 30 2020 at 17:12):

Yes

view this post on Zulip Patrick Massot (May 30 2020 at 17:12):

I linked to real.metric_space

view this post on Zulip Patrick Massot (May 30 2020 at 17:14):

Oh we still have underlined links in the API docs :sad:

view this post on Zulip 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

view this post on Zulip 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:

view this post on Zulip Patrick Massot (May 30 2020 at 17:20):

I think he's having dinner.

view this post on Zulip Patrick Massot (May 30 2020 at 17:20):

But I don't understand how a young nerd can have dinner away from his keyboard.

view this post on Zulip 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!

view this post on Zulip 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

view this post on Zulip Ryan Lahfa (May 30 2020 at 17:22):

I can try to move it forward today

view this post on Zulip Ryan Lahfa (May 30 2020 at 17:26):

By curiosity, do we even have distributions in Lean?

view this post on Zulip Patrick Massot (May 30 2020 at 17:29):

Distributions in the sense of Schwartz?

view this post on Zulip Patrick Massot (May 30 2020 at 17:30):

We don't.

view this post on Zulip 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

view this post on Zulip Yury G. Kudryashov (May 30 2020 at 17:33):

We don't. We have is_preconnected_iff_forall_Icc_subset and is_preconnected_I??.

view this post on Zulip Yury G. Kudryashov (May 30 2020 at 17:35):

How would you formulate real.is_(pre)connected_iff to make it useful?

view this post on Zulip Patrick Massot (May 30 2020 at 17:38):

I think we could at least say connected iff convex

view this post on Zulip 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?

view this post on Zulip Patrick Massot (May 30 2020 at 17:40):

It's dinner time. See you later

view this post on Zulip Yury G. Kudryashov (May 30 2020 at 17:42):

has_sum uses tendsto (λ n, ∑ i in range n, a i) at_top (nhds s).

view this post on Zulip 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)

view this post on Zulip Patrick Massot (May 30 2020 at 17:58):

There are two different has_sum then

view this post on Zulip Patrick Massot (May 30 2020 at 17:58):

Where is yours?

view this post on Zulip 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.

view this post on Zulip Yury G. Kudryashov (May 30 2020 at 18:00):

I should read my messages before sending them.

view this post on Zulip 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

view this post on Zulip Patrick Massot (May 30 2020 at 18:02):

But we still miss a def here

view this post on Zulip Paul van Wamelen (May 30 2020 at 18:28):

How do I help edit this on github? (without submitting a PR from a fork?)

view this post on Zulip Patrick Massot (May 30 2020 at 18:35):

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

view this post on Zulip Patrick Massot (May 30 2020 at 18:36):

Do you see the little pen button on the top-right corner?

view this post on Zulip 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)

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip 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"

view this post on Zulip Patrick Massot (May 30 2020 at 18:46):

Sorry I misunderstood. Technically it does create a fork, but nothing happens on your hard-drive.

view this post on Zulip 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

view this post on Zulip Patrick Massot (May 30 2020 at 18:47):

Fixes to the English and styling are welcome of course

view this post on Zulip Paul van Wamelen (May 30 2020 at 18:54):

Did a VERY small PR just to see how it works...

view this post on Zulip Patrick Massot (May 30 2020 at 19:02):

Merged!

view this post on Zulip 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.

view this post on Zulip 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).

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip Patrick Massot (May 30 2020 at 19:41):

I mean I would fill this item with a version of this lemma involving converging series

view this post on Zulip 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.

view this post on Zulip 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)

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Patrick Massot (May 30 2020 at 19:54):

Sure, we can use this link, but the question of converging series still stansd

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip Patrick Massot (May 30 2020 at 20:03):

Does anyone know the English translation of "Réduction des endomorphismes"?

view this post on Zulip Johan Commelin (May 30 2020 at 20:04):

Context? Analysis?

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip Patrick Massot (May 30 2020 at 20:09):

The yaml file calls it a cancelling polynomial but it sounds fishy to me

view this post on Zulip Bryan Gin-ge Chen (May 30 2020 at 20:10):

I learned it as the characteristic polynomial.

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip Patrick Massot (May 30 2020 at 20:12):

Yes any polynomial

view this post on Zulip Bryan Gin-ge Chen (May 30 2020 at 20:13):

Right, I misread. I agree with Alex.

view this post on Zulip 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.

view this post on Zulip Patrick Massot (May 30 2020 at 20:14):

What about "Réduction des endomorphismes"?

view this post on Zulip Patrick Massot (May 30 2020 at 20:14):

Does anyone has a translation?

view this post on Zulip 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: ''

view this post on Zulip Bryan Gin-ge Chen (May 30 2020 at 20:15):

Patrick Massot said:

What about "Réduction des endomorphismes"?

Finite-dimensional spectral theory?

view this post on Zulip Patrick Massot (May 30 2020 at 20:15):

By the way, the translation "kernel lemma" also sounds fishy

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip Patrick Massot (May 30 2020 at 20:16):

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

view this post on Zulip Johan Commelin (May 30 2020 at 20:17):

Nope... the only other place on earth where such a lemma exists is in Catalan...

view this post on Zulip Patrick Massot (May 30 2020 at 20:17):

annihilating polynomial is the direct translation of the French name, I like it

view this post on Zulip Patrick Massot (May 30 2020 at 20:17):

Seriously, Johan, didn't you study linear algebra?

view this post on Zulip Johan Commelin (May 30 2020 at 20:18):

Not really... actually. I skipped all the lectures.

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip Johan Commelin (May 30 2020 at 20:25):

I wouldn't know the axioms... mul_assoc? But not has_one?

view this post on Zulip Patrick Massot (May 30 2020 at 20:26):

https://en.wikipedia.org/wiki/Ring_(mathematics)#Multiplicative_identity:_mandatory_vs._optional

view this post on Zulip Johan Commelin (May 30 2020 at 20:26):

I guess the answer to your question is no.

view this post on Zulip Paul van Wamelen (May 30 2020 at 20:27):

I submitted another PR

view this post on Zulip Johan Commelin (May 30 2020 at 20:28):

We have noncommutative rings in mathlib... isn't that good enough?

view this post on Zulip Patrick Massot (May 30 2020 at 20:29):

Crap, this PR is super conflicting what I was doing

view this post on Zulip Paul van Wamelen (May 30 2020 at 20:31):

I can try and "hand merge" it... Gimme a sec.

view this post on Zulip 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.

view this post on Zulip Patrick Massot (May 30 2020 at 20:32):

Let's do both actually: I'll my merge my PR and you'll fix yours

view this post on Zulip Patrick Massot (May 30 2020 at 20:33):

And then I'll fix conflicts with my local changes

view this post on Zulip Patrick Massot (May 30 2020 at 20:33):

Done. Now you have conflicts

view this post on Zulip 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)

view this post on Zulip Patrick Massot (May 30 2020 at 20:40):

And how do you say "réduction des endomorphismes"?

view this post on Zulip Reid Barton (May 30 2020 at 20:41):

Is this "structure theory of endomorphisms"?

view this post on Zulip Reid Barton (May 30 2020 at 20:41):

I guess that's kind of a mixed metaphor

view this post on Zulip Paul van Wamelen (May 30 2020 at 20:45):

I think I cleared the conflicts

view this post on Zulip Patrick Massot (May 30 2020 at 20:47):

Awesome.

view this post on Zulip 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

view this post on Zulip Ryan Lahfa (May 30 2020 at 20:54):

Hahahaha, this thread has really turned into how does you say X in english :'D

view this post on Zulip Kenny Lau (May 30 2020 at 20:55):

what a surprise, a second language is not just the first language plus a dictionary

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Ryan Lahfa (May 30 2020 at 21:02):

And same goes for many terms I guess

view this post on Zulip 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!

view this post on Zulip 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"

view this post on Zulip Ryan Lahfa (May 30 2020 at 21:15):

Anyway, I'm getting sidetracked… :D

view this post on Zulip Kevin Buzzard (May 30 2020 at 21:26):

Hecke algebras are something which will be within reach soon, and they're rings without 1

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip Johan Commelin (Jun 01 2020 at 09:06):

#7 is on single variable complex analysis, and it's going to make us look ridiculous...

view this post on Zulip Johan Commelin (Jun 01 2020 at 09:08):

I'll start on #8. Topology now.

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip Johan Commelin (Jun 01 2020 at 09:16):

Aha, makes sense

view this post on Zulip 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.

view this post on Zulip Patrick Massot (Jun 01 2020 at 09:18):

Don't we have at least the definition of a probability measure?

view this post on Zulip Johan Commelin (Jun 01 2020 at 09:19):

pmf ­– Probability mass function

view this post on Zulip Johan Commelin (Jun 01 2020 at 09:19):

But otherwise, not much, I think

view this post on Zulip 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.

view this post on Zulip Patrick Massot (Jun 01 2020 at 09:24):

Don't hesitate to reorder and slightly reword stuff if it makes more sense.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Oliver Nash (Jun 01 2020 at 09:25):

Understood, I will stick to a three-level structure.

view this post on Zulip Johan Commelin (Jun 01 2020 at 09:26):

Thanks for helping!

view this post on Zulip Oliver Nash (Jun 01 2020 at 09:26):

My pleasure!

view this post on Zulip 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:)

view this post on Zulip Johan Commelin (Jun 01 2020 at 09:35):

Note: affine spaces have been merged

view this post on Zulip 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

view this post on Zulip Patrick Massot (Jun 01 2020 at 09:38):

Each time I type leanproject up in mathlib, elan downloads something... :grinning:

view this post on Zulip 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?

view this post on Zulip Patrick Massot (Jun 01 2020 at 10:15):

I've updated the metric topology section.

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (Jun 01 2020 at 10:25):

https://github.com/LAC1213/compact_unit_ball

view this post on Zulip 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...

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Patrick Massot (Jun 01 2020 at 10:35):

Of course turning this into something PRable means work.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip David Wärn (Jun 01 2020 at 10:57):

Shouldn't this argument be phrased using docs#riesz_lemma ?

view this post on Zulip Patrick Massot (Jun 01 2020 at 11:09):

Indeed it looks like someone started this road but gave up.

view this post on Zulip Patrick Massot (Jun 01 2020 at 11:10):

It seems to be Jean. @Jean Lo what is the status of this?

view this post on Zulip 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).

view this post on Zulip Johan Commelin (Jun 01 2020 at 11:58):

@Joseph Myers Sure... but all small bits help.

view this post on Zulip 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?

view this post on Zulip Johan Commelin (Jun 01 2020 at 12:25):

Is "C is algebraically closed" somewhere on the agreg list?

view this post on Zulip Patrick Massot (Jun 01 2020 at 13:52):

I hope so

view this post on Zulip Patrick Massot (Jun 01 2020 at 13:53):

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

view this post on Zulip 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).

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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...

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip 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…

view this post on Zulip Yury G. Kudryashov (Jun 01 2020 at 15:29):

English Wikipedia never mentions this name, just "Fundamental theorem of algebra"

view this post on Zulip Ryan Lahfa (Jun 01 2020 at 15:30):

That's an invitation to change the name into "fundamental theorem of algebra" I believe

view this post on Zulip Yury G. Kudryashov (Jun 01 2020 at 16:08):

https://github.com/leanprover-community/leanprover-community.github.io/commit/bebb1e9cafaee64414639bc9714f09d9b124ca0f

view this post on Zulip 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".

view this post on Zulip Kevin Buzzard (Jun 01 2020 at 16:27):

It's because algebra := polynomials and matrices in 1800 or something, right?

view this post on Zulip 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?

view this post on Zulip 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:

view this post on Zulip Patrick Massot (Jun 01 2020 at 17:55):

The title could be "C\mathbb C is algebraically closed"...

view this post on Zulip Johan Commelin (Jun 01 2020 at 17:56):

Such a boring theorem name... you've been influenced too much by mathlib naming conventions.

view this post on Zulip Patrick Massot (Jun 01 2020 at 17:58):

I can see you don't know what this theorem is called in mathlib...

view this post on Zulip Johan Commelin (Jun 01 2020 at 17:58):

polynomial.complex_exists_root?

view this post on Zulip Johan Commelin (Jun 01 2020 at 17:58):

That's just because we don't have class algebraically_closed (K : Type*) [field K] yet.

view this post on Zulip Johan Commelin (Jun 01 2020 at 17:59):

Otherwise it would be complex.algebraically_closed.

view this post on Zulip 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.

view this post on Zulip Yury G. Kudryashov (Jun 01 2020 at 21:33):

E.g., from #2907

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Yury G. Kudryashov (Jun 02 2020 at 05:05):

Probably we should stop hijacking Patrick's thread.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Johan Commelin (Jun 02 2020 at 08:54):

Otherwise our todo-list is much too optimistic.

view this post on Zulip 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...

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Ryan Lahfa (Jun 02 2020 at 09:21):

I'll look into it

view this post on Zulip Johan Commelin (Jun 02 2020 at 09:21):

Thanks!

view this post on Zulip Johan Commelin (Jun 02 2020 at 09:21):

Alternative: strip out the classes and generate two files...

view this post on Zulip 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

view this post on Zulip Ryan Lahfa (Jun 02 2020 at 09:22):

Hahahaha

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip 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?

view this post on Zulip Johan Commelin (Jun 02 2020 at 09:48):

Internal direct sum = sup in the lattice semimodule _ _??

view this post on Zulip Kevin Buzzard (Jun 02 2020 at 09:48):

It's no different to internal sum though

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Johan Commelin (Jun 02 2020 at 09:51):

We just totalise the function...

view this post on Zulip Johan Commelin (Jun 02 2020 at 09:51):

And define it for non-othogonal submodules as well

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (Jun 02 2020 at 10:16):

https://github.com/leanprover-community/leanprover-community.github.io/pull/50 bilinear and quadratic forms

view this post on Zulip Patrick Massot (Jun 02 2020 at 10:18):

Merged!

view this post on Zulip Patrick Massot (Jun 02 2020 at 10:18):

But I'll probably need to fix structure

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Jun 02 2020 at 10:19):

And I didn't know how to check if the links work.

view this post on Zulip Kevin Buzzard (Jun 02 2020 at 10:19):

(e.g. I might have missed a namespace)

view this post on Zulip 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.

view this post on Zulip Patrick Massot (Jun 02 2020 at 10:22):

Hold on for two minutes

view this post on Zulip 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

view this post on Zulip Patrick Massot (Jun 02 2020 at 10:27):

That's what I call "fixing structure", following the guidelines quoted above.

view this post on Zulip Kevin Buzzard (Jun 02 2020 at 10:27):

I see, so actually changing the structure of the yaml to be a bit more sane

view this post on Zulip Kevin Buzzard (Jun 02 2020 at 10:28):

keep precisely the same leaves but we can move them around a bit

view this post on Zulip Patrick Massot (Jun 02 2020 at 10:28):

Yes. Actually I'm pretty disappointed by the source document. I thought it was more structured.

view this post on Zulip Kevin Buzzard (Jun 02 2020 at 10:28):

it probably wasn't written by a computer scientist!

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip Patrick Massot (Jun 02 2020 at 10:29):

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

view this post on Zulip Patrick Massot (Jun 02 2020 at 10:29):

Oh, the preceding line is a wrong translation

view this post on Zulip Patrick Massot (Jun 02 2020 at 10:30):

"vector product" means cross product

view this post on Zulip Johan Commelin (Jun 02 2020 at 10:30):

I'm learning new stuff everyday...

view this post on Zulip Patrick Massot (Jun 02 2020 at 10:30):

But we call it "produit vectoriel" in French.

view this post on Zulip 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)

view this post on Zulip Patrick Massot (Jun 02 2020 at 10:30):

The triple product thins is about computing determinants using the Euclidean structure

view this post on Zulip Kevin Buzzard (Jun 02 2020 at 10:30):

3 is overrated

view this post on Zulip Patrick Massot (Jun 02 2020 at 10:31):

That's why I named this section "low dimensions"

view this post on Zulip Kevin Buzzard (Jun 02 2020 at 10:31):

why not just call it n-ary product and link to det :-)

view this post on Zulip Patrick Massot (Jun 02 2020 at 10:31):

The fact that you can compute determinants using the Euclidean structure has some content

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Patrick Massot (Jun 02 2020 at 10:51):

I thought physics was all about dimension 4.

view this post on Zulip Kevin Buzzard (Jun 02 2020 at 10:55):

I thought 10?

view this post on Zulip Ryan Lahfa (Jun 02 2020 at 11:07):

Sometimes they forget about time and wrapped dimensions, :-°

view this post on Zulip 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.

view this post on Zulip Yury G. Kudryashov (Jun 02 2020 at 13:16):

https://leanprover-community.github.io/mathlib_docs/analysis/ODE/gronwall.html

view this post on Zulip Johan Commelin (Jun 02 2020 at 13:17):

Aah, I made a typo...

view this post on Zulip Johan Commelin (Jun 02 2020 at 13:18):

Thanks!

view this post on Zulip Johan Commelin (Jun 02 2020 at 13:21):

We don't really have a definition of a sigma algebra :expressionless:

view this post on Zulip Yury G. Kudryashov (Jun 02 2020 at 13:22):

We have [measurable α]

view this post on Zulip Johan Commelin (Jun 02 2020 at 13:24):

Yup... it's just that the name isn't recognisable

view this post on Zulip 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.

view this post on Zulip Sebastien Gouezel (Jun 02 2020 at 13:35):

A sigma algebra is exactly an instance of measurable_space α

view this post on Zulip Johan Commelin (Jun 02 2020 at 13:40):

It's just that the list has 'measureable spaces' and 'sigma algebras' as seperate items :expressionless:

view this post on Zulip 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:

view this post on Zulip Gabriel Ebner (Jun 02 2020 at 13:43):

What is the difference between a measurable space and a set with a sigma algebra?

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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".

view this post on Zulip 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...

view this post on Zulip Sebastien Gouezel (Jun 02 2020 at 14:09):

Ah, this is a docstring from the ancient times!

view this post on Zulip Patrick Massot (Jun 02 2020 at 14:09):

Sébastien, do you know whether counting measures are hidden somewhere?

view this post on Zulip Patrick Massot (Jun 02 2020 at 14:10):

And non-discrete probability measures?

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Patrick Massot (Jun 02 2020 at 14:39):

Oh, I should have checked here before pushing, I missed Sébastien's message.

view this post on Zulip Johan Commelin (Jun 02 2020 at 14:41):

You can push again... it's free.

view this post on Zulip Patrick Massot (Jun 02 2020 at 14:42):

Done

view this post on Zulip 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?

view this post on Zulip Sebastien Gouezel (Jun 02 2020 at 14:47):

Monotone convergence is lintegral_supr_ae in integration.lean.

view this post on Zulip Sebastien Gouezel (Jun 02 2020 at 14:48):

Fatou is lintegral_liminf_le in integration.lean.

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip Patrick Massot (Jun 02 2020 at 14:59):

Thanks. We really need some md file describing how to navigate that part of mathlib.

view this post on Zulip Johan Commelin (Jun 02 2020 at 15:00):

Well, a yaml file is a good first start (-;

view this post on Zulip Patrick Massot (Jun 02 2020 at 15:01):

The YaML file doesn't explain what this crazy ∫⁻ symbol means

view this post on Zulip 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?

view this post on Zulip Patrick Massot (Jun 02 2020 at 15:03):

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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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 :)

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip Johan Commelin (Jun 03 2020 at 18:43):

It's at 1200 tonight

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Gabriel Ebner (Jun 03 2020 at 18:44):

@Johan Commelin Which timezone?

view this post on Zulip Johan Commelin (Jun 03 2020 at 18:46):

Midnight in Amsterdam, Paris, Berlin

view this post on Zulip Johan Commelin (Jun 03 2020 at 18:46):

I think it's 1800 Princeton time

view this post on Zulip Gabriel Ebner (Jun 03 2020 at 18:47):

So in 3 hours, i.e. 24:00? I was confused by the 12.

view this post on Zulip Patrick Massot (Jun 03 2020 at 18:47):

It's getting dangerously close.

view this post on Zulip Reid Barton (Jun 03 2020 at 18:47):

I see 5:30 pm on the IAS website which I assume is US/Eastern

view this post on Zulip Patrick Massot (Jun 03 2020 at 18:47):

Yes, 3 hours

view this post on Zulip Patrick Massot (Jun 03 2020 at 18:47):

5:30 is the beginning of discussions, but the talk starts half an hour later.

view this post on Zulip Patrick Massot (Jun 03 2020 at 18:47):

It's a crazy format.

view this post on Zulip Reid Barton (Jun 03 2020 at 18:48):

Interesting idea to discuss the talk before it happens

view this post on Zulip Patrick Massot (Jun 03 2020 at 18:48):

I replaces a very informal seminar featuring wine and cheese.

view this post on Zulip Patrick Massot (Jun 03 2020 at 18:48):

Before the talk peoples are randomly distributed in Zoom rooms with 6 participants.

view this post on Zulip Patrick Massot (Jun 03 2020 at 18:49):

Then there is the talk and then general discussion.

view this post on Zulip 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.

view this post on Zulip Patrick Massot (Jun 04 2020 at 00:21):

The talk went fine, discussion just stopped (almost two hours after the talk stopped).

view this post on Zulip Johan Commelin (Jun 04 2020 at 14:55):

#2946 Eisenstein criterion (thanks @Chris Hughes :tada: ) is on the merge queue.

view this post on Zulip Johan Commelin (Jun 04 2020 at 14:55):

So we can update this yaml in a moment (-;

view this post on Zulip 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.

view this post on Zulip 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.)

view this post on Zulip 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.

view this post on Zulip 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).

view this post on Zulip Johan Commelin (Jun 04 2020 at 15:41):

Yup, that's the kind of thing I was meaning

view this post on Zulip Johan Commelin (Jun 04 2020 at 15:41):

Same applies to 100.yaml

view this post on Zulip Johan Commelin (Jun 04 2020 at 15:41):

And stacks.yaml, when we ever get there (-;

view this post on Zulip Patrick Massot (Jun 04 2020 at 15:42):

The case of 100.yaml is slightly different because it also lists stuff from outside mathlib

view this post on Zulip Johan Commelin (Jun 04 2020 at 15:43):

But only very little right? Even archive/ is in the mathlib repo

view this post on Zulip Johan Commelin (Jun 04 2020 at 15:43):

So it's only CH that is outside, I think.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Johan Commelin (Jun 04 2020 at 15:49):

Yup, no worries.

view this post on Zulip 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:

view this post on Zulip 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).

view this post on Zulip 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.


Last updated: May 16 2021 at 22:14 UTC