Zulip Chat Archive

Stream: condensed mathematics

Topic: liquid tensor experiment


view this post on Zulip Johan Commelin (Jan 20 2021 at 10:45):

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.

view this post on Zulip 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 p-adic geometry, please join forces with us!

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

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

view this post on Zulip 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 sorrys is great help.

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

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

view this post on Zulip Johan Commelin (Jan 20 2021 at 11:01):

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

view this post on Zulip Riccardo Brasca (Jan 20 2021 at 11:01):

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

view this post on Zulip Johan Commelin (Jan 20 2021 at 11:03):

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

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

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

view this post on Zulip Peter Scholze (Jan 20 2021 at 11:14):

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

view this post on Zulip Johan Commelin (Jan 20 2021 at 11:17):

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

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

view this post on Zulip Peter Scholze (Jan 20 2021 at 11:32):

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!

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

view this post on Zulip Johan Commelin (Jan 20 2021 at 15:47):

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

view this post on Zulip Riccardo Brasca (Jan 20 2021 at 15:49):

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

view this post on Zulip 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 sorrys under your guidance.

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

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

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

view this post on Zulip Bhavik Mehta (Jan 20 2021 at 21:40):

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

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

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

view this post on Zulip Johan Commelin (Mar 18 2021 at 08:56):

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

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

view this post on Zulip Peter Scholze (Mar 18 2021 at 09:18):

In particular, I now really think that the proof has to go from R\mathbb R to Z((T))r\mathbb Z((T))_r. Previously, my main motivation to do so was the desire to combine real and pp-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.

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

view this post on Zulip Peter Scholze (Mar 18 2021 at 09:36):

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

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

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

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

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

view this post on Zulip Damiano Testa (Mar 18 2021 at 09:39):

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

view this post on Zulip Peter Scholze (Mar 18 2021 at 09:40):

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

view this post on Zulip Peter Scholze (Mar 18 2021 at 09:40):

they even have holes!

view this post on Zulip 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 non-simply-connected amoeba.

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

view this post on Zulip Damiano Testa (Mar 18 2021 at 09:43):

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.

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

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

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

view this post on Zulip Peter Scholze (Mar 22 2021 at 20:55):

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: ;-)

view this post on Zulip Patrick Massot (Mar 22 2021 at 20:56):

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

view this post on Zulip Peter Scholze (Mar 22 2021 at 20:57):

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

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

view this post on Zulip 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/nonconvexity-and-discretization . This probably makes it ~10 times likelier that there's a fatal mistake somewhere... :grimacing: ;-)

10ε=ε10 \cdot \varepsilon = \varepsilon


Last updated: May 09 2021 at 22:13 UTC