## Stream: condensed mathematics

### Topic: freestyle

#### Johan Commelin (Apr 01 2021 at 05:16):

I propose a somewhat radical change of plans. It's clear to all of us that reaching a sorry-free proof of first_target (aka theorem 9.4) is just a matter of time. So I think that we should think big, and look ahead a quite bit further. We now have a very clear idea of how to do homological algebra, and the derived functor RHom in the statement of 9.1 should be well within reach.
In line with the Formal Abstracts proposal, we should focus more on definitions and theorem statements, and just sorry our way towards 9.1. We should then steam ahead, define pre-analytic rings and analytic rings, and state theorem 6.5 (that $\R$ is an analytic ring). I'm optimistic that with our sorry-strategy, we can get there in a very short amount of time. We are spending way too much human capital on proving these sorry's, but we should be leaving those to AIs that are getting better and better. See for example GPT-AF that is hot from the presses. In a couple of months these AIs will look at the gaps that we jump over and just fill them in without thinking twice.

And then the fun begins! Once we have 6.5 stated in Lean, we can start freestyling! Formulate a liquid Hodge theory that works over (some form of) $\mathrm{Spec}(\Z)$ with specializations to classical Hodge theory and $p$-adic Hodge theory, get comparison isomorphisms between the various cohomology theories almost for free; state the Hodge conjecture in a very general form. We just sorry the Hodge conjecture, and move on! Some AI will come along and prove it, maybe 1 year from now. Who knows what lies beyond. Let's dance into a wide open future!

#### Patrick Massot (Apr 01 2021 at 07:14):

I prefer Jason's autoformalisation plan, it sounds more ambitious.

#### Filippo A. E. Nuccio (Apr 01 2021 at 08:08):

Although I certainly sympathize with @Johan Commelin 's free-style dance proposal, and humbled by his experience, I simply wonder if going too far ahead before trying to formalize would not harm the choice of "right" definitions. For instance, all the pain Damiano is going through with something mathematically "basic" as Gordan's lemma, scares me a bit.

#### Kevin Buzzard (Apr 01 2021 at 08:13):

You shouldn't worry about this Gordan's lemma thing. This is just the usual kind of noise which formalisation runs into now and again, and will be solved soon -- it's just all about setting up definitions correctly. Diamonds are always a problem but they can be eliminated

#### Filippo A. E. Nuccio (Apr 01 2021 at 08:17):

No, I was not worried about the Gordan's think per se. Just that similar things might occur if we steam ahead and we later need to refactor.

#### Filippo A. E. Nuccio (Apr 01 2021 at 08:17):

But OK, I am admittedly not enough experienced in the large picture, so don't mind.

#### Damiano Testa (Apr 01 2021 at 08:19):

Also, just a small comment: the noise right now is about the fact that we "feel" that we should have finished the proof a few lines earlier than where it really finished!

I would like to get to the bottom of this, but Riccardo did prove the lemma, as stated.

#### Riccardo Brasca (Apr 01 2021 at 08:21):

And the problem has nothing to do with Gordan's lemma!

#### Riccardo Brasca (Apr 01 2021 at 10:53):

Regarding the general plan I agree that we should start thinking big. Getting the right definitions is hard, but in my opinion leaving a lot of sorry is a very good idea (I mean, when we are more or less convinced we can prove the result): this should guide us towards the good notion, and also is very important for someone who will want to join the project. Starting to work on small sorry is fun and doable quite quickly. If a beginner arrives and see that the main discussion is about having a topology on each M_c but not on the union for reasons that are completely irrelevant mathematically I don't think he will become interested.

#### Riccardo Brasca (Apr 01 2021 at 10:56):

This was at least my personal experience. When I opened the project for the first time I was really surprised that it was reasonable to prove a proposition that appears quite late in the paper in a few days (the normed snake lemma). And I was even more surprised when this actually worked pretty well. Of course this happened thank's to the incredible effort of Johan, that had already set up all the foundations in the right way.

#### Mario Carneiro (Apr 01 2021 at 10:56):

If a beginner arrives and see that the main discussion is about having a topology on each M_c but not on the union for reasons that are completely irrelevant mathematically I don't think he will become interested.

That depends on what kind of beginner you are talking about

#### Riccardo Brasca (Apr 01 2021 at 10:57):

Yes, I was thinking about something coming from "standard mathematics".

#### Mario Carneiro (Apr 01 2021 at 10:58):

for folks like me who know how to lean but have very little insight into condensed sets and normed group something somethings it's good to have unsolved formalization questions in largely-encapsulated form

#### Riccardo Brasca (Apr 01 2021 at 10:58):

I wouldn't call you "a beginner"... :rolling_on_the_floor_laughing:

#### Mario Carneiro (Apr 01 2021 at 10:59):

Of course a successful advanced mathematics formalization project requires a mixture of formalizers and mathematicians

#### Mario Carneiro (Apr 01 2021 at 11:02):

I'm not just talking about me though, but also say undergraduate students who are new to the mathematics and have been playing with lean for a little while (i.e. me from 6 years ago)

#### Mario Carneiro (Apr 01 2021 at 11:02):

(well, I wasn't playing with lean 6 years ago but you get the idea)

#### Riccardo Brasca (Apr 01 2021 at 11:05):

Sure! I was thinking about my colleagues, they are not so interested to see the details of the work, and they are probably a little skeptical, but if we succeed they will surely want to know more about it. For example there is a working group in my university about condensed sets and if I can say to them "we have all the tiny details written down extremely precisely" this can help the understanding of the math.
On the other end of the spectrum there are people like you, expert in formalization but less into the mathematics... and of course nothing would be possible without you.

#### Mario Carneiro (Apr 01 2021 at 11:12):

I see most mathematicians taking a role like Scholze has been doing, where they may help with making the paper proof more precise and detailed without necessarily actually interacting directly with the proof assistant. You have to already be somewhat computationally minded to even get as far as writing real lean code

#### Patrick Massot (Apr 01 2021 at 11:23):

All these people seriously discussing Johan's message are scaring me off. Did this whole condensed mathematics stuff also started as an April fool by Peter saying we should stop using topological spaces and start using, say sheaves on the proétale whatever instead?

#### Peter Scholze (Apr 01 2021 at 11:32):

I saw some discussion on the internet whether my "liquid tensor experiment" blogpost was really an elaborate joke; somehow nobody seems convinced by my judgment that this may be my most important theorem

#### Riccardo Brasca (Apr 01 2021 at 11:39):

I got that "Formulate a liquid Hodge theory that works over (some form of) $\mathrm{Spec}(\Z)$ with specializations to classical Hodge theory and $p$-adic Hodge theory, get comparison isomorphisms between the various cohomology theories almost for free" was a little too ambitious to be true, but the idea of thinking big seems very good to me... even on April 1st!

#### Peter Scholze (Apr 01 2021 at 11:41):

Well, before you think big, I actually want a sorry-free proof of 9.4 (and 9.1) :wink: Giving sorry-ed proofs is easy enough to do on paper :stuck_out_tongue:

#### Filippo A. E. Nuccio (Apr 01 2021 at 11:43):

Are you looking for the next inspiration for the name of a theory? https://www.youtube.com/watch?v=WJI2HVWIQZw :grinning_face_with_smiling_eyes:

#### Peter Scholze (Apr 01 2021 at 11:45):

@Filippo A. E. Nuccio OK, I'm not getting that joke

#### Filippo A. E. Nuccio (Apr 01 2021 at 11:46):

@Peter Scholze Was just referring to some tribute paid to Liquid Tension Experiment and to Prisms, but doesn't matter... I just ended up finding that song and the thinking big/small discussion made link in my mind.

#### Johan Commelin (Apr 01 2021 at 12:47):

(Speaking of April Fool's jokes... Dutch politics probably doesn't make it far onto the international scene, but right now they are having some very elaborate "jokes" while forming the new government. They couldn't have chosen a better day. :see_no_evil: )

#### Adam Topaz (Apr 01 2021 at 13:37):

All jokes aside, it does seem to me that Peter was trolling the physicists when he mentioned the Novikov ring ;)

#### Peter Scholze (Apr 01 2021 at 13:48):

Not really... I mean I don't think that's real physicists, but just mirror symmetry people, right? We do end up looking at pretty much exactly the Novikov ring... so I actually do wonder whether there's some relation, but of course I understand very little about mirror symmetry

#### Adam Topaz (Apr 01 2021 at 13:50):

(I was actually joking :smile:) I also know nothing about this, but there are more math-physicists in my department than number theorists so I hear about the Novikov ring and quantum cohomology much more than p-adic Hodge theory

#### Adam Topaz (Apr 01 2021 at 13:52):

And yeah I think it's just the mirror-symmetry and the Gromov-Witten invariant folks who work with this object.

#### Peter Scholze (Apr 01 2021 at 13:53):

In mirror symmetry, there's this weird thing that you have to replace the coefficients $\mathbb Z$ by this funny Novikov ring. Somehow exactly the same happens in the liquid story: It can't be defined directly over $\mathbb Z$, you first have to pass to essentially the Novikov ring. It may not mean anything, but it's at least worth pointing out...

#### Adam Topaz (Apr 01 2021 at 13:56):

From what I understand (and I don't actually understand), it's not necessarily that it's required to work over the Novikov ring, but rather you can deform the usual cup-product if you work over this ring so that the cup-product encodes something about Gromov-Witten invariants.

#### Adam Topaz (Apr 01 2021 at 13:56):

But I agree it would be surprising if it's a coincidence :)

#### Peter Scholze (Apr 01 2021 at 13:56):

Hmm, I think the Fukaya category is only defined over this ring

Oh I see yeah

#### Adam Topaz (Apr 01 2021 at 14:02):

Peter, the first example in section 5 of https://ncatlab.org/nlab/show/Novikov+field might have some connection with your recent MO post. Unfortunately "magnitude homology" is a stub on the nlab

#### Matthew Ballard (Apr 01 2021 at 14:04):

The introduction of the Novikov ring (or field) is essentially a compactness issue for moduli spaces. If you weight the holomorphic curves by area, then the areas $\to \infty$ and you make a ring off this. In situations where there is some ampleness of the anti-canonical bundle you can prove convergence of the resulting series. The really interesting thing is that Novikov seems to be an essential ingredient for mirror symmetry in general: statements won't match up even they make sense over $\mathbb{C}$ but will over $\Lambda$.

If condensed mathematics can say something about the structure of derived categories for varieties that is not accessible otherwise, that would be nice.

#### Matthew Ballard (Apr 01 2021 at 14:12):

(Sorry to jump in. This Zulip is my relaxing reading.)

#### Peter Scholze (Apr 01 2021 at 14:12):

sorry, I was away for a second!

#### Peter Scholze (Apr 01 2021 at 14:15):

Interesting @ magnitude homology

#### Peter Scholze (Apr 01 2021 at 14:23):

@Matthew Ballard What do you mean by "the structure of derived categories"?

#### Matthew Ballard (Apr 01 2021 at 14:24):

I wonder if there applications to degeneration questions or categorical stability questions for the category.

#### Peter Scholze (Apr 01 2021 at 14:25):

Here's something very vague. If I understand it right (from very far away), if you start with a symplectic manifold $M$, its Fukaya category is a $\Lambda$-linear triangulated category. Homological mirror symmetry says that this should be the category of coherent sheaves on some algebraic variety. But, as the category is $\Lambda$-linear, this should really be an algebraic variety over $\Lambda$. And it seems it shouldn't a priori be an algebraic variety, but it might be more appropriate to, at least a priori, consider it as an analytic variety over $\Lambda$

#### Matthew Ballard (Apr 01 2021 at 14:25):

There is also work in the vein of "objects in a category have norms" like https://arxiv.org/abs/1706.01073. Superficially similar but perhaps more.

#### Peter Scholze (Apr 01 2021 at 14:25):

And this whole liquid stuff exactly allows you to talk about analytic geometry over $\Lambda$

#### Matthew Ballard (Apr 01 2021 at 14:27):

I also remember a talk by Kontsevich where he defined a bridgeland stability condition for a general product of elliptic curves over $\Lambda$ which required the analytic structure of $\Lambda$. That was years ago but there should still be video up.

#### Adam Topaz (Apr 01 2021 at 14:28):

There's a pretty recent lecture series: https://www.youtube.com/watch?v=F8HlMCknSrk

#### Adam Topaz (Apr 01 2021 at 14:28):

Is that what you mean Matt?

#### Matthew Ballard (Apr 01 2021 at 14:29):

Here is a more precise-ish question: what is the right categorification of the mixed hodge structure coming from a semi-stable degeneration? Ie for the smooth fibers we use $D^b(X_t)$. What fits in at $0$ and why?

#### Matthew Ballard (Apr 01 2021 at 14:30):

Is that what you mean Matt?

Not the same talk but most likely the same topic.

#### Peter Scholze (Apr 01 2021 at 14:37):

That's an interesting question! It reminds me of the question "what is the correct category for log-schemes", for which Dmitry Vaintrob has a very nice answer

#### Peter Scholze (Apr 01 2021 at 14:37):

(Related to my early love, almost mathematics etc. ;-) )

#### Matthew Ballard (Apr 01 2021 at 14:38):

I should say it is not mine. Caldararu frequently asks people this.

#### Peter Scholze (Apr 01 2021 at 14:40):

https://arxiv.org/abs/1712.00045

#### Matthew Ballard (Apr 01 2021 at 14:41):

Thanks - I had guessed something like should be the case that the answer should be built from the category of parabolic sheaves on these infinite stacks. It is nice to see a precise answer (even if I know little about almost math :flushed:)

#### Matthew Ballard (Apr 01 2021 at 14:53):

Perhaps it is time to back slowly out of the hole I made in the constructive conversation but it would be nice to see if the ideas presented in Kontsevich's talk and the paper on stability by Haiden-Katzarkov-Kontsevich-Pandit could be recast more generally using condensed math.

#### Patrick Massot (Apr 01 2021 at 15:09):

The symplectic side of mirror symmetry is close to my area and I can tell you the mirror symmetry people will be delighted if they can use anything from condensed mathematics. They love all kinds of fancy mathematics.

#### Peter Scholze (Apr 01 2021 at 15:41):

Well, one spin-off from condensed math -- nuclear modules -- has already found a way into stuff like derived categories of singularities, which I believe has something to do with "matrix factorizations"? https://www.math.k-state.edu/research/m-center/efimov_feb21.pdf

#### Matthew Ballard (Apr 01 2021 at 16:02):

I think Efimov's Theorem 1) on pg 32 is a good way to explain the what/why of nuclear modules to people who know nothing about condensed math (like me). On the left hand side, we have a purely categorical construction for which existence is a serious question. On the right hand side, we have an explicit construction build from the proper dg-algebra itself.

#### Matthew Ballard (Apr 01 2021 at 16:03):

The construction/presentation of such internal homs in related settings has been useful and well-received.

Last updated: May 09 2021 at 23:10 UTC