profinite sets

Stream: Is there code for X?

[Kevin Buzzard]

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]

Totally disconnected compact Hausdorff is easy to write down

[Adam Topaz]

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

[Adam Topaz]

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]

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

[Adam Topaz]

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]

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]

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]

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]

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]

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

[Reid Barton]

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

[Adam Topaz]

Does mathlib have Ind?

[Adam Topaz]

Or Pro?

[Reid Barton]

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

[Reid Barton]

whether that's useful is another matter

[Reid Barton]

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]

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]

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

[Reid Barton]

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

[Reid Barton]

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]

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]

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]

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]

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

[Reid Barton]

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

[Adam Topaz]

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]

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

[Adam Topaz]

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]

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]

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

[Adam Topaz]

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]

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]

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]

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.

[Christian Merten]

I am new to lean, but would like to add the characterization of profinite sets as compact, T2 spaces that have clopen sets as topological basis. The reason for this is, that I would then like to add the category of profinite groups and show the corresponding characterizations there, i.e. a profinite group is an inverse limit of finite discrete groups and equivalently a compact, T2 topological group, that admits a neighborhood basis of the neutral element given by open, normal subgroups. Is there already some process in this direction?

[Johan Commelin]

Welcome! I think most of these things already exist in mathlib, or maybe in slight variants. Probably the category of profinite groups hasn't been defined yet.

[Christian Merten]

Could you give me a hint, where to look for these statements in mathlib?

[Johan Commelin]

These are files on profinite sets:

Mathlib/Topology/Category/Profinite/AsLimit.lean
Mathlib/Topology/Category/Profinite/Basic.lean
Mathlib/Topology/Category/Profinite/CofilteredLimit.lean
Mathlib/Topology/Category/Profinite/EffectiveEpi.lean
Mathlib/Topology/Category/Profinite/Limits.lean
Mathlib/Topology/Category/Profinite/Projective.lean

[Johan Commelin]

There's also stuff on neighborhood basis of 0 in topological groups.

[Christian Merten]

Thank you, I was thinking about something like:

example : (X : TopCat) [T2Space X] [CompactSpace X] :
  TotallyDisconnectedSpace X ↔ IsTopologicalBasis {s | IsClopen s}

and corresponding refined statements for profinite groups.

[Alex J. Best]

@loogle TotallyDisconnectedSpace, TopologicalSpace.IsTopologicalBasis

[Alex J. Best]

Ok idk why the bot doesn't like me but I wanted to link you to https://loogle.lean-fro.org/?q=TotallyDisconnectedSpace%2C+TopologicalSpace.IsTopologicalBasis

[Christian Merten]

Thank you, that is very convenient.

[Alex J. Best]

Which shows two answers for the forward direction of your example (I guess one is strictly more general than the other so one should be deleted?)

[Christian Merten]

Is there some interest in adding the converse, ideally a lemma showing the converse without the compactness assumptions?
Also are there corresponding statements on the level of profinite groups, i.e. that there is a neighborhood basis of the neutral element of open, normal subgroups? I tried to loogle this as well, but I did not find anything (which certainly does not mean anything).

[Alex J. Best]

Oh it looks like we have the converse in the form of docs#totallySeparatedSpace_of_t1_of_basis_clopen combined with docs#compact_t2_tot_disc_iff_tot_sep

[Christian Merten]

Wow, I really need to learn how to navigate mathlib more effectively, thank you!

[Christian Merten]

Is there somewhere a statement along the lines of:

import Mathlib.GroupTheory.Subgroup.Basic
import Mathlib.Topology.Category.TopCat.Basic
import Mathlib.Topology.Algebra.Group.Basic

variable (G : Type u) [Group G] [TopologicalSpace G] [TopologicalGroup G]
  [TotallyDisconnectedSpace G] [CompactSpace G] [T2Space G]

example : Filter.HasBasis (nhds 1)
    (fun s : Subgroup G => IsOpen s.carrier ∧ Subgroup.Normal s)
    (fun s => s.carrier) :=
  sorry

To clarify: I want to state that for a profinite group, the neutral element has a neighborhood basis of open and normal subgroups.

[Adam Topaz]

could you please keep your lines of code a bit shorter? Also, please read #mwe -- your code snippet doesn't include any imports.

[Christian Merten]

Adam Topaz said:

could you please keep your lines of code a bit shorter? Also, please read #mwe -- your code snippet doesn't include any imports.

Sorry, I hope the snippet now meets all requirements.

[Adam Topaz]

No problem at all. It just helps to be able to copy and paste your code, and making a true #mwe helps a lot!

[Adam Topaz]

Presumably you want to use docs#TopologicalGroup ? In any case, my guess is that we don't have such an assertion.

[Christian Merten]

Adam Topaz said:

Presumably you want to use docs#TopologicalGroup ? In any case, my guess is that we don't have such an assertion.

yes, there is a typo in the snippet, instead of two TopologicalSpace G instances, one of them should be TopologicalGroup G.

[Christian Merten]

If I typed up a proof of this, would there be any interest in opening up a PR to mathlib for this? I suppose the proof needs some lemmas on the finiteness of some orbits of the conjugate action of a compact group on its subgroups.

[Adam Topaz]

yes, I think this is definitely worthwhile to have in mathlib.

[Patrick Massot]

Before you start, you can write this statement more compactly as

import Mathlib.Topology.Algebra.Group.Basic

open Topology Filter

variable (G : Type*) [Group G] [TopologicalSpace G] [TopologicalGroup G]
  [TotallyDisconnectedSpace G] [CompactSpace G]

example : (𝓝 (1: G)).HasBasis (fun s : Subgroup G ↦ IsOpen (s : Set G) ∧ s.Normal) (fun s ↦ s)

In particular we never explicitly use Subgroup.carrier.

[Patrick Massot]

This isn't purely cosmetic, you will have to fight Mathlib if you insist on those s.carrier.

[Patrick Massot]

Read Section 7.3 of MIL if needed.

[Christian Merten]

Thanks!

[Christian Merten]

I finally took the time to write a working version of this: https://github.com/leanprover-community/mathlib4/pull/7991. I used some of @Patrick Massot s suggestions about showing finiteness of a quotient (in some other thread here on Zulip). Probably most of this should go to some other file or can be replaced entirely by some library function, any suggestions are very much appreciated.