freestyle

Stream: condensed mathematics

[Johan Commelin]

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]

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

[Filippo A. E. Nuccio]

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]

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]

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]

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

[Damiano Testa]

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]

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

[Riccardo Brasca]

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]

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]

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]

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

[Mario Carneiro]

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]

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

[Mario Carneiro]

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

[Mario Carneiro]

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]

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

[Riccardo Brasca]

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]

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]

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]

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]

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]

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]

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]

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

[Filippo A. E. Nuccio]

@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]

(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]

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

[Peter Scholze]

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]

(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]

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

[Peter Scholze]

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]

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]

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

[Peter Scholze]

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

[Adam Topaz]

Oh I see yeah

[Adam Topaz]

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]

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]

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

[Peter Scholze]

sorry, I was away for a second!

[Peter Scholze]

Interesting @ magnitude homology

[Peter Scholze]

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

[Matthew Ballard]

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

[Peter Scholze]

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]

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]

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

[Matthew Ballard]

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]

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

[Adam Topaz]

Is that what you mean Matt?

[Matthew Ballard]

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]

Adam Topaz said:

Is that what you mean Matt?

Not the same talk but most likely the same topic.

[Peter Scholze]

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]

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

[Matthew Ballard]

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

[Peter Scholze]

https://arxiv.org/abs/1712.00045

[Matthew Ballard]

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

Perhaps thinking carefully about it also answers the question I asked.

[Matthew Ballard]

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]

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]

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]

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]

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