liquid tensor experiment

Stream: condensed mathematics

[Johan Commelin]

https://github.com/leanprover-community/lean-liquid 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/liquid-tensor-experiment/).
The main source for this project is http://www.math.uni-bonn.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:

1. The proof of theorem 9.4 (the statement that is formalized in the repo I linked to above).

2. 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]

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 p-adic geometry, please join forces with us!

[Riccardo Brasca]

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]

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]

@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 sorrys is great help.

(Of course I don't want to discourage you from playing with definitions.)

[Riccardo Brasca]

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]

I think such a list of things will start to appear quite soon.

[Riccardo Brasca]

@Johan Commelin Killing some sorry is exactly what I am looking for :)

[Johan Commelin]

Here's something that doesn't look too complicated: lemma 9.7

[Peter Scholze]

I'm really impressed that within a month, you were able to formalize the statement of the technical main result!

[Peter Scholze]

@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.uni-bonn.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]

As is the "normed snake lemma" 9.10 or the "normed spectral sequence" 9.6

[Johan Commelin]

I'll try to push a statement of 9.10 in a moment.

[Peter Scholze]

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]

The appendix to lecture 9, in the written version, contains some heavy backwards referencing to Breen-Deligne resolutions, but Johan Commelin found a very nice way to avoid any of the hard proofs on Breen-Deligne resolutions!

[Riccardo Brasca]

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/266894-liquid/topic/bounded.20exactness/near/220823654 in src/system_of_complexes.lean doesn't work for me.

[Johan Commelin]

aah, that's because it links to a deprecated private stream from the experimentation period...

[Riccardo Brasca]

In any case the file is very readable at its current state

[Filippo A. E. Nuccio]

I want to second Riccardo' s comment, saying that I'd also like to start playing with proofs and helping resolving some sorrys under your guidance.

[Kevin Buzzard]

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]

@Filippo A. E. Nuccio Cool, welcome. If you want, you can have a go at lemma 9.7.

[Filippo A. E. Nuccio]

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]

As for the categorical side, the rough status is that we have the pro-etale 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.uni-bonn.de/people/scholze/Condensed.pdf

[Peter Scholze]

Some reflections about the proof, trying to get some perspective on what's actually happening: https://mathoverflow.net/questions/386796/nonconvexity-and-discretization

[Johan Commelin]

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]

I think this analogy is really nice, by the way!

[Peter Scholze]

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]

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]

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 non-linear) 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]

Hmm, is that a similar situation? Somehow tropical geometry is highly nonconvex

[Damiano Testa]

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]

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]

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]

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]

I have in mind that you try to fit non-linear data with as much linearity as you can...

[Peter Scholze]

But you see, those amoebas are really nonconvex...

[Peter Scholze]

they even have holes!

[Kevin Buzzard]

Are you sure this isn't the nucleus? I would be worried about the health of a non-simply-connected amoeba.

[Damiano Testa]

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]

Anyway, I intuitively think of tropical geometry as a "first-order 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]

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]

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]

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=pMlo3L-D3wU

[Peter Scholze]

Hmm, Terry Tao doesn't seem to know the method https://mathoverflow.net/questions/386796/nonconvexity-and-discretization . This probably makes it ~10 times likelier that there's a fatal mistake somewhere... :grimacing: ;-)

[Patrick Massot]

Oh, I wanted to suggest asking him and then I forgot.

[Peter Scholze]

MO did so, see the comments to my question ;-)

[Peter Scholze]

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]

Peter Scholze said:

Hmm, Terry Tao doesn't seem to know the method https://mathoverflow.net/questions/386796/nonconvexity-and-discretization . This probably makes it ~10 times likelier that there's a fatal mistake somewhere... :grimacing: ;-)

$10 \cdot \varepsilon = \varepsilon$

[Johan Commelin]

This post is of course quite late... I've been living under a rock the last couple of months.

This whole experiment started with a blogpost and a theme song. For anyone who's into it, here is another theme song, Solid Resolution Theory:
https://www.youtube.com/watch?v=DTnXcMLfUBc&list=OLAK5uy_nYyRCFDMzg4lNQnHrOsf7tcoG1PfRxNzQ&index=10

Who would have thought that the Liquid Tensor Experiment blogpost (Dec 5, 2020) would prompt the original LTE to pick up their instruments again after more than 20 years, and announce a new album within two weeks after Peter's blogpost!!!

[Peter Scholze]

I think now we're also even with stealing names ;-)