Zulip Chat Archive

Stream: Is there code for X?

Topic: profinite sets


view this post on Zulip Kevin Buzzard (Nov 29 2020 at 14:01):

We don't have them, right? What's the definition? I was taught "a projective limit of finite sets", that sounds like a disaster. "compact and totally disconnected" sounds like a better bet.

view this post on Zulip Adam Topaz (Nov 29 2020 at 14:29):

Totally disconnected compact Hausdorff is easy to write down

view this post on Zulip Adam Topaz (Nov 29 2020 at 14:31):

And I've been (very slowly) adding stuff to make this usable.

view this post on Zulip Adam Topaz (Nov 29 2020 at 14:36):

E.g. only as of a few days ago does mathlib have the fact that the disjoint union of two t2 spaces is t2.

view this post on Zulip Kevin Buzzard (Nov 29 2020 at 14:36):

Should I just make some new file profinite.lean in topology?

view this post on Zulip Adam Topaz (Nov 29 2020 at 14:44):

My inclination is to make the category of profinite sets directly in topology/category/Profinite.lean since we already have the three classes compact_space t2_space and totally_disconnected

view this post on Zulip Reid Barton (Nov 29 2020 at 14:47):

I agree that "projective limit of finite sets" sounds like a potential disaster as a definition but somehow it's the definition we want, so maybe we can create an API around the "totally disconnected compact Hausdorff" definition. For example, we should know that a map to a discrete space is continuous iff it factors through a finite quotient.

view this post on Zulip Adam Topaz (Nov 29 2020 at 14:48):

And we need to prove that Profinite has limits (all limits? or is it just filtered? I don't remember), this way we can construct profinite sets as inverse limits of finite sets

view this post on Zulip Reid Barton (Nov 29 2020 at 14:48):

And we should be able to construct examples as cofiltered limits of finite sets (e.g. build the p-adics from just algebraic data) and know that the original diagram presents the profinite set in this sense

view this post on Zulip Adam Topaz (Nov 29 2020 at 14:51):

By the way, there is a more or less canonical way to write a profinite set as an inverse limit of finites, see e.g. the proof in the stacks project

view this post on Zulip Reid Barton (Nov 29 2020 at 14:53):

that makes sense because as a category, profinite sets is (Ind(FinSet^op))^op

view this post on Zulip Reid Barton (Nov 29 2020 at 14:53):

so it's the opposite of a locally finitely presentable category

view this post on Zulip Adam Topaz (Nov 29 2020 at 14:56):

Does mathlib have Ind?

view this post on Zulip Adam Topaz (Nov 29 2020 at 14:56):

Or Pro?

view this post on Zulip Reid Barton (Nov 29 2020 at 15:00):

Not sure but it's definitely capable of expressing one definition of Ind

view this post on Zulip Reid Barton (Nov 29 2020 at 15:00):

whether that's useful is another matter

view this post on Zulip Reid Barton (Nov 29 2020 at 15:06):

If we unfold the definitions it says that a profinite set is something that we know how to map into finite sets, in a way that respects finite limits. But this only gives us access to the "locale" side, e.g., we know what all the ways to split our profinite set into two clopen subsets are, because they're the maps into {0,1}

view this post on Zulip Reid Barton (Nov 29 2020 at 15:08):

To get the points of the profinite set XX you'd need some Stone duality-like "assignment of an element of SS to every map XSX \to S"

view this post on Zulip Reid Barton (Nov 29 2020 at 15:09):

which I guess is just saying: natural transformations from the one-point space to XX, so maybe it's not too bad

view this post on Zulip Reid Barton (Nov 29 2020 at 15:11):

So in this picture a profinite set is just a finite limit-preserving (covariant) functor from finite sets to sets

view this post on Zulip Reid Barton (Nov 29 2020 at 15:13):

I think Scott did add recently-ish that filtered colimits commute with finite limits, which is the main thing you need to make this workable at all

view this post on Zulip Adam Topaz (Nov 29 2020 at 15:18):

So a profinite set X is identified with the functor sending a finite set F to the set of continuous maps X to F?

view this post on Zulip Kevin Buzzard (Nov 29 2020 at 15:29):

This raises the question as to how important the underlying topological space is. I guess that depends on what you're trying to do.

view this post on Zulip Reid Barton (Nov 29 2020 at 15:36):

The topology is easy to describe too, it should be the coarsest one that makes the maps to finite sets continuous. So we can write down both categories and both functors and if we prove they form an equivalence then we probably have a pretty good API for either side.

view this post on Zulip Reid Barton (Nov 29 2020 at 15:41):

Of course finite sets are sufficiently more annoying than expected that it might actually be technically easier to use topological spaces

view this post on Zulip Reid Barton (Nov 29 2020 at 15:46):

I still like my half-joking suggestion to make Type 0 only allow finite types

view this post on Zulip Adam Topaz (Nov 29 2020 at 15:46):

I think it's a mistake to divorce from topological spaces (even if there is a way to describe the topology). E.g. we will want to ensure that talking about closed subgroups of a profinite group is as easy as possible

view this post on Zulip Reid Barton (Nov 29 2020 at 15:52):

In general I think the answer to choice of representation questions like this has to be to choose both representations

view this post on Zulip Adam Topaz (Nov 29 2020 at 15:55):

Right. For example, we can start like this:

structure Profinite :=
(to_Top : Top)
[is_compact : compact_space to_Top]
[is_t2 : t2_space to_Top]
[is_td : totally_disconnected_space to_Top]

Then construct the functor to FinType \functor Type* that we discussed above and prove it's fully faithful, and describe its essential image as well.

view this post on Zulip Adam Topaz (Nov 29 2020 at 15:56):

Proving that Profinite has finite coproducts should be easy, and proving that it has limits shouldn't be too bad (e.g. the category CompHaus has limits, as can be proved using the equivalence with Compactum)

view this post on Zulip Adam Topaz (Nov 29 2020 at 15:57):

I guess the forgetful functor Profinite \functor CompHaus creates limits?

view this post on Zulip Adam Topaz (Nov 29 2020 at 16:04):

This is another recent addition which will help in proving that finite sets are profinite :rofl:
https://github.com/leanprover-community/mathlib/blob/1f1ba587f272d203a40801c6b21af453f7de6ee3/src/topology/subset_properties.lean#L1305

view this post on Zulip Adam Topaz (Nov 29 2020 at 16:06):

Reid Barton said:

I still like my half-joking suggestion to make Type 0 only allow finite types

What we really need is a whole new proof assistant where everything takes place internally in the topos of condensed sets.

view this post on Zulip Jesse Michael Han (Nov 29 2020 at 18:16):

i'm waiting for the magical day when there's a usable soundness theorem for replaying proofs in {algebraic, coherent, etc} theories in the internal logic of toposes that interpret them

view this post on Zulip Reid Barton (Dec 02 2020 at 15:21):

Adam Topaz said:

Reid Barton said:

I still like my half-joking suggestion to make Type 0 only allow finite types

What we really need is a whole new proof assistant where everything takes place internally in the topos of condensed sets.

I agree this somehow feels very natural. Inductive types are discrete while coinductive types are profinite. Lean doesn't have coinductive types built in, but you can build them using functions and I think this construction produces the right topology when internalized in condensed sets. If you combine inductive and coinductive types then you get things like infinite unions of profinite sets that appear everywhere in the condensed theory, and if you also add in (exact) quotients then you get things that look like arbitrary condensed sets.


Last updated: May 17 2021 at 14:12 UTC