Analytic Prop 6.8

Stream: condensed mathematics

[Kevin Buzzard]

(part 1 of 3)

I am finally finding the time to get up to speed with this project. First and foremost I'd like to thank Johan for the phenomenal efforts he has made already, and also thanks to people like Riccardo who seem to have just seamlessly joined the group.

I decided a couple of days ago to stop just looking at section 9 and to re-read the earlier sections to remind myself of what is going on. This was initially going to be some questions about the stuff before and in the proof of Prop 6.8 of analytic.pdf, but it's one of those situations where trying to write down all my questions clearly in a message just made them go away. It seems a bit ridiculous to now just let this knowledge disappear (especially seeing as in 6 months I will have forgotten it) so I am posting a summary of some details of what is going on around 6.8. There is no question (unless I've got the definition of either $S$ or $C(S,\mathbb{Z})$ wrong, which now seems unlikely to me; I'm just being paranoid here because I couldn't find them explicitly written). Everything here is either in the notes directly, or obvious once you know what's going on.

The condensed ring $\mathbb{Z}((T))_r$ (here $0<r<1$ is real) is defined just before 6.8, and it is defined by giving its $S$-valued points. Peter doesn't say what $S$ is, but I assumed "profinite" and convinced myself that this works. Maybe it is all OK for compact Hausdorff but I'm not sure. $\mathbb{Z}((T))_r$ is supposed to be a condensed ring, and I will sketch why this is below (there are no difficulties, I am just writing down more details than is in the paper).

A condensed ring is a functor from profinite sets to rings (satisfying the sheaf axiom for this "finite cover" topology on profinite sets), and if $S$ is profinite then $\mathbb{Z}((T))_r(S)$ is explicitly defined in the pdf as $\cup_{c\geq0}\mathbb{Z}((T))_{r,\leq c}(S)$, where $\mathbb{Z}((T))_{r,\leq c}(S):=\{\sum_{n\in\mathbb{Z}}a_nT^n\,|\,\sum_n|a_n|r^n\le c\}.$ I'll explain what all this means. The $a_n$ are elements of $C(S,\mathbb{Z})$, notation which seems to be first used on p13 and from the calculations there it seems to mean locally constant functions. Of course this is the same as continuous functions if we put the discrete topology on $\mathbb{Z}$, and note also that because $S$ is compact the image of a locally constant $\mathbb{Z}$-valued function is finite, and such a function factors through a map $S_i\to\mathbb{Z}$ with $S_i$ finite and $S\to S_i$ surjective and locally constant. So we have a $\mathbb{Z}$-indexed collection of locally constant functions $a_n:S\to\mathbb{Z}$ and the condition is that for all $s\in S$ the sum $\sum_{n\in\mathbb{Z}}|a_n(s)|r^n$ converges to something $\leq c$, or equivalently that the ennreal-valued function $S\to\R_{\geq0}\cup\{\infty\}$ defined as $\sum|a_n|r^n$ is globally bounded above by $c$. Note that the ennreal-valued function is also only taking finitely many values, so the slightly less precise notation $\sum_{n\in\mathbb{Z}}|a_n|r^n<\infty$ is justified however you want to interpret it. Note also that if $f=\sum a_n T^n\in\mathbb{Z}((T))_r(S)$
then there exists some lower bound $B(f)$ such that $a_n=0$ for $n\leq B(f)$; this is because $f\in\mathbb{Z}((T))_{r,\leq c}(S)$ for some $c$ and if $n$ is sufficiently small (i.e., $<<0$) then already $r^n>c.$

[Kevin Buzzard]

So we now have a clear understanding of the functor. The next thing to check is that it takes values in comm_rings. For both addition and multiplication this boils down to the assertion that if $\sum_{n\in\mathbb{Z}}a_nT^n$ and $\sum_{n\in\mathbb{Z}}b_nT^n$ are in $\mathbb{Z}[[T]][1/T]$ (i.e., have at worst poles at 0) and both series converge absolutely at $T=r$ then so does their sum, difference and product (note $r>0$ so there's no problem with poles). This is standard. Note of course that the bounds can change -- $\mathbb{Z}((T))_{r,\leq c}$ isn't a condensed ring, it's like the reals (a ring) being the union of $[-c,c]$ (not rings) as cc grows.

The next claim is that $\mathbb{Z}((T))_{r,\leq c}$ and $\mathbb{Z}((T))_r$ are sheaves. Results from Condensed.pdf tell us that to check something is a sheaf we just have to check that it sends finite disjoint unions to products, which is completely formal (one only needs to check the case of unions of 0 and 2 things for the usual reasons, but arbitrary finite unions works fine), and that it plays well with surjections, which turns out to be a straightforward calculation: if $S'\to S$ is a continuous surjection of profinite sets then it's obvious that to give a $\mathbb{Z}((T))$-valued function on $S$ is to give a $\mathbb{Z}((T))$-valued function on $S'$ which is constant on pre-images of elements of $S$, and then the only things left to check are that bounds match up and that local constancy of the coefficients matches up.

[Kevin Buzzard]

OK so finally onto 6.8! The claim is that a condensed set "is" a profinite set. More precisely what we're going to do is to put a topology on $X:=\mathbb{Z}((T))_{r,\leq c}(\{*\}),$ show that it's profinite, and then prove that there's a "canonical" isomorphism from $\mathbb{Z}((T))_{r,\leq c}(S)$ to $Cont(S,X),$ where "canonical" means "a bunch of diagrams commute"; more precisely we give an isomorphism between $\mathbb{Z}((T))_{r,\leq c}$ and a sheaf represented by a profinite set. I will now proceed to not check any of the diagrams commute and just write down the isomorphism, because I am still a mathematician at heart and this post is already long enough. Everything is trivial though, one just works in the space of functions from $S$ to $\mathbb{Z}((T))$ to check diagrams commute (i.e. use ext).

So $X$ is just the power series $\sum_{n\in\mathbb{Z}}a_nT^n$ with $\sum_n|a_n|r^n\leq c.$ If $B$ (a negative integer) satisfies $r^B>c$ then $a_n=0$ for $n<B;$ more generally for a fixed $n$ we have $|a_n|r^n\leq c$ so there are only finitely many choices for each $a_n$ coming from an element of $X$; this shows that for any $N$ the image $X_N$ of $X$ under the "truncation" map sending $T^n$ to $0$ if $n\geq N$ is finite, and $X$ is easily checked to be a projective limit of these maps, so it inherits a profinite topology.

Given any map $S\to X$ with this topology we certainly get a power series attached to each element of $S$; the only remaining thing to do (to define the map -- I'm skipping all the proofs that the diagrams commute because they're obvious) is to check that this map is continuous iff all the induced maps $a_n:S\to\mathbb{Z}$ are locally constant. If $S\to X$ is continuous then, by definition of the topology on $X$, the induced "take coefficient of $T^n$" map is a continuous map $S\to\mathbb{Z}$ (the latter having the discrete topology), and is thus locally constant. Conversely if all the "coefficient of $T^n$" maps are locally constant, then note that this does not necessarily imply that the map $S\to X$ is locally constant (a counterexample with $S=\mathbb{Z}_p$ sends $p^nu$ to $T^n$ and $0$ to $0$) but it does imply that all the induced maps $S\to X_N$ are locally constant (there are only finitely many coefficients involved, namely those between $B$ and $N$) and hence continuous, so the map $S\to X$ coming from the fact that $X$ is the limit of the $X_N$ is continuous.

I guess in retrospect what I have written here is what Patrick or Sander would call a roadmap for the proof (which will be straightforward to do in Lean).

[Kevin Buzzard]

Other remarks: (1) I know that this stuff isn't directly what some people are aiming for right now but still it helped me. Maybe some people want to suggest roadmaps for other parts of the document; (2) I posted all this in one post and Zulip failed to process it and it was quite hard to recover (I had to cut and paste from the processed text and then do all the markup again) so beware anyone who wants to post long maths proofs.

[Johan Commelin]

This stuff is certainly on my radar is third_target or fourth_target.

[Johan Commelin]

Thanks for writing up all these details.

[Peter Scholze]

Kevin Buzzard said:

So we have a $\mathbb{Z}$-indexed collection of locally constant functions $a_n:S\to\mathbb{Z}$ and the condition is that for all $s\in S$ the sum $\sum_{n\in\mathbb{Z}}|a_n(s)|r^n$ converges to something $\leq c$, or equivalently that the ennreal-valued function $S\to\R_{\geq0}\cup\{\infty\}$ defined as $\sum|a_n|r^n$ is globally bounded above by $c$. Note that the ennreal-valued function is also only taking finitely many values, so the slightly less precise notation $\sum_{n\in\mathbb{Z}}|a_n|r^n<\infty$ is justified however you want to interpret it.

Thanks for the long post, Kevin! Just a remark that the function can take infinitely many values, and be noncontinuous. The issue is that while all the individual coefficients $a_n$ are locally constant, the whole function is not.

[Kevin Buzzard]

Aah yes -- I realised some aspect of this later on! I'll edit.

[Marc Masdeu]

I've been following the stream without participating, but when I saw this post I thought that this is something that I woudn't mind giving a shot at. Do
you guys (@Johan Commelin and @Kevin Buzzard) think that it's worth trying to formalize at this point, or should be all working on section 9?

[Johan Commelin]

@Marc Masdeu which statement exactly are you thinking of?

[Marc Masdeu]

Prop 6.8 (see the title of the stream!), or Thm 6.9?

[Adam Topaz]

@Marc Masdeu Prop 6.8 is (more-or-less) already in the repo (but stated for Mbar)

[Johan Commelin]

But that variant is certainly welcome.

[Johan Commelin]

We can work on many things in parallel. (My focus will be S9 for now, but eventually I want to do the other stuff as well.)

[Johan Commelin]

@Marc Masdeu were you planning on doing Laurent series first?

[Marc Masdeu]

I guess they'll be needed, right?

[Kevin Buzzard]

Did you see the blueprint Marc? The reason I wrote the above was that I decided to read through all of analytic.pdf again to get my head around some more of the details of the argument (my first reading through it was more superficial, now I am much more motivated to understand some of the details though). Johan makes some comments about Mbar but this claim that it "is" a profinite set can't be in mathlib because the people working on condensed sets haven't yet made a PR with the definition as far as I know (unless I'm behind -- am I?). Certainly @Bhavik Mehta and @Calle Sönne on the discord have been working on the stuff at the beginning of condensed.pdf but, even though this stuff is not really in the blueprint right now, it still seems to me to be accessible in Lean. Maybe I should collect my thoughts about what I think is "ready" (in the sense that the prerequisites are there).

[Bhavik Mehta]

Kevin Buzzard said:

Did you see the blueprint Marc? The reason I wrote the above was that I decided to read through all of analytic.pdf again to get my head around some more of the details of the argument (my first reading through it was more superficial, now I am much more motivated to understand some of the details though). Johan makes some comments about Mbar but this claim that it "is" a profinite set can't be in mathlib because the people working on condensed sets haven't yet made a PR with the definition as far as I know (unless I'm behind -- am I?). Certainly Bhavik Mehta and Calle Sönne on the discord have been working on the stuff at the beginning of condensed.pdf but, even though this stuff is not really in the blueprint right now, it still seems to me to be accessible in Lean. Maybe I should collect my thoughts about what I think is "ready" (in the sense that the prerequisites are there).

The category of profinite sets is in mathlib (https://github.com/leanprover-community/mathlib/blob/master/src/topology/category/Profinite.lean), but it's defined as a compact hausdorff totally disconnected space rather than a projective limit of finite sets - I'm passively thinking about how to get this in Lean though. We're close to having the category of condensed abelian groups in mathlib also

[Kevin Buzzard]

I should catch up on this stuff! 6.8 would be a nice test to see if we had a working definition of a condensed set. Something else which I think would be a good test would be checking that it's possible to prove that condensed abelian groups are an abelian category (the stuff done in the second lecture of condensed.pdf).

[Bhavik Mehta]

I think that before we have the equivalence of CH+TD spaces with projective limits in FinSet, we won't have a great API of profinite set - in particular on a skim read of that argument it uses the latter. On the other hand I'm optimistic that it's possible to prove condensed abelian groups are an abelian category in Lean soon-ish, though I can't estimate how soon

[Marc Masdeu]

I was thinking of working on the liquid project, not on mathlib, so whether it's been PRd or not would be irrelevant. I will definitely start by looking at what's done already and see whether (and where) I could contribute.

[Kevin Buzzard]

My vision about this condensed stuff right now was that the general stuff about profinite sets etc should definitely be in mathlib, and probably the extremely disconnected stuff too, maybe the definition of condensed sets should be in mathlib but this might be up for debate. All this lemma 9.5 stuff should probably be in the liquid repo. Marc a good place to start reading if you want to contribute directly to the challenge is the blueprint.

[Peter Scholze]

@Kevin Buzzard Of course condensed sets ought to be in mathlib ;-)

[Johan Commelin]

@Marc Masdeu we should discuss a bit more about what you would like to work on

[Johan Commelin]

It seems to me like laurent_series would probably be the first step. What do you think?

[Marc Masdeu]

I've also looked at polyhedral_lattice. It seems that the conversation kind of stalled, and if no-one else is looking at that, then I could try it. Laurent series may be fun, but writing them in mathlib-level generality seems daunting (maps on ordered abelian groups?)

[Johan Commelin]

@Marc Masdeu I think several people could work on polyhedral lattices. But it would be good to coordinate with @Damiano Testa. He seemed to have some ideas about how to set up an api.

[Peter Scholze]

Another project that's open (although I think Johan has some work on it?) is to set up some simplicial things; one goal is to formalize 8.19

[Johan Commelin]

Yes, I should get back to it :sweat_smile:

[Johan Commelin]

I somehow am not completely confident that my approach is the best. It would be good to stress test it. I've defined simplicial homology. But I also want geometric realization, Kan complexes, infty cats, Dold-Kan.

[Johan Commelin]

If all of those work, then I'm quite sure the basic api is right.

[Peter Scholze]

Going all the way up to \infty-cats just to test the basic API of simplicial sets seems quite courageous

[Marc Masdeu]

That seems a lot more involved than polyhedral lattices!

[Peter Scholze]

I think Johan has much larger dreams than just formalizing 8.19 :-)

[Johan Commelin]

@Peter Scholze The definition of infty-cats is not that involved, right? I just want to test the waters. Not build a full fledged library (yet).

[Peter Scholze]

OK, that's fair.

[Johan Commelin]

@Marc Masdeu I agree that the simplicial stuff is (for now) orthogonal to the polyhedral lattices.

[Johan Commelin]

In the proof of 9.5 they will meet.

[Damiano Testa]

Hi All, sorry if I have been a little quiet. I am now in my teaching term and have not found time to work on this.

In any case, I am still thinking about formalizing Lemma 9.7 and quite a bit of polyhedral stuff will go into that. I will try to lay out a plan of attack for this and will inform you along the way. This may be a little slow, though!

Of course, I am happy to receive help! So, Marc (or anyone else), if you want to think about this together, I am happy to do so!

In any case, I will probably also post related questions along the way, so you will be able to see my progress! :smile:

[Filippo A. E. Nuccio]

Hi Damiano! I have also been quietly thinking about Lemma 9.7 and got basically nowhere. I was trying to figure out a more combinatorial proof, but failed miserably for the time being. Let's keep in touch, though!

[Calle Sönne]

Bhavik Mehta said:

Kevin Buzzard said:

Did you see the blueprint Marc? The reason I wrote the above was that I decided to read through all of analytic.pdf again to get my head around some more of the details of the argument (my first reading through it was more superficial, now I am much more motivated to understand some of the details though). Johan makes some comments about Mbar but this claim that it "is" a profinite set can't be in mathlib because the people working on condensed sets haven't yet made a PR with the definition as far as I know (unless I'm behind -- am I?). Certainly Bhavik Mehta and Calle Sönne on the discord have been working on the stuff at the beginning of condensed.pdf but, even though this stuff is not really in the blueprint right now, it still seems to me to be accessible in Lean. Maybe I should collect my thoughts about what I think is "ready" (in the sense that the prerequisites are there).

The category of profinite sets is in mathlib (https://github.com/leanprover-community/mathlib/blob/master/src/topology/category/Profinite.lean), but it's defined as a compact hausdorff totally disconnected space rather than a projective limit of finite sets - I'm passively thinking about how to get this in Lean though. We're close to having the category of condensed abelian groups in mathlib also

All the lemmas necessary for the stacks project proof of this are in mathlib (https://stacks.math.columbia.edu/tag/08ZY). I was actually working on this, but got derailed and started working on proving that Profinite is reflective in CompHaus instead (which is more or less done now). I can get back to this once I have cleaned up the code.