## Stream: Is there code for X?

### Topic: profinite sets

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

#### Adam Topaz (Nov 29 2020 at 14:29):

Totally disconnected compact Hausdorff is easy to write down

#### Adam Topaz (Nov 29 2020 at 14:31):

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

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

#### Kevin Buzzard (Nov 29 2020 at 14:36):

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

#### 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

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

#### 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

#### 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

#### 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

#### Reid Barton (Nov 29 2020 at 14:53):

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

#### Reid Barton (Nov 29 2020 at 14:53):

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

#### Adam Topaz (Nov 29 2020 at 14:56):

Does mathlib have Ind?

Or Pro?

#### Reid Barton (Nov 29 2020 at 15:00):

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

#### Reid Barton (Nov 29 2020 at 15:00):

whether that's useful is another matter

#### 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}

#### Reid Barton (Nov 29 2020 at 15:08):

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

#### Reid Barton (Nov 29 2020 at 15:09):

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

#### 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

#### 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

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

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

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

#### 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

#### Reid Barton (Nov 29 2020 at 15:46):

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

#### 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

#### 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

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

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

#### Adam Topaz (Nov 29 2020 at 15:57):

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

#### 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

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

#### 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

#### Reid Barton (Dec 02 2020 at 15:21):

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