Zulip Chat Archive

Stream: condensed mathematics

Topic: Analytic Prop 6.8


view this post on Zulip Kevin Buzzard (Jan 26 2021 at 16:00):

(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 SS or C(S,Z)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 Z((T))r\mathbb{Z}((T))_r (here 0<r<10<r<1 is real) is defined just before 6.8, and it is defined by giving its SS-valued points. Peter doesn't say what SS is, but I assumed "profinite" and convinced myself that this works. Maybe it is all OK for compact Hausdorff but I'm not sure. Z((T))r\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 SS is profinite then Z((T))r(S)\mathbb{Z}((T))_r(S) is explicitly defined in the pdf as c0Z((T))r,c(S)\cup_{c\geq0}\mathbb{Z}((T))_{r,\leq c}(S), where Z((T))r,c(S):={nZanTnnanrnc}.\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 ana_n are elements of C(S,Z)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 Z\mathbb{Z}, and note also that because SS is compact the image of a locally constant Z\mathbb{Z}-valued function is finite, and such a function factors through a map SiZS_i\to\mathbb{Z} with SiS_i finite and SSiS\to S_i surjective and locally constant. So we have a Z\mathbb{Z}-indexed collection of locally constant functions an:SZa_n:S\to\mathbb{Z} and the condition is that for all sSs\in S the sum nZan(s)rn\sum_{n\in\mathbb{Z}}|a_n(s)|r^n converges to something c\leq c, or equivalently that the ennreal-valued function SR0{}S\to\R_{\geq0}\cup\{\infty\} defined as anrn\sum|a_n|r^n is globally bounded above by cc. Note that the ennreal-valued function is also only taking finitely many values, so the slightly less precise notation nZanrn<\sum_{n\in\mathbb{Z}}|a_n|r^n<\infty is justified however you want to interpret it. Note also that if f=anTnZ((T))r(S)f=\sum a_n T^n\in\mathbb{Z}((T))_r(S)
then there exists some lower bound B(f)B(f) such that an=0a_n=0 for nB(f)n\leq B(f); this is because fZ((T))r,c(S)f\in\mathbb{Z}((T))_{r,\leq c}(S) for some cc and if nn is sufficiently small (i.e., <<0<<0) then already rn>c.r^n>c.

view this post on Zulip Kevin Buzzard (Jan 26 2021 at 16:00):

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 nZanTn\sum_{n\in\mathbb{Z}}a_nT^n and nZbnTn\sum_{n\in\mathbb{Z}}b_nT^n are in Z[[T]][1/T]\mathbb{Z}[[T]][1/T] (i.e., have at worst poles at 0) and both series converge absolutely at T=rT=r then so does their sum, difference and product (note r>0r>0 so there's no problem with poles). This is standard. Note of course that the bounds can change -- Z((T))r,c\mathbb{Z}((T))_{r,\leq c} isn't a condensed ring, it's like the reals (a ring) being the union of [c,c][-c,c] (not rings) as cc grows.

The next claim is that Z((T))r,c\mathbb{Z}((T))_{r,\leq c} and Z((T))r\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 SSS'\to S is a continuous surjection of profinite sets then it's obvious that to give a Z((T))\mathbb{Z}((T))-valued function on SS is to give a Z((T))\mathbb{Z}((T))-valued function on SS' which is constant on pre-images of elements of SS, and then the only things left to check are that bounds match up and that local constancy of the coefficients matches up.

view this post on Zulip Kevin Buzzard (Jan 26 2021 at 16:00):

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:=Z((T))r,c({}),X:=\mathbb{Z}((T))_{r,\leq c}(\{*\}), show that it's profinite, and then prove that there's a "canonical" isomorphism from Z((T))r,c(S)\mathbb{Z}((T))_{r,\leq c}(S) to Cont(S,X),Cont(S,X), where "canonical" means "a bunch of diagrams commute"; more precisely we give an isomorphism between Z((T))r,c\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 SS to Z((T))\mathbb{Z}((T)) to check diagrams commute (i.e. use ext).

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

Given any map SXS\to X with this topology we certainly get a power series attached to each element of SS; 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 an:SZa_n:S\to\mathbb{Z} are locally constant. If SXS\to X is continuous then, by definition of the topology on XX, the induced "take coefficient of TnT^n" map is a continuous map SZS\to\mathbb{Z} (the latter having the discrete topology), and is thus locally constant. Conversely if all the "coefficient of TnT^n" maps are locally constant, then note that this does not necessarily imply that the map SXS\to X is locally constant (a counterexample with S=ZpS=\mathbb{Z}_p sends pnup^nu to TnT^n and 00 to 00) but it does imply that all the induced maps SXNS\to X_N are locally constant (there are only finitely many coefficients involved, namely those between BB and NN) and hence continuous, so the map SXS\to X coming from the fact that XX is the limit of the XNX_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).

view this post on Zulip Kevin Buzzard (Jan 26 2021 at 16:05):

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.

view this post on Zulip Johan Commelin (Jan 26 2021 at 16:05):

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

view this post on Zulip Johan Commelin (Jan 26 2021 at 16:05):

Thanks for writing up all these details.

view this post on Zulip Peter Scholze (Jan 26 2021 at 16:12):

Kevin Buzzard said:

So we have a Z\mathbb{Z}-indexed collection of locally constant functions an:SZa_n:S\to\mathbb{Z} and the condition is that for all sSs\in S the sum nZan(s)rn\sum_{n\in\mathbb{Z}}|a_n(s)|r^n converges to something c\leq c, or equivalently that the ennreal-valued function SR0{}S\to\R_{\geq0}\cup\{\infty\} defined as anrn\sum|a_n|r^n is globally bounded above by cc. Note that the ennreal-valued function is also only taking finitely many values, so the slightly less precise notation nZanrn<\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 ana_n are locally constant, the whole function is not.

view this post on Zulip Kevin Buzzard (Jan 26 2021 at 17:41):

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

view this post on Zulip Marc Masdeu (Jan 29 2021 at 16:18):

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?

view this post on Zulip Johan Commelin (Jan 29 2021 at 16:38):

@Marc Masdeu which statement exactly are you thinking of?

view this post on Zulip Marc Masdeu (Jan 29 2021 at 16:41):

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

view this post on Zulip Adam Topaz (Jan 29 2021 at 16:43):

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

view this post on Zulip Johan Commelin (Jan 29 2021 at 16:43):

But that variant is certainly welcome.

view this post on Zulip Johan Commelin (Jan 29 2021 at 16:44):

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

view this post on Zulip Johan Commelin (Jan 29 2021 at 16:45):

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

view this post on Zulip Marc Masdeu (Jan 29 2021 at 17:11):

I guess they'll be needed, right?

view this post on Zulip Kevin Buzzard (Jan 29 2021 at 17:31):

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

view this post on Zulip Bhavik Mehta (Jan 29 2021 at 17:37):

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

view this post on Zulip Kevin Buzzard (Jan 29 2021 at 17:39):

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

view this post on Zulip Bhavik Mehta (Jan 29 2021 at 17:41):

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

view this post on Zulip Marc Masdeu (Jan 29 2021 at 17:44):

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.

view this post on Zulip Kevin Buzzard (Jan 29 2021 at 18:59):

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.

view this post on Zulip Peter Scholze (Jan 29 2021 at 20:43):

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

view this post on Zulip Johan Commelin (Feb 01 2021 at 09:48):

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

view this post on Zulip Johan Commelin (Feb 01 2021 at 09:49):

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

view this post on Zulip Marc Masdeu (Feb 02 2021 at 15:31):

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

view this post on Zulip Johan Commelin (Feb 02 2021 at 15:32):

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

view this post on Zulip Peter Scholze (Feb 02 2021 at 15:43):

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

view this post on Zulip Johan Commelin (Feb 02 2021 at 15:52):

Yes, I should get back to it :sweat_smile:

view this post on Zulip Johan Commelin (Feb 02 2021 at 15:53):

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.

view this post on Zulip Johan Commelin (Feb 02 2021 at 15:54):

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

view this post on Zulip Peter Scholze (Feb 02 2021 at 15:58):

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

view this post on Zulip Marc Masdeu (Feb 02 2021 at 15:58):

That seems a lot more involved than polyhedral lattices!

view this post on Zulip Peter Scholze (Feb 02 2021 at 15:58):

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

view this post on Zulip Johan Commelin (Feb 02 2021 at 16:01):

@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).

view this post on Zulip Peter Scholze (Feb 02 2021 at 16:02):

OK, that's fair.

view this post on Zulip Johan Commelin (Feb 02 2021 at 16:02):

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

view this post on Zulip Johan Commelin (Feb 02 2021 at 16:03):

In the proof of 9.5 they will meet.

view this post on Zulip Damiano Testa (Feb 02 2021 at 17:01):

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:

view this post on Zulip Filippo A. E. Nuccio (Feb 02 2021 at 18:59):

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!

view this post on Zulip Calle Sönne (Feb 02 2021 at 21:31):

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.


Last updated: May 09 2021 at 16:20 UTC