proetale site on profinite

Stream: condensed mathematics

[Johan Commelin]

@Bhavik Mehta @Calle Sönne can you give me an idea of how far we are from defining the proetale site on profinite sets?

[Johan Commelin]

Once we have it, we can define profinite sets (of course), but I think one of the first things that needs to be done after that, is proving the equivalent "sheaf condition" in terms of extremally disconnected sets.

[Johan Commelin]

There will also be a design question about how to handle condensed abelian groups. Do we want to define them as Ab-valued sheaves or as abelian group objects in Cond(Set) and then define dedicated constructors?

[Johan Commelin]

@Peter Scholze My gut feeling is that it will be useful to know that the category of condensed sets/groups/etc... is defeq a sheaf category, because then you can apply general facts. But as soon as you are "off the ground" you almost always want to work with functors on extremally disconnected spaces. Is that right?

[Peter Scholze]

It's a good question about what the "official" definition of condensed sets ought to be. In fact, it's a question I've been debating a lot with Dustin, and we haven't quite settled it. There are three options, all of which are definitionally sheaf categories (up to the same set-theoretic problems; so maybe I'm really doing pyknotic things here):

a) Take the site of extremally disconnected profinite sets, with covers open covers.
b) Take the site of profinite sets, with covers finite families of jointly surjective maps.
c) Take the site of compact Hausdorff spaces, with covers finite families of jointly surjective maps.

The extremally disconnected profinite sets are exactly the compact projective condensed sets, and it's quite useful to build the theory from compact projectives, so this would be a strong argument for a). The compact Hausdorff spaces are exactly the coherent (=quasicompact + quasiseparated) condensed sets, so this gives an argument for c). But profinite sets are some weird middle ground; they aren't really distinguished by any simple property inside condensed sets.

Still, I am advocating for taking b) as the definition. One reason is that the site in b) has all finite limits (in particular, finite products), and this is generally an extremely useful property to have. The other reason (making it more suitable than c)) is that profinite sets are in many ways much more basic than general compact Hausdorff spaces -- for example, they are pro-(finite sets), and anti-equivalent to Boolean algebras. Relatedly, many of the basic constructions, like the free solid or liquid modules, are easily and uniformly defined for all profinite sets (but not for general compact Hausdorff spaces).

I wouldn't be surprised if condensed sets turn out to be a really good test case for the problem of handling the idea of "the following definitions are canonically equivalent"...

[Johan Commelin]

Another reason for b) is that it's a special case of the pro-etale site, right. To what extent do you think that's a good reason for making it the "official" definition?

[Peter Scholze]

I think that's more of a historical reason

[Johan Commelin]

For proving 9.1, do you think that (a) is the most useful definition?

[Peter Scholze]

I'm not sure. You need the vanishing $H^i(S,\hat{V})=0$ for profinite $S$ (and $i>0$), and I think this is most conveniently proved when your site has all profinite $S$ in it.

[Peter Scholze]

You also need free modules $\mathbb Z[S]$ for arbitrary profinite $S$ a lot

[Johan Commelin]

Ooh, right. So we probably want (a) + (b) and the equivalence between them.

[Peter Scholze]

My internal point of view is that b) is the "official definition", but immediately comes with an equivalence to a), and this equivalence is used to prove lots of facts about b).

[Bhavik Mehta]

I think in a branch I had the definition of the site - if not I had the definition of the covers with some sorried axioms.

[Bhavik Mehta]

I'd taken approach b)

[Bhavik Mehta]

I'll check today how much of the axioms are done - I think most but I could well be misremembering

[Bhavik Mehta]

Updates on this - the axioms were just over half-done, I'm finishing them off right now

[Bhavik Mehta]

https://github.com/leanprover-community/mathlib/blob/proetale/src/topology/category/proetale.lean is the sorry-free definition of the proetale topology on profinites, so it's one line to get the category of condensed sets now and once #5927 is ironed out, another couple of lines to get condensed abelian groups (or maybe pyknotic?)

[Johan Commelin]

Awesome!

[Johan Commelin]

@Bhavik Mehta are you planning to PR it directly to mathlib?

[Bhavik Mehta]

I'll definitely PR the first two sections - I think the third can be generalised and made nicer, so it might be easiest for now to put the third and fourth in the LTE repo since the PR process could take time

[Johan Commelin]

Yes, please push it to LTE in that case.

[Bhavik Mehta]

@[derive category]
def Condensed (A : Type (u+1)) [large_category A] : Type (u+1) := Sheaf.{u} proetale_topology A

example : category.{u+1} (Condensed Ab.{u}) := infer_instance
example : category.{u+1} (Condensed Ring.{u}) := infer_instance

Works too! :)

[Johan Commelin]

That's great!

[Bhavik Mehta]

The notation came out nicer than I expected :D

[Johan Commelin]

So now we can start working on Condensed.S2

[Bhavik Mehta]

Yup, I think the next two goals here are to show the equivalent conditions to be a condensed set here: https://ncatlab.org/nlab/show/condensed+set#definition, and Theorem 2.2 from Condensed.pdf

[Adam Topaz]

Johan Commelin said:

So now we can start working on Condensed.S2

Is that the condensed sphere?

[Johan Commelin]

Bhavik, I guess you've now finally justified the name of this stream! Thanks so much for doing this :grinning:

[Bhavik Mehta]

Bhavik Mehta said:

Yup, I think the next two goals here are to show the equivalent conditions to be a condensed set here: https://ncatlab.org/nlab/show/condensed+set#definition

Is there a maths proof of the equivalence between these two conditions written down somewhere? Or does it just drop out if you play with the definitions a bit more

[Peter Scholze]

Hmm, I think it should be reasonably direct

[Johan Commelin]

Should we go directly for the condition in terms of extremally disconnected sets?

[Peter Scholze]

The idea is that if you have a cover $\{S_i'\}_{i\in I}\to S$ (so $I$ finite) you can use the first part to see that $\mathcal F(\bigsqcup_i S_i')\cong \prod_i \mathcal F(S_i')$, and then reduce the sheaf axiom for $\{S_i'\}_i\to S$ to the cover $\bigsqcup S_i'\to S$. (You will also need to use a similar equality on fibre products, of course.)

[Peter Scholze]

I think it's better to make this intermediate step