condensed sets

Stream: condensed mathematics

[Johan Commelin]

@Bhavik Mehta pushed a definition of condensed sets to condensed/. We have some sorrys again!

[Johan Commelin]

If you feel like hacking on condensed sets, please read the two files, and coordinate with Bhavik if you want to work on some of the sorries.

[Johan Commelin]

There's a bunch of basic API from S2 of Condensed.pdf that people can start working on.

[Johan Commelin]

A good first target might be to show that Cond(Ab) has enough projectives (this will keep us busy for a bit).

[Johan Commelin]

Ooh, and we now have linters that warn about missing docstrings and such: https://github.com/leanprover-community/lean-liquid/runs/3067223382

[Adam Topaz]

I'm confused. How can we write down Condensed A for a category A with no further instances about existence of certain limits?

[Adam Topaz]

Or is the sheaf condition tested in the presheaf category associated to A?

[Peter Scholze]

To say that something is a sheaf, you only need to ask that something is a limit; you don't need to ask that the limit exists and the map to the limit is an isomorphism

[Adam Topaz]

Oh yes of course

[Adam Topaz]

But will this definition (which uses Profinite) be equivalent to the other definitions using ExtrDisc and/or CompHaus if A has no further structure?

[Peter Scholze]

No, not in general.

[Peter Scholze]

You need that A admits certain finite limits (reflexive equalizers)

[Peter Scholze]

(It's actually an interesting and not completely obvious question for which kinds of categories A the usual notion of A-valued sheaves is the "correct" one. Certainly for abelian groups or rings, but not for finitely generated abelian groups, or for fields. Maybe instead of fields, local rings is a better example to keep in mind -- then we know what the correct notion ought to be. In those examples, it's generally better to somehow "repeat the definition internally".)

[Johan Commelin]

But I guess it's not clear that there is one approach that covers all the use cases. Before the condensed formalism, a sheaf of topological rings really needed TopCommRing-valued sheaves. I don't think that could be done internally.

[Bhavik Mehta]

Kevin and I discussed this quite a bit when we were trying to get the right definition for mathlib, we went with https://stacks.math.columbia.edu/tag/00VR since it makes sense for any category A

[Adam Topaz]

@Bhavik Mehta can we sheafify yet?

[Peter Scholze]

It's definitely the standard approach and deserves to be the mathlib-approach. I'm just trying to point out that it may not always give the intended notion (and I don't have it completely clear in my head when it does).

[Bhavik Mehta]

Adam Topaz said:

Bhavik Mehta can we sheafify yet?

Not yet. In my topos repo there's a definition of sheafification for type-valued presheaves on a site (in fact it gives sheafification on Lawvere-Tierney topologies which I then specialise to sites), but there's nothing about moving this to A-valued sheafification on a site.

[Adam Topaz]

My mental definition of a sheaf involves drawing some diagram involving some limits, so my mental typeclass system failed to find the correct instance :smile: . Anyway, I completely agree that this is the right definition.

[Kevin Buzzard]

I have a naive question. Is it always possible to sheafify a presheaf of A's? I'm assuming not, but for example is it even always possible to sheafify a presheaf of topological rings? In the theory of adic spaces one just rejects A such that the presheaf of top rings on Spa(A,A0) isn't a sheaf, rather than attempting to sheafify it

[Adam Topaz]

I think you need certain (co)limits to exist in A to sheafify.

[Adam Topaz]

Let me find the construction in stacks

[Adam Topaz]

stacks#00W1 is for sheaves of sets, but the idea is there.

[Adam Topaz]

Speaking of sheafification, IIRC we need to be able to sheafify to construct the left adjoint of the forgetful functor from Cond Ab to CondSet, right? And this is probably one of the key steps to show that Cond Ab has enough projectives.

[Reid Barton]

/-!
# Condensed sets
Defines the category of condensed sets and condensed structures.
*Strictly speaking* these are pyknotic, but we hope that in the context of Lean's type theory they
serve the same purpose.
-/

def CondensedSet : Type (u+1) := SheafOfTypes.{u} proetale_topology.{u}

I don't think the universes are correct here. It should be sheaves valued in Type (u+1) or something, not Type u.

[Adam Topaz]

I think it's okay? Since Type u : Type (u+1).

[Adam Topaz]

These take values in Type u so the type of all such should be in Type (u + 1)

[Adam Topaz]

Why should they take values in Type (u+1)?

[Adam Topaz]

Oh, I think I understand... If we use SheafOfTypes.{u + 1} proetale_topology.{u} then the morphisms would be in Type (u+1) which agrees with the universe level of Profinite.{u}.

[Reid Barton]

CondensedSet as it is won't be a topos

[Reid Barton]

I think it's the exponentials that are the problem. Basically, it's a bad idea to consider all (pre)sheaves on a large category, and relative to u, Profinite.{u} is a large category.

[Adam Topaz]

Yeah I see. I thought @Bhavik Mehta had some tricks up his sleeves using small or something.

[Bhavik Mehta]

I'm not entirely sure I follow. In Condensed.pdf, we are explicitly taking presheaves over the large category of profinites, and I thought the idea was that we ignore the set-theoretic issues mentioned there

[Bhavik Mehta]

I'm happy to amend if everyone else is convinced though

[Reid Barton]

In any case the "pyknotic" approach intrinsically postulates an additional universe, so either the final result needs to be in Type (u+2) or there needs to be an axiom about Type u already containing an inaccessible (which you couldn't prove if u is 0).

[Adam Topaz]

The discussion here
https://leanprover.zulipchat.com/#narrow/stream/267928-condensed-mathematics/topic/extremally.20disconnected.20sets/near/244951268
is certainly related

[Bhavik Mehta]

Reid Barton said:

CondensedSet as it is won't be a topos

Perhaps I'm missing something, but isn't this the whole point? Condensed sets shouldn't form a topos

[Reid Barton]

There are two possibilities:

• the "condensed" approach is to consider small sheaves on the large category Profinite; it's not described in exactly those terms in Condensed.pdf but AFAIK it's equivalent (at least if you have a universe to work within, maybe). The resulting category of condensed sets is not quite a Grothendieck topos but it has the important properties of one--IIRC it satisfies the Giraud axioms except that it's not locally presentable (only "class-presentable", and in particular still cocomplete and complete).
• the "pyknotic" approach is just to regard Profinite.{u} as being a small category in universe u+1, and take sheaves there, so you definitely get a real u+1-topos. See page 6 of https://arxiv.org/pdf/1904.09966.pdf but in brief, one could say that the "default size" is Type 1 not Type 0.

[Reid Barton]

Bhavik Mehta said:

Reid Barton said:

CondensedSet as it is won't be a topos

Perhaps I'm missing something, but isn't this the whole point? Condensed sets shouldn't form a topos

The comment I quoted claims to be taking the pyknotic approach. But currently CondensedSet isn't either the condensed version or the pyknotic version.

[Bhavik Mehta]

What do you suggest changing then?

[Reid Barton]

I was under the impression that the plan was to use the pyknotic approach, and take sheaves valued in Type (u+1).

[Bhavik Mehta]

I see, I think it's pretty easy to solve then

[Reid Barton]

A variation would be to add a constant in Type u for an inaccessible cardinal and then restrict Profinite to spaces that are smaller than it, but that's probably too radical

[Reid Barton]

The idea would be to avoid having to write Type (u+1) everywhere. Maybe you should just define local notation `TYPE` := Type (u+1) :upside_down:

[Reid Barton]

Or call it Set, then everyone will be equally confused.

[Bhavik Mehta]

Just to clarify, the suggestion is to change the site to be on pretopology (as_small.{u+1} Profinite.{u}), ie Profinite.{u} but viewed as a small category:

instance : small_category.{u+1} (as_small.{u+1} Profinite.{u}) := infer_instance

then the category of presheaves should be _ ⥤ Type (u+1)?

[Reid Barton]

Yes, that sounds right

[Bhavik Mehta]

Got it. I think the only real barrier to implementing this is some missing instances on as_small.

[Peter Scholze]

As I've said before, I'm happy with you going the pyknotic way. But maybe one could also call it pyknotic in the Lean code then? It would seem more fair to me.

[Peter Scholze]

(And "small sheaves = the thing defined in [Condensed]" does not need any universes/inaccessibles)

[Peter Scholze]

I'm starting to be curious what your experience will be: whether it's more trouble keeping track of universes as in the pyknotic way, or occasionally having to prove smallness, as in the condensed way. Would you have enough stuff about cardinals in mathlib to talk about $\kappa$-small condensed sets for a strong limit $\kappa$, say? (and have this be a small category)

[Johan Commelin]

I doubt that we have the definition of strong limit $\kappa$, but otherwise we have some API around cardinals.

[Adam Topaz]

we have docs#cardinal.is_inaccessible but I've never even come close to using that part of mathlib

[Adam Topaz]

Also docs#cardinal.is_strong_limit

[Johan Commelin]

We have

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

due to the valiant efforts of @Bhavik Mehta. How far are we from showing that it is a preadditive category?

[Johan Commelin]

I pushed a stub to master in consendes/ab.lean.

[Johan Commelin]

-- TODO (BM): put this in mathlib (it's already in a mathlib branch with API)
def category_theory.functor.preserves_terminal (X : Profinite.{u}ᵒᵖ ⥤ Type u) : Prop := sorry
-- TODO (BM): put this in mathlib (it's already in a mathlib branch with API)
def category_theory.functor.preserves_binary_products (X : Profinite.{u}ᵒᵖ ⥤ Type u) : Prop := sorry

@Bhavik Mehta can you please tell me which branch? Can you use some help with getting it into mathlib?

[Adam Topaz]

I think the more pressing issue with the stuff in condensed/* is to get the universe levels correct... In the other code I've written the easiest approach I found was to use (as_small.{u+1} Profinite.{u})\op \func Type (u+1). If I understand correctly, we're still missing a way to transport a Grothendieck topology along an equivalence of categories?

[Johan Commelin]

I guess so

[Adam Topaz]

By the way, in the definition of $\mathcal{M}(S,\mathbb{Z}((T))_r)$ it seems that we're exploiting the fact that $\mathbb{Z}((T))_r[S]_{\le c}$ is a profinite set and that our condensed objects are sheaves on Profinite. Now what happens for $\mathcal{M}_p(S)$? The analogous members of the filtration are compact Hausdorff. Are we sure we don't want to build condensed objects as sheaves on CompHaus?

[Johan Commelin]

We can still view X : CompHaus as a condensed set, right?

[Johan Commelin]

What do you think would become easier?

[Johan Commelin]

More representables?

[Adam Topaz]

Yes exactly.

[Adam Topaz]

It doesn't really matter if we have a good complete API, of course.

[Johan Commelin]

So in the end the question is: which definitions are best for setting up the API?
I don't know the answer

[Adam Topaz]

I'm just thinking we may want to generalize ProfinitelyFilteredPseudoNormedGroup to CompHauslyFilteredPseudoNormedGroup

[Johan Commelin]

but we only need it once, I think

[Johan Commelin]

for this M_p construction

[Johan Commelin]

Adam Topaz said:

I'm just thinking we may want to generalize ProfinitelyFilteredPseudoNormedGroup to CompHauslyFilteredPseudoNormedGroup

Actually, profinitely_filtered_pseudo_normed_group could easily extend comp_haus_filtered_pseudo_normed_group. That would just be a few lines.
And then we need something like

def Cond_Ab_mk_of_chfpng (A : Type*) [comp_haus_filtered_pseudo_normed_group A] :
  Condensed Ab :=
sorry

Which would work for profinitely filtered png's as well, by typeclass inference.

We can then apply this constructor to $\mathcal M(S, \Z((T))_r)$ and $\mathcal M_p(S)$.

I'm not sure whether we want to make it functorial in general. We will only need functoriality once, I think. Because we need a "quotient" map

$$\mathcal M(S, \Z((T))_r) \to \mathcal M_p(S)$$

[Johan Commelin]

This quotient map is the content of prop 7.2 of Analytic.pdf. We'll need to fill in a bunch of details there.

[Johan Commelin]

@Adam Topaz @Filippo A. E. Nuccio Are you also defining $\Z((T))_r$? Or only the $\mathcal M$ spaces?

[Johan Commelin]

Of course $\Z((T))_r$ is matheq to $\mathcal M(*, \Z((T))_r)$. But I don't think that's a nice lean def.

[Johan Commelin]

As soon as we have a def of $\Z((T))_r$ together with its filtration, someone can start looking into prop 7.2.

[Adam Topaz]

What sort of structure do we have on pfpsn's?

[Adam Topaz]

E.g. can we take a product?

[Adam Topaz]

Can we take a tensor product?

[Adam Topaz]

Because presumably we should define $\mathbb{Z}((T))_r$ as a profinitely-filtered-pseudo-normed-ring

[Johan Commelin]

It's not clear to me that we need the ring structure, but we probably do...
The reason it's not clear to me, is that the challenge is about an Ext in condensed abelian groups, not in condensed R-modules.

[Johan Commelin]

So maybe we don't need condensed rings for this challenge.

[Adam Topaz]

We don't need the $\mathbb{Z}[T^{-1}]$-module structure?

[Filippo A. E. Nuccio]

Related to this: on p. 37 $\mathbb{Z}((T))_r[S]$ is said to be a free module: I guess it is meant to be a free module over the ring $\mathbb{Z}((T))_r$, no?

[Adam Topaz]

yes, I'm fairly certain it's free over $\mathbb{Z}((T))$, but that doesn't necessarily matter if we're only interested in the structure as a (condensed) abelian group.

[Filippo A. E. Nuccio]

Well, I am just slightly worried that in Thm 6.9 (ii) (or Prop 7.2 Johan was referring to) it might be useful to have the language of ideals at our disposal to speak about "principal" kernels. But I confess I haven't dug in the details of the proof yet, you certainly have a clearer picture.

[Johan Commelin]

Well, if it turns out we need the ring structure, then we just add it.

[Johan Commelin]

I mean, we need the ring structure. But I don't know whether we need it as condensed ring. Certainly Prop 7.2 as stated is a bunch of computations about ordinary rings.

[Johan Commelin]

Adam Topaz said:

We don't need the $\mathbb{Z}[T^{-1}]$-module structure?

I think we do need this. But that might boil down to explicitly recording the endomorphism through which $T^{-1}$ acts. Just like we had normed_with_aut in the first part of LTE.

[Filippo A. E. Nuccio]

Yes, you're right.

[Filippo A. E. Nuccio]

Johan Commelin said:

Of course $\Z((T))_r$ is matheq to $\mathcal M(*, \Z((T))_r)$. But I don't think that's a nice lean def.

I was thinking about this again: do you mean that $\mathcal M(\ast,\dagger)$ is the functor of "taking global sections of the condensed ab. group $\dagger$, and that, for fixed $\dagger$ it has the same value on $\ast$ as $\dagger$?

[Johan Commelin]

In this case, I just meant the very mundane observation that for $S = \text{pt} = *$ the space $\mathcal M(S, \Z((T))_r)$ is canonically isom to $\Z((T))_r$. I haven't thought too much about generalizing the second argument to some arbitrary $\dagger$.

[Adam Topaz]

Presumably we can give a construction which takes any profinitely-filtered-pseudo-normed-ring comphausly-filtered-pseudo-normed-ring $R$ and constructs $\mathcal{M}(S,R)$.

[Johan Commelin]

yes, I think that works. But for the $\R$-version we'll need type aliases for $\R_{\ell^p}$ or something like that. I'm not sure it is worth it.

[Adam Topaz]

A step toward fixing the universe issues: I just pushed a definition of the pro-etale topology on as_small Profinite in https://github.com/leanprover-community/lean-liquid/blob/master/src/condensed/proetale_site_as_small.lean

The code that @Bhavik Mehta wrote works almost exactly the same, once the correct concrete_category instances were activated. The most annoying part was proving that as_small Profinite has pullbacks, which is still a bit of a mess (and should be generalized somehow anyway), which can be found in a more general setting in for_mathlib/pulllbacks.

[Adam Topaz]

A much better approach would be to build a construction which transports a grothendieck topology across an equivalence, but the trouble I had transporting existence of pullbacks along an equivalence makes me think that this will be a very VERY annoying construction.