Zulip Chat Archive
Stream: condensed mathematics
Topic: liquid tensor experiment
Johan Commelin (Jan 20 2021 at 10:45):
https://github.com/leanprovercommunity/leanliquid together with @Adam Topaz and @Kevin Buzzard I've worked on formalizing the statement that is the goal of the Liquid Tensor Experiment (https://xenaproject.wordpress.com/2020/12/05/liquidtensorexperiment/).
The main source for this project is http://www.math.unibonn.de/people/scholze/Analytic.pdf .
I can now say that I'm confident that we can make this project happen. Succesful completion of this project would be a major success story for mathlib and its community.
As I see it, there are two independent strands that can be worked on:
 The proof of theorem 9.4 (the statement that is formalized in the repo I linked to above).

Theorem 9.4 is a crucial building block in setting up liquid/condensed maths. If you want to flex your categorical mathlib muscles, it would be very interesting to build the category of solid modules, and state theorem 6.5.
 Once that is done, we can start working on connecting 6.5 and 9.4. But that is certainly something that should be postponed for the time being.
Johan Commelin (Jan 20 2021 at 10:51):
The proof of 9.4 (so, part 1) contains a lot of calculations with normed abelian groups, and inequalities between norms of elements living in complexes of normed abelian groups. So if your background is functional analysis instead of padic geometry, please join forces with us!
Riccardo Brasca (Jan 20 2021 at 10:54):
If there is a way to help for people less experienced in Lean than you pleas let us know. I would be very happy to contribute
Kevin Buzzard (Jan 20 2021 at 10:56):
I think it would be very interesting to write down a detailed paper proof of what needs to be done, perhaps more detailed than the blog post but not as long as the two Scholze course files!
Johan Commelin (Jan 20 2021 at 10:58):
@Riccardo Brasca I'm sure you can help. The tricky thing is to get definitions right. But a proof is a proof, so helping to kill sorry
s is great help.
(Of course I don't want to discourage you from playing with definitions.)
Riccardo Brasca (Jan 20 2021 at 11:00):
I agree. I think that there are quite a lot of people in a position similar to mine: we are ready to contribute, but we do not know how to start for such a huge project and we need some guidance. I am not saying you should coordinate people (that requires a lot of effort and it is probably not that interesting), just that in a dream world there would be a list of stuff to be done, and we can start working on the easiest. Of course it is super interesting just to read what you have done and play with it.
Johan Commelin (Jan 20 2021 at 11:01):
I think such a list of things will start to appear quite soon.
Riccardo Brasca (Jan 20 2021 at 11:01):
@Johan Commelin Killing some sorry is exactly what I am looking for :)
Johan Commelin (Jan 20 2021 at 11:03):
Here's something that doesn't look too complicated: lemma 9.7
Peter Scholze (Jan 20 2021 at 11:10):
I'm really impressed that within a month, you were able to formalize the statement of the technical main result!
Peter Scholze (Jan 20 2021 at 11:13):
@Kevin Buzzard The proof of 9.4, that is the main focus right now, is essentially completely contained in Lecture 9 and its appendix in www.math.unibonn.de/people/scholze/Analytic.pdf ; I think there is almost no backwards referencing (one thing that is relevant is the second appendix to Lecture 8, on completions of normed abelian groups). So everybody who wants to contribute can concentrate on that part. I think each Lemma that is stated (e.g. 9.7 and 9.8) is something that one can work on.
Peter Scholze (Jan 20 2021 at 11:14):
As is the "normed snake lemma" 9.10 or the "normed spectral sequence" 9.6
Johan Commelin (Jan 20 2021 at 11:17):
I'll try to push a statement of 9.10 in a moment.
Peter Scholze (Jan 20 2021 at 11:32):
Just checking: I think one literally only needs to read the second appendix to Lecture 8 (on completions of normed abelian groups) and lecture 9 with its appendix.
Peter Scholze (Jan 20 2021 at 11:32):
The appendix to lecture 9, in the written version, contains some heavy backwards referencing to BreenDeligne resolutions, but Johan Commelin found a very nice way to avoid any of the hard proofs on BreenDeligne resolutions!
Riccardo Brasca (Jan 20 2021 at 15:42):
I don't know if you are interested in comments about typos in your project, but if this is the case, the link https://leanprover.zulipchat.com/#narrow/stream/266894liquid/topic/bounded.20exactness/near/220823654 in src/system_of_complexes.lean
doesn't work for me.
Johan Commelin (Jan 20 2021 at 15:47):
aah, that's because it links to a deprecated private stream from the experimentation period...
Riccardo Brasca (Jan 20 2021 at 15:49):
In any case the file is very readable at its current state
Filippo A. E. Nuccio (Jan 20 2021 at 15:51):
I want to second Riccardo' s comment, saying that I'd also like to start playing with proofs and helping resolving some sorry
s under your guidance.
Kevin Buzzard (Jan 20 2021 at 16:25):
I'm having a rather hectic week (giving 5 talks in a 7 day period!) but when the chaos is over on Friday I will be turning my mind to trying to figure out how we can use the community here to do something brilliant.
Johan Commelin (Jan 20 2021 at 16:51):
@Filippo A. E. Nuccio Cool, welcome. If you want, you can have a go at lemma 9.7.
Filippo A. E. Nuccio (Jan 20 2021 at 17:03):
Sure! I'm now finishing a project on Dedekind domains (still ten days), and won't be very fast 'till then. But I will certainly start looking at it.
Starting from February I'll be more efficient. If that is a problem, you can assign the Lemma to someone else, but if not I'll be happy to work on it.
Bhavik Mehta (Jan 20 2021 at 21:40):
As for the categorical side, the rough status is that we have the proetale site of a point in a branch of mathlib (with myself, @Kenny Lau and mostly @Calle Sönne) and sheaves of structures in another branch of mathlib (with myself and @Kevin Buzzard). As Kevin and Johan have mentioned elsewhere, an intermediate goal is to construct the category of condensed abelian groups and prove Theorem 2.2 of https://www.math.unibonn.de/people/scholze/Condensed.pdf
Peter Scholze (Mar 18 2021 at 08:25):
Some reflections about the proof, trying to get some perspective on what's actually happening: https://mathoverflow.net/questions/386796/nonconvexityanddiscretization
Johan Commelin (Mar 18 2021 at 08:53):
Say you want to travel from A to B. The convex solution is to just take your car: The cost (as say measured in time) scales pretty much linearly in the distance, and you will simply take the shortest route. If you look at the region you can reach in a given time, you get some convex region  essentially a circle. The nonconvex solution is to first walk to the bus station, then take the bus to the train station, then take the train to the airport, then fly, and finally reverse those steps. The set of points you can reach via this method in a given time is highly nonconvex.
I'm glad we now finally have a formal proof of this folklore result :rofl:
Johan Commelin (Mar 18 2021 at 08:56):
I think this analogy is really nice, by the way!
Peter Scholze (Mar 18 2021 at 09:17):
Yes, I was really happy when I found that analogy! I actually only found it when writing the question, and I think it made me understand much better what's going on
Peter Scholze (Mar 18 2021 at 09:18):
In particular, I now really think that the proof has to go from $\mathbb R$ to $\mathbb Z((T))_r$. Previously, my main motivation to do so was the desire to combine real and $p$adic stuff, and the justification for doing so was purely technical (the importance of profinite sets for condensed math), but now I think there's a clear conceptual reason for doing it.
Damiano Testa (Mar 18 2021 at 09:27):
Peter, a vague idea that floats in my mind is that a baby case of what you are describing is what happens in tropical geometry, where you convert a (usually nonlinear) algebraic variety to a piecewise linear combinatorial structure. The connection happens via valued fields.
I also remember going to a talk (for which I can try to remember more details, if there is the need), where tropical geometry was applied to solve (or at least change) some differential equation into a combinatorial problem.
Peter Scholze (Mar 18 2021 at 09:36):
Hmm, is that a similar situation? Somehow tropical geometry is highly nonconvex
Damiano Testa (Mar 18 2021 at 09:37):
I kind of view the data of tropical geometry as being packaged by piecewise linear (piecewise convex, in this context) information. From the point of view of algebraic geometry, tropical geometry is very linear!
Damiano Testa (Mar 18 2021 at 09:38):
So, I would view your analogy as the picture of a "forming amoeba": let me see if I can find an animation for that.
Peter Scholze (Mar 18 2021 at 09:39):
Hmm OK, I see what you say. I guess tropical geometry is also looking at a space by viewing it from widely different scales
Damiano Testa (Mar 18 2021 at 09:39):
Hmm, not exactly an animation, but some of the pictures in this paper convey some idea:
https://arxiv.org/pdf/math/0403015.pdf
Damiano Testa (Mar 18 2021 at 09:39):
I have in mind that you try to fit nonlinear data with as much linearity as you can...
Peter Scholze (Mar 18 2021 at 09:40):
But you see, those amoebas are really nonconvex...
Peter Scholze (Mar 18 2021 at 09:40):
they even have holes!
Kevin Buzzard (Mar 18 2021 at 09:41):
Are you sure this isn't the nucleus? I would be worried about the health of a nonsimplyconnected amoeba.
Damiano Testa (Mar 18 2021 at 09:41):
I can see that, but I also remember that a "line" is a tripod! So, linear outside of tropical geometry becomes piecewise linear, but the language allows you to treat is as "more linear than you would imagine"!
Damiano Testa (Mar 18 2021 at 09:43):
Anyway, I intuitively think of tropical geometry as a "firstorder approximation" to algebraic geometry and, when you look at it like this, you can see a resemblance of linearity. The valued fields are really key to this.
Damiano Testa (Mar 18 2021 at 09:44):
Of course, if you are linearizing a curve of genus one, there has to be a hole and some "bending", but this happens in a very controlled way.
Peter Scholze (Mar 18 2021 at 09:47):
Yes, that's a fair picture. I'd just expect that somebody like Bourgain might have used techniques somewhat similar to what I'm asking about, but I just don't know anything about the general area. Well, I hope the MO question will generate some interesting answers.
Damiano Testa (Mar 18 2021 at 09:53):
In the meantime, I found a video of a seminar that looks almost identical to the one that I had in mind. The speaker gives an idea of how to convert differential equations into combinatorial structures that are almost exactly the realm of tropical geometry:
https://www.youtube.com/watch?v=pMlo3LD3wU
Peter Scholze (Mar 22 2021 at 20:55):
Hmm, Terry Tao doesn't seem to know the method https://mathoverflow.net/questions/386796/nonconvexityanddiscretization . This probably makes it ~10 times likelier that there's a fatal mistake somewhere... :grimacing: ;)
Patrick Massot (Mar 22 2021 at 20:56):
Oh, I wanted to suggest asking him and then I forgot.
Peter Scholze (Mar 22 2021 at 20:57):
MO did so, see the comments to my question ;)
Peter Scholze (Mar 22 2021 at 20:59):
I find this genuinely confusing, I was sure that after extracting this kind of "big picture idea" I would finally be able to connect this stuff to what other people are doing over the reals. But it just seems to be different... but coming from the condensed perspective, there's literally nothing else one might be doing over the reals!
Adam Topaz (Mar 22 2021 at 21:12):
Peter Scholze said:
Hmm, Terry Tao doesn't seem to know the method https://mathoverflow.net/questions/386796/nonconvexityanddiscretization . This probably makes it ~10 times likelier that there's a fatal mistake somewhere... :grimacing: ;)
$10 \cdot \varepsilon = \varepsilon$
Last updated: May 09 2021 at 22:13 UTC