blueprint / dependency graph

Stream: condensed mathematics

[Johan Commelin]

@Patrick Massot wrote some fantastic tooling for the Sphere eversion project, and has improved it over the last couple of days.
I've used it to write some sort of blueprint. But the parts that lie before us are not yet fleshed out in a lot of detail. Work in progress. As a wonderful side effect, we get a really nice graph of what is done, and where we want to go (at least as first target).

I hope that this will move to a more stable URL in a couple of days, but I'm sharing this now because it might already be useful for some things.

https://math.commelin.net/web/
https://math.commelin.net/web/dep_graph.html

[Johan Commelin]

I have not yet updated the text about the snake lemma to reflect the recent discussions.

[Johan Commelin]

If you want to contribute to the text, just ping and I'll give you access to the underlying repo.

[Adam Topaz]

@Johan Commelin It might be worthwhile to add these two links to the README.md file in leanprover-community/lean-liquid.

[Johan Commelin]

I was thinking to wait with that till we have a better URL

[Adam Topaz]

Ah ok.

[Adam Topaz]

I mostly don't want to dig through zulip every time I want to find it :)

[Johan Commelin]

I'm sharing this now with people actively working on the project. But it should become a resource for others as well that want to browse/study the code.

[Johan Commelin]

Yes, but currently it's a random subdirectory of my homepage...

[Johan Commelin]

It should just use github pages, and auto-build using CI. But I don't really know how to set that up.

[Adam Topaz]

I guess we can ask how @Patrick Massot set it up for sphere eversion...

[Adam Topaz]

It looks like https://github.com/leanprover-community/sphere-eversion has no CI.

[Johan Commelin]

Patrick is very busy with setting up his course. And indeed the sphere project doesn't use CI.

[Johan Commelin]

But CI should be easier now, with the changes that Patrick made to his tooling last week.

[Yakov Pechersky]

http://leanprover-community.github.io/liquid

[Yakov Pechersky]

That will auto update on pushes to the master branch of the blueprint, like latex changes

[Yakov Pechersky]

And will also automatically make sure that it links properly to the declarations in the actual lean repo

[Johan Commelin]

Thank you so much for setting up the CI!

[Johan Commelin]

http://leanprover-community.github.io/liquid/dep_graph.html is the graph. we should add a link to it from the main page...

[Yakov Pechersky]

It's very nice to work with Patrick's tools, they're very clear on what they do. The ci is just plumbing his great tools with the ridiculous requirements of getting graphviz and latex to work.

[Yakov Pechersky]

Also Ron's leanprover contrib actions were quite helpful. I think the ci here could be generalized to any mathlib project. And we could provide lean images and actions.

[Yakov Pechersky]

Although probably not worth the effort for lean 3 anymore...

[Kevin Buzzard]

This stuff is really sexy.

[Kevin Buzzard]

I also like how the graph clearly explains how we're about 3/4 the way through the proof :P

[Johan Commelin]

That only means that I should write a lot more stuff about how we break 9.5 into pieces....

[David Michael Roberts]

Def 7 and Lemma 8 in section 2 have missing \tos.

[David Michael Roberts]

And in the bibliography there is

to3em, Lectures on Analytic Geometry, 2020.

[Johan Commelin]

@David Michael Roberts thanks, I'll fix them asap

[Johan Commelin]

I fixed the \tos. I have no idea what's happening in the bibliography. The .bib file looks fine.

[Johan Commelin]

Oooh, in the PDF it looks fine. It should be a long underscore, indicating "same author as above".

@Patrick Massot this seems like a small bug in plastex. Can you confirm?

[Johan Commelin]

I've changed the bib style to avoid the issue

[Patrick Massot]

@Yakov Pechersky it seems CI is no longer working.

[Yakov Pechersky]

Hmm. Seems like a pygraphviz issue. Could this be a function of pip turning off py2 support? Weird, because we're using py3.

[Yakov Pechersky]

Ah I see new pygraphviz doesn't need that cli arg

[Yakov Pechersky]

/home/runner/work/liquid/liquid/lean-liquid/src/system_of_double_complexes.lean:165:4: error: invalid field notation, 'col'' is not a valid "field" because environment does not contain 'system_of_double_complexes.col''

Is this expected?

[Yakov Pechersky]

Ah, it caught a bad lean-liquid commit. Let's try again.

[Yakov Pechersky]

kpathsea:make_tex: Invalid filename `Latin Modern Math/OT', contains ' '
)

! Package fontspec Error: The font "Latin Modern Math" cannot be found.

For immediate help type H <return>.
 ...

l.9 \setmathfont
                [range=\varnothing]{Asana Math}
?
! Emergency stop.
 ...

l.9 \setmathfont
                [range=\varnothing]{Asana Math}
No pages of output.
Transcript written on ../print/blueprint.log.

[Yakov Pechersky]

I have to log off, unfortunately. So I can't fix this particular error currently. Next time I'll be able to will be tomorrow evening. Apologies. But the pygraphviz should be fixed though!

[Scott Morrison]

By the way --- the blueprint and/or dependency graph don't seem to have many links to them! I couldn't find any, and had to construct the URL myself from knowing how github-pages works. Presumably the README.md at https://github.com/leanprover-community/lean-liquid and at https://github.com/leanprover-community/liquid should contain direct links to the rendered pages?

[Bryan Gin-ge Chen]

@Yakov Pechersky The missing font error seems unrelated. The "Latin Modern Math" font was added to blueprint.tex in this commit. I'm not sure why the font isn't being found though; as far as I can tell it should be included in the TexLive image..?

[Johan Commelin]

@Scott Morrison Sorry, this is an artifact of launching the blueprint, but not creating links because it wasn't really fleshed out and there was no CI yet. Then gradually fixing those issues, but forgetting to add links. We should add those links now.

[Johan Commelin]

I've added links to both READMEs

[Yakov Pechersky]

I have an idea on how to fix it, but before that, can we try to revert the font commit that added the Latin Modern Math and Asana Math to the tex files? The new apt add texlive... line would also need to be removed.

[Bryan Gin-ge Chen]

I'm sure Patrick won't mind as long as you're able to figure out how to get it working later.

[Patrick Massot]

I'm deeply shocked that any kind of setup can have difficulties having Latin modern math font, but I don't mind switching to any other font that has decent unicode support.

[Patrick Massot]

In any kind of project mixing LaTeX and Lean we want to be able to copy paste between Lean and LaTeX without converting unicode to ascii or ascii to unicode so \usepackage{unicode-math} is crucial.

[Yakov Pechersky]

The issue was naming the font, it requires hyphens for the Unix setup. I'm finalizing some fixes to speed up CI too

[Yakov Pechersky]

The CI is back to being fixed. And it should be marginally faster now too.

[Yakov Pechersky]

The crucial fix was https://github.com/leanprover-community/liquid/commit/063ed84ee1d21f0d330b285883b26558e9764aec

\setmathfont{latinmodern-math.otf}
\setmathfont[range=\varnothing]{Asana Math} \setmathfont[range=\varnothing]{Asana-Math.otf}

[Yakov Pechersky]

Hmm, no, the blueprint is now just the bibliography.

[Yakov Pechersky]

OK, I've reverted the various CI changes. The only crucial fixes were working with the newer pygraphviz and the font paths. And the websites work now. Sorry this took a while.

[Bryan Gin-ge Chen]

Thanks for working on this!

[Kevin Buzzard]

Yes -- many thanks. I show this web page to mathematicians quite a bit.

[Yakov Pechersky]

I'm glad to help. This type of CI work is a lot of yak shaving. And unfortunately, the github actions aren't amenable to testing locally. The only tool I know that supports this (nektos/act) doesn't support the yaml that we need to pipe the run commands to the texlive image.

[Patrick Massot]

I'm extremely grateful for your work on this because I hate setting up CI (exactly because of the difficulties you met).

[Yakov Pechersky]

image.png

[Yakov Pechersky]

Back to working. My current attempts at making it less brittle have led to empty pages. So I'm going to leave as is for now. The rate limiting step is still building the lean-liquid library.

[Yakov Pechersky]

Happy to participate in the project!

[Johan Commelin]

@Yakov Pechersky Thanks a lot for making everything work again!

[Yakov Pechersky]

Do you prefer all the Proof sections expanded by default on page load?

[Johan Commelin]

I don't have a strong preference here. What do others think? @Patrick Massot

[Patrick Massot]

This is actually a bug in the current blueprint plugin for plasTeX. Around Christmas I updated the default plasTeX theme and when I set up the liquid blueprint I adapted the blueprint plugin only minimally. If you look at the sphere eversion blueprint you'll see proof are folded by default and the + sign next to the proof word actually works.

[Riccardo Brasca]

This is maybe my fault, but in the proof of lemmas 4.7 and 4.8 in https://leanprover-community.github.io/liquid/ there is an equation that is not well displayed (I see the LaTeX source instead of the actual formula)

[Patrick Massot]

This is purely a mathjax issue, but I have a hard time understanding what mathjax doesn't like here (given that it likes several things that seem to use the same LaTeX stuff).

[Filippo A. E. Nuccio]

Is it able to understand \left and \right with the unicode symbol for \Vert?

[Patrick Massot]

Minimized version:

<!DOCTYPE html>
<html lang="en">
<head>
<script type="text/x-mathjax-config">
  MathJax.Hub.Config({tex2jax: {inlineMath: [['$','$'], ['\\(','\\)']]}});
</script>
<script type="text/javascript" src="https://cdnjs.cloudflare.com/ajax/libs/mathjax/2.7.7/latest.js?config=TeX-AMS_CHTML">
</script>
<meta charset="utf-8" />
<title>Mathjax is sometimes strange</title>
</head>

<body>
<p>The following works:</p>
<span>\begin{align*}  ‖y‖ & ≤ K ‖dw‖ + τ \\ & ≤ K (‖x_{|kc}‖ + K‖dx‖ + η) + τ \\ & ≤ K(K + 1) ‖x‖ + Kη + τ \end{align*}</span>
<p>but the following doesn't work:</p>
<span>\begin{align*}  ‖x_{|c} - dy‖ & = \left‖∑_{j ≥ 0} x^j_{|c} - dy^j\right‖ \\ & ≤ ∑_{j ≥ 0} \left‖x^j_{|c} - dy^j\right‖ \\ & ≤ ∑_{j ≥ 0} K‖dx^j‖ + δ_j \\ & ≤ K‖dx‖ + Kε_0 + δ_0 + ∑_{j > 0} (Kε_j + δ_j) \end{align*}</span>

</body>
</html>

Anyone can paste that in a html file and open it in a browser.

[Patrick Massot]

And Filippo gets credit for a successful psychoanalysis of mathjax!

[Patrick Massot]

So we should replace \left‖ by \left\| everywhere in the blueprint.

[Patrick Massot]

Maybe it's a good place to point out that || and \| do not produce the same result in LaTeX (the notes are full of ||, this is minor point but since we are discussing it anyway...).

[Filippo A. E. Nuccio]

:wink:

[Patrick Massot]

I tried a search/replace, let's see whether CI builds something nicer.

[Filippo A. E. Nuccio]

Also, do you want to distinguish between delimiters and binary operations? They get mixed up, using |, no?

[Kevin Buzzard]

there's \mid and \vert right?

[Filippo A. E. Nuccio]

Yes

[Johan Commelin]

I have refactored the blueprint to the generalisation of the construction system of complexes to work for profinitely filtered pseudo-normed groups with $r'$-action of $T^{-1}$.

[Johan Commelin]

So now it should match the Lean code again, if I didn't mess up.

[David Michael Roberts]

Johan Commelin said:

http://leanprover-community.github.io/liquid/dep_graph.html is the graph. we should add a link to it from the main page...

I can't see such a link at https://leanprover-community.github.io/liquid/ or on the community homepage.

[Johan Commelin]

@Patrick Massot Can we easily add a link to the graph from the blueprint page?

[Johan Commelin]

I've started moving bits and pieces of the proof of 9.5 into separate definitions and sublemmas. I will continue doing that in the next few days. Hopefully that will give more people an idea of the global picture of the proof.

[Patrick Massot]

Maybe it's time to split the blueprint into several HTML pages anyway. In that case we can easily add a link to the graph page from the menu, as in https://leanprover-community.github.io/sphere-eversion/blueprint/index.html

[Johan Commelin]

I already split the tex into several files this morning...

[Johan Commelin]

@Patrick Massot If you could help with splitting the blueprint into several html pages, that would be great

[Patrick Massot]

Sure, I'll do it.

[Patrick Massot]

I managed to waste almost two hours on this because I forgot I set myself a trap in the leanblueprint plasTeX plugin. The liquid blueprint modification is two characters long (actually one would be enough) but it didn't work before I fixed the plugin. I forgot that the page layout is overidden in the blueprint plugin (precisely to add this dependency graph link!). And I forgot to propagate a plasTeX change there, so things were inconsistent...

[David Michael Roberts]

There's a funny empty lemma in the blueprint now: https://leanprover-community.github.io/liquid/sect0003.html#a0000000085. The proof is given as:

This is a standard result. We have not formalised it yet, but it is work in progress.

:rolling_on_the_floor_laughing:

[Adam Topaz]

This is referring to Gordan's lemma. It's a rendering issue.

[Adam Topaz]

You can take a look at the source here...
https://github.com/leanprover-community/liquid/blob/a905f671aa440b92ec44bb58e95ff0068579e78f/src/polyhedral_lattice.tex#L46

[David Michael Roberts]

I thought as much. Was just worth flagging, methinks.

[Johan Commelin]

@Patrick Massot Thanks a lot! The new version looks fantastic!

[David Michael Roberts]

Ditto, it's very nice!

[Johan Commelin]

There's now a pretty fleshed out roadmap again. Major thanks to @Peter Scholze for all his input.
See https://leanprover-community.github.io/liquid/dep_graph.html for what the graph looks like now.

[Johan Commelin]

Important: some of the non-green things might already be done in Lean. I still need to add a bunch of pointers.

[Johan Commelin]

So please ask on this stream before you start hacking on something.

[Johan Commelin]

Here is yet another update of the dep-graph: https://leanprover-community.github.io/liquid/dep_graph_section_2.html

The node M-ses is approaching completion. Filippo is working on this.
The node Lbar-ses is also almost done. Two relatively straightforward sorrys remain.

acyclic-sheaf and free-png are two nodes that will require something beyond homological algebra. The rest seems to be only homological algebra.

[Adam Topaz]

How are we defining $H^i(S,M)$ in acyclic-sheaf? As Ext(Z[S],M)?

[Johan Commelin]

Yes, exactly

[Adam Topaz]

Okay, that shouldn't be too bad once we have the LES for Ext (the sheaf condition should be straighforward I think)...

[Kevin Buzzard]

I'll try the Lbar-ses sorries now

[Johan Commelin]

Adam, I think you already did a prerequisite in part 1, right?

[Johan Commelin]

We really need to finally get a complete API for Ext...

[Johan Commelin]

Sorry count is going down again! We were almost at a hundred just a little while ago.

3 src/condensed/rescale.lean
4 src/condensed/condensify.lean
5 src/Lbar/ext.lean
2 src/Lbar/ses.lean
6 src/real_measures/basic.lean
1 src/breen_deligne/main.lean
1 src/free_pfpng/acyclic.lean
3 src/free_pfpng/main.lean
6 src/invpoly/ses.lean
2 src/laurent_measures/thm69.lean
2 src/laurent_measures/ext.lean
3 src/laurent_measures/ses2.lean
14 src/laurent_measures/ses.lean
1 src/for_mathlib/bicartesian.lean
1 src/for_mathlib/derived/les.lean
2 src/for_mathlib/derived/les_facts.lean
12 src/for_mathlib/derived/derived_cat.lean
1 src/for_mathlib/derived/les2.lean
69 total

[Johan Commelin]

Yet another green oval: https://leanprover-community.github.io/liquid/dep_graph_section_2.html
Thanks to @Kevin Buzzard's efforts Lbar-ses is now done.

[Scott Morrison]

I have spent the day trying to make discrete either a structure or irreducible. This might not look like LTE, but secretly is: afterward I'm hoping both shift functors and pretriangulated categories will work better, and we'll have a clearer path to setting up derived categories.

[Johan Commelin]

Did you hit trouble? Or is it mostly working?

[Scott Morrison]

Unfortunately the coherence theorems for monoidal categories and bicategories seem to rely on this heavily, and I quickly got lost.

[Scott Morrison]

I will ask Yuma and/or Markus soon to help out. Otherwise, it is starting to work. Still a ways to go. I may ask @Adam Topaz if he can help fix the multiequalizers file, as I'm confused by the errors there and he wrote it recently. (This is on branch#discrete_structure.)

[Scott Morrison]

I've finally reached the shift.lean file --- where apparently every single line has a red squiggle. :-) Hopefully this is a good sign, however, that after fixing it will work better.