Zulip Chat Archive

Stream: condensed mathematics

Topic: freestyle


view this post on Zulip 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\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) Spec(Z)\mathrm{Spec}(\Z) with specializations to classical Hodge theory and pp-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!

view this post on Zulip Patrick Massot (Apr 01 2021 at 07:14):

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

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

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

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

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

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

view this post on Zulip Riccardo Brasca (Apr 01 2021 at 08:21):

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

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

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

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

view this post on Zulip Riccardo Brasca (Apr 01 2021 at 10:57):

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

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

view this post on Zulip Riccardo Brasca (Apr 01 2021 at 10:58):

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

view this post on Zulip Mario Carneiro (Apr 01 2021 at 10:59):

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

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

view this post on Zulip Mario Carneiro (Apr 01 2021 at 11:02):

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

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

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

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

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

view this post on Zulip Riccardo Brasca (Apr 01 2021 at 11:39):

I got that "Formulate a liquid Hodge theory that works over (some form of) Spec(Z)\mathrm{Spec}(\Z) with specializations to classical Hodge theory and pp-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!

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

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

view this post on Zulip Peter Scholze (Apr 01 2021 at 11:45):

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

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

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

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

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

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

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

view this post on Zulip Peter Scholze (Apr 01 2021 at 13:53):

In mirror symmetry, there's this weird thing that you have to replace the coefficients Z\mathbb Z by this funny Novikov ring. Somehow exactly the same happens in the liquid story: It can't be defined directly over Z\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...

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

view this post on Zulip Adam Topaz (Apr 01 2021 at 13:56):

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

view this post on Zulip Peter Scholze (Apr 01 2021 at 13:56):

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

view this post on Zulip Adam Topaz (Apr 01 2021 at 13:56):

Oh I see yeah

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

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

view this post on Zulip Matthew Ballard (Apr 01 2021 at 14:12):

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

view this post on Zulip Peter Scholze (Apr 01 2021 at 14:12):

sorry, I was away for a second!

view this post on Zulip Peter Scholze (Apr 01 2021 at 14:15):

Interesting @ magnitude homology

view this post on Zulip Peter Scholze (Apr 01 2021 at 14:23):

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

view this post on Zulip Matthew Ballard (Apr 01 2021 at 14:24):

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

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

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

view this post on Zulip Peter Scholze (Apr 01 2021 at 14:25):

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

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

view this post on Zulip Adam Topaz (Apr 01 2021 at 14:28):

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

view this post on Zulip Adam Topaz (Apr 01 2021 at 14:28):

Is that what you mean Matt?

view this post on Zulip 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 Db(Xt)D^b(X_t). What fits in at 00 and why?

view this post on Zulip Matthew Ballard (Apr 01 2021 at 14:30):

Adam Topaz said:

Is that what you mean Matt?

Not the same talk but most likely the same topic.

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

view this post on Zulip Peter Scholze (Apr 01 2021 at 14:37):

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

view this post on Zulip Matthew Ballard (Apr 01 2021 at 14:38):

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

view this post on Zulip Peter Scholze (Apr 01 2021 at 14:40):

https://arxiv.org/abs/1712.00045

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

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

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

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

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

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

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