lessons learned

Stream: condensed mathematics

[Johan Commelin]

Before we start moving towards the 2nd target in this project, I would like to invite everyone involved in the first part to write down observations / lessons learned. This can range from mathematical observations, specific stuff about Lean 3, community patterns, how to run a formalization project, ideas for better automation (please try to be somewhat specific, instead of wishing for Mjolnir).
I think it's good to record this, before we forget the details.

[Peter Scholze]

This is not really on topic for this thread, but it's also "lessons learned". So far, I've had trouble giving a punchline about why condensed sets are better than topological spaces. I think here's one: Topological spaces are meant to capture the idea of spaces with a notion of "nearness" of points. However, they can't handle the idea that "two points are infinitely near, but distinct". But condensed sets can!

[Johan Commelin]

Do you mean that there are separated spaces with such points?

[Johan Commelin]

In my mind, the two points of the "line with the double origin" are infinitely near but distinct. But that's a pathological example.

[Peter Scholze]

Hmm, infinitely near in the sense of "each neighborhood of one contains the other"

[Peter Scholze]

The upshot being that "neighborhoods" weren't the right thing to consider in the first place

[Peter Scholze]

And no, if you add "separated" as an assumption, then this is also ruled out in condensed sets. But the key to all the good algebraic properties is that non-separated quotients like $\mathbb R/\mathbb Q$ or $\ell^2(\mathbb N)/\ell^1(\mathbb N)$ can play along

[Johan Commelin]

Aah, I see. So the two origins are actually quite far apart, in some sense.

[Johan Commelin]

One thing that this first part of LTE made very clear to me, is that we are in dire need of automation that can be handed two objects and the task to build a "canonical" isomorphism between them. (Maybe even of the maps can be given to the tactic.)
I don't have a concrete plan on how to attack this problem. But it is something that deserves attention, and I would want to spend some time thinking about it.

[Adam Topaz]

I remember Scott mentioning a follow your nose tactic that could fill in things like \lambda X, X as data.

[Johan Commelin]

Yes, there is a tactic that allows you to define the Yoneda embedding as $\lambda\hskip-1ex/ Y, \lambda\hskip-1ex/ X, X \longrightarrow Y$. (Here $\lambda\hskip-1ex/$ was a special kind of lambda, for constructing functors, invoking tactics to fill in all the missing pieces.)

[Peter Scholze]

One categorical level down, is there good automation for showing that two numbers are equal? (The one time I played with Lean in one strange lemma (for about an hour, with Johan's guidance), I was merely trying to explain how to rebracket and exchange the order of summing over some finite sets, or so. The two expressions whose equality (as elements of $\mathbb R_{\geq 0}$) was desired seemed indistinguishable to a human reader.)

[Patrick Massot]

Peter Scholze said:

And no, if you add "separated" as an assumption, then this is also ruled out in condensed sets. But the key to all the good algebraic properties is that non-separated quotients like $\mathbb R/\mathbb Q$ or $\ell^2(\mathbb N)/\ell^1(\mathbb N)$ can play along

I didn't get that separation discussion. What does it mean that non-separated quotients can play along?

[Peter Scholze]

They are perfectly well-behaved as condensed sets/abelian groups.

[Peter Scholze]

So for example $\ell^2(\mathbb N)/\ell^1(\mathbb N)$ is a liquid vector space. In all liquid vector spaces, it is about as strange as a torsion abelian group in all abelian groups.

[Peter Scholze]

But as a topological vector space, it's indiscrete and so has no structure at all

[Patrick Massot]

I guess I would need to understand more in what sense they are "perfectly well-behaved", but that's probably a vague question.

[Patrick Massot]

Is it related to your usual example of the missing cokernel (of the identity from discrete reals to reals) or independent?

[Patrick Massot]

I should probably go to bed and think about this tomorrow, but I guess the answer is obvious to you. Say in the $\mathbb{R}/\mathbb Q$ case, is it clear what would be a good profinite S such that $C(S, \mathbb{R})/C(S, \mathbb{Q})$ is interesting?

[Patrick Massot]

And how does it fix the non-separatedness issue?

[David Michael Roberts]

Is that Q with the discrete or subspace topology?

[Peter Scholze]

discrete topology

[Peter Scholze]

It's definitely related to the example of the missing cokernel

[Peter Scholze]

I wouldn't look for any particular $S$ where the value is enlightening, but it's nonzero for all of them

[Peter Scholze]

By the way, here's a fun exercise: Show that the following formula defines a nonzero map of condensed (even liquid) $\mathbb R$-vector spaces $\ell^1(\mathbb N)\to \ell^2(\mathbb N)/\ell^1(\mathbb N)$:

$(x_n)_n\mapsto (x_n \log |x_n|)_n$

So $x\mapsto x \log|x|$ pretends to be linear! The main theorem on liquid vector spaces in some sense gives a bound for how strange maps of this kind can be.

[Peter Scholze]

But Johan should reclaim this thread for its intended discussion! sorry...

[Johan Commelin]

Peter Scholze said:

One categorical level down, is there good automation for showing that two numbers are equal?

It's a good idea to improve this first. There is some automation out there, but it is far from perfect. What we currently have in Lean is ring for elementary expressions in the language of rings. (So it understands * and +, but it doesn't understand $\sum$.) And there is linarith for linear inequalities. And then there is norm_cast (and its friends) that will juggle around canonical inclusions between common types, such as $\N$, $\Z$, $\R$, etc...

[Johan Commelin]

A first easy step would be to teach ring about $\sum$ and $\prod$. But I think there is also room for some tactic on top of these, that combines the lower level tactics. Maybe a variant on tidy.

[Peter Scholze]

I wouldn't be surprised if such algorithms for proving numbers equal could then be adapted to produce canonical isomorphisms. Often that's also about juggling sums and products etc.

[Peter Scholze]

Did you already start a version of the "algebraic hierarchy" one categorical level up? has_add meaning that the category admits finite coproducts (or products? maybe one even wants to say they are equal), has_mul meaning has monoidal structure, etc... it will be a little different, as some of these things are now merely conditions (like has_add), while some become extra structure (for example commutativity of multiplication is data, not just a condition)

[Johan Commelin]

Yes, there is quite a hierarchy for categories by now. Unfortunately they use the slightly more verbose has_products, has_terminal, has_limits_of_shape J, etc... (these are all Props)

[Johan Commelin]

Monoidal categories take the $\otimes$ as extra data of course.

[Damiano Testa]

I really liked Peter's take on this question, about why are condensed sets better than topological spaces. While I do not have a good answer to this, I would like to contribute some ideas about "lessons learned -- formalizing some very specific result".

• Having a list of sorried lemmas was, in my mind, one of the driving forces of this project. This requires planning and reading statements with the caveat that the final version might be slightly different and some glue will be needed.
• The first pass may benefit from a "formalize what you can, possibly with unnecessarily strong assumptions". Linting and streamlining can be done later and will likely be better.
• Dive in: start proving a sorried lemma and you will learn something!