Zulip Chat Archive

Stream: condensed mathematics

Topic: condensed sets


Johan Commelin (Jul 14 2021 at 13:34):

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

Johan Commelin (Jul 14 2021 at 13:34):

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 (Jul 14 2021 at 13:35):

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

Johan Commelin (Jul 14 2021 at 13:35):

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

Johan Commelin (Jul 14 2021 at 13:38):

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

Adam Topaz (Jul 14 2021 at 13:41):

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 (Jul 14 2021 at 13:42):

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

Peter Scholze (Jul 14 2021 at 13:42):

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 (Jul 14 2021 at 13:43):

Oh yes of course

Adam Topaz (Jul 14 2021 at 13:51):

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 (Jul 14 2021 at 13:52):

No, not in general.

Peter Scholze (Jul 14 2021 at 13:53):

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

Peter Scholze (Jul 14 2021 at 14:13):

(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 (Jul 14 2021 at 14:17):

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 (Jul 14 2021 at 14:17):

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 (Jul 14 2021 at 14:19):

@Bhavik Mehta can we sheafify yet?

Peter Scholze (Jul 14 2021 at 14:19):

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 (Jul 14 2021 at 14:22):

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 (Jul 14 2021 at 14:37):

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 (Jul 14 2021 at 15:44):

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 (Jul 14 2021 at 15:56):

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

Adam Topaz (Jul 14 2021 at 15:56):

Let me find the construction in stacks

Adam Topaz (Jul 14 2021 at 15:57):

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

Adam Topaz (Jul 14 2021 at 16:00):

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 (Jul 14 2021 at 16:47):

/-!
# 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 (Jul 14 2021 at 16:56):

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

Adam Topaz (Jul 14 2021 at 16:57):

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

Adam Topaz (Jul 14 2021 at 16:58):

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

Adam Topaz (Jul 14 2021 at 17:03):

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 (Jul 14 2021 at 17:05):

CondensedSet as it is won't be a topos

Reid Barton (Jul 14 2021 at 17:07):

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 (Jul 14 2021 at 17:07):

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

Bhavik Mehta (Jul 14 2021 at 17:09):

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 (Jul 14 2021 at 17:10):

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

Reid Barton (Jul 14 2021 at 17:10):

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 (Jul 14 2021 at 17:12):

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

Bhavik Mehta (Jul 14 2021 at 17:17):

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 (Jul 14 2021 at 17:18):

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 (Jul 14 2021 at 17:19):

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 (Jul 14 2021 at 17:20):

What do you suggest changing then?

Reid Barton (Jul 14 2021 at 17:26):

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

Bhavik Mehta (Jul 14 2021 at 17:30):

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

Reid Barton (Jul 14 2021 at 17:32):

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 (Jul 14 2021 at 17:33):

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 (Jul 14 2021 at 17:34):

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

Bhavik Mehta (Jul 14 2021 at 17:38):

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 (Jul 14 2021 at 17:39):

Yes, that sounds right

Bhavik Mehta (Jul 14 2021 at 17:40):

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

Peter Scholze (Jul 14 2021 at 19:23):

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 (Jul 14 2021 at 19:24):

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

Peter Scholze (Jul 14 2021 at 19:48):

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 (Jul 14 2021 at 21:11):

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

Adam Topaz (Jul 14 2021 at 21:25):

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

Adam Topaz (Jul 14 2021 at 21:26):

Also docs#cardinal.is_strong_limit

Johan Commelin (Aug 09 2021 at 06:09):

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 (Aug 09 2021 at 06:16):

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

Johan Commelin (Aug 11 2021 at 08:25):

-- 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 (Aug 11 2021 at 12:42):

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 (Aug 11 2021 at 12:46):

I guess so

Adam Topaz (Aug 11 2021 at 13:00):

By the way, in the definition of M(S,Z((T))r)\mathcal{M}(S,\mathbb{Z}((T))_r) it seems that we're exploiting the fact that Z((T))r[S]c\mathbb{Z}((T))_r[S]_{\le c} is a profinite set and that our condensed objects are sheaves on Profinite. Now what happens for Mp(S)\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 (Aug 11 2021 at 13:01):

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

Johan Commelin (Aug 11 2021 at 13:02):

What do you think would become easier?

Johan Commelin (Aug 11 2021 at 13:02):

More representables?

Adam Topaz (Aug 11 2021 at 13:04):

Yes exactly.

Adam Topaz (Aug 11 2021 at 13:05):

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

Johan Commelin (Aug 11 2021 at 13:06):

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

Adam Topaz (Aug 11 2021 at 13:06):

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

Johan Commelin (Aug 11 2021 at 13:20):

but we only need it once, I think

Johan Commelin (Aug 11 2021 at 13:20):

for this M_p construction

Johan Commelin (Aug 12 2021 at 16:15):

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 M(S,Z((T))r)\mathcal M(S, \Z((T))_r) and Mp(S)\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

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

Johan Commelin (Aug 12 2021 at 16:16):

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 (Aug 12 2021 at 16:18):

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

Johan Commelin (Aug 12 2021 at 16:18):

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

Johan Commelin (Aug 12 2021 at 16:19):

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

Adam Topaz (Aug 12 2021 at 17:33):

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

Adam Topaz (Aug 12 2021 at 17:33):

E.g. can we take a product?

Adam Topaz (Aug 12 2021 at 17:33):

Can we take a tensor product?

Adam Topaz (Aug 12 2021 at 17:34):

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

Johan Commelin (Aug 12 2021 at 17:49):

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 (Aug 12 2021 at 17:49):

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

Adam Topaz (Aug 12 2021 at 17:52):

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

Filippo A. E. Nuccio (Aug 12 2021 at 17:58):

Related to this: on p. 37 Z((T))r[S]\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 Z((T))r\mathbb{Z}((T))_r, no?

Adam Topaz (Aug 12 2021 at 17:59):

yes, I'm fairly certain it's free over Z((T))\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 (Aug 12 2021 at 18:27):

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 (Aug 12 2021 at 18:28):

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

Johan Commelin (Aug 12 2021 at 18:28):

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 (Aug 12 2021 at 18:30):

Adam Topaz said:

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

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

Filippo A. E. Nuccio (Aug 12 2021 at 18:31):

Yes, you're right.

Filippo A. E. Nuccio (Aug 12 2021 at 19:23):

Johan Commelin said:

Of course Z((T))r\Z((T))_r is matheq to M(,Z((T))r)\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 M(,)\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 (Aug 12 2021 at 19:27):

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

Adam Topaz (Aug 12 2021 at 19:49):

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

Johan Commelin (Aug 13 2021 at 05:06):

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

Adam Topaz (Sep 03 2021 at 03:12):

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 (Sep 03 2021 at 03:16):

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.


Last updated: Dec 20 2023 at 11:08 UTC