Categories of compact Hausdorff spaces

Stream: mathlib4

[Dagur Asgeirsson]

There are now four different important subcategories of compact Hausdorff spaces in Mathlib (CompHaus, Profinite, Stonean, and LightProfinite). They are all used for similar purposes (being the defining site for variants of condensed sets). This leads to quite a lot of code repetition and I'm thinking about a refactor where their definitions are unified by defining a structure CompHausLike as follows

import Mathlib.Topology.Category.TopCat.Basic

universe u

open CategoryTheory

variable (P : TopCat.{u} → Prop)

/-- The type of Compact Hausdorff topological spaces satisfying an additional property `P`. -/
structure CompHausLike where
  /-- The underlying topological space of an object of `CompHausLike P`. -/
  toTop : TopCat
  /-- The underlying topological space is compact. -/
  [is_compact : CompactSpace toTop]
  /-- The underlying topological space is T2. -/
  [is_hausdorff : T2Space toTop]
  /-- The underlying topological space satisfies P. -/
  prop : P toTop

The current definitions of Stonean and Profinite are essentially this. For LightProfinite, it would be a slightly bigger refactor, but I think we have enough to prove the relevant equivalence of categories.

The advantage is of course to be able to prove things for all four categories at once.

Is this a sensible design decision?

[Dagur Asgeirsson]

I experiment with copying some stuff from CompHaus/Basic  using this approach in #12930

[Johan Commelin]

Is it possible to set up the API for categories with a distinguished fully faithful functor to CompHaus? That would be math equivalent to what you propose. But might leave a bit more flexibility in the definitions...

[Johan Commelin]

But maybe using the fully faithful functor will be annoying?

[Dagur Asgeirsson]

The issue with the general fully faithful functor approach is that the objects are too abstract. I want my objects to be topological spaces and my morphisms to be continuous maps.

Another option would be to use the FullSubcategory API, but that approach would still involve developing some specialised API for full subcategories of TopCat or CompHaus.

The application I have in mind is to generalise most of what is done in the file Condensed/Discrete/LocallyConstant in #12185 to CompHausLike P where P is stable under forming finite coproducts (which we have a very explicit construction for in these topological categories). Then deduce the result about discrete condensed sets and light condensed sets at once.

[Dagur Asgeirsson]

More generally, we could get rid of all the repetition in the files CompHaus/Limits, Profinite/Limits etc. and make general constructions for when P is stable under the formation of these limits.

[Dagur Asgeirsson]

I've started the refactor at #12930 and it breaks surprisingly little for CompHaus, Profinite and Stonean. I'll continue and see how it goes with the limits and LightProfinite, and report back here

[Kevin Buzzard]

Could you mimic how concrete categories are set up?

[Dagur Asgeirsson]

These CompHausLike are meant to be full subcatgeories of CompHaus and not just abstract categories with a forgetful functor to CompHaus. As Johan said, it's mathematically equivalent to set up the API for categories with a distinguished fully faithful functor to CompHaus, but I explained above why I don't want that.

This approach is also closer to how I think about these categories. For example: why does Profinite have pullbacks? Well, it's because taking the pullback in CompHaus, or TopCat, or whatever, (i.e. forming the subset of the product of those pairs whose coordinates are mapped to the same thing) preserves the property of being totally disconnected. Now we can just do this once for a general CompHausLike P for which P is preserved by forming pullbacks, and not have the whole API for CompHaus.pullback, Profinite.pullback, LightProfinite.pullback, etc.

[Adam Topaz]

I'm not sure hat I agree. If you have some predicate P on a the objects of C, you can easily obtain the fully faithful functor from the associated full subcategory. And in order to show that this functor creates limits of a certain shape it quite quickly boils down to showing that P preserves such limits. So I'm not convinced using the approach above would simplify things in any meaningful way. Also, I can imagine having categories which are CompHausLike which are not given by a predicate. For example, docs#Compactum or Pro(FinType).

[Dagur Asgeirsson]

I don't want to define CompHausLike as a property of categories. I want to define the categories CompHaus, Profinite, Stonean etc. as CompHausLike P for the relevant predicate P

[Adam Topaz]

But why can't those just be full subcategories?

[Dagur Asgeirsson]

The examples you mention should then have equivalences to CompHaus and Profinite

[Dagur Asgeirsson]

I have just found the FullSubcategory API a bit awkward to work with. For example, we don't define CompHaus as a FullSubcategory of TopCat now. We define a structure CompHaus and give it the induced category instance. Profinite and Stonean are defined in a similar way. My point is that these categories share many properties but it's hard to argue about them all at once.

[Dagur Asgeirsson]

Would you rather suggest defining them all as FullSubcategorys of TopCat, and prove theorems about such full subcategories?

[Adam Topaz]

Dagur Asgeirsson said:

My point is that these categories share many properties but it's hard to argue about them all at once.

That's a perfectly fair point and I agree.

Dagur Asgeirsson said:

Would you rather suggest defining them all as FullSubcategorys of TopCat, and prove theorems about such full subcategories?

To be honest, I don't know what I want to suggest yet. The key points I think we should address are as follows:

• First, as I said above, I agree that we need to have some principled way to reason about all such categories.
• Second, I also think that we might want to abstract away CompHaus itself! By this I mean making some abstraction that either captures CompHaus up to equivalence, or even better, captures only the essential ingredients for condensed math.

[Dagur Asgeirsson]

The second point is interesting, but I'm almost going in the opposite direction here. At least in #12185 (which is what led me to think about this), where I prove that the S-valued points of a discrete condensed set X are the locally constant maps S \to X, I heavily use the definitional properties of finite coproducts in CompHaus. I want to change every occurence of CompHaus in that file to CompHausLike P where P is preserved by taking finite coproducts, and deduce the same thing for condensed and light condensed sets at once.

[Dagur Asgeirsson]

What do you have in mind when you say the "essential ingredients" for condensed math? We also need to keep in mind light condensed sets

[Adam Topaz]

yeah the light stuff complicates things, but I'm sure there is some natural abstraction from general stone duality. Maybe we should invite @Sam van G to the discussion?

[Sam van G]

Thanks for the invitation and sorry for the delay :) I’m not completely sure what the question is so just some loose remarks. As you know, (light) profinite sets are dually equivalent to (countable) Boolean algebras, but I would expect to encounter the same problem on the other side of the duality. Stone duality for non-zero-dimensional spaces is an interesting field with active research. Not sure if it will be immediately useful here.
From just reading the discussion above, it sounds like the FullSubcategory API is what mostly needs work? I haven’t had to work with it myself but I have generally found categories in Mathlib more difficult to work with than, say, algebra or topology, so I understand why some are hesitant.

[Adam Topaz]

I guess one concrete question I'm thinking of is whether Profinite can be distinguished in purely categorical terms within CompHaus? I know how to do it if we have not just the category CompHaus but also the forgetful functor CompHaus -> Type. Any ideas?

[Johan Commelin]

You can distinguish the terminal object, hence finite sets. So you can look at all finite quotients of a space, and take the limit of that diagram. And if the map to that limit is an iso, then it must have been a profinite space.

[Adam Topaz]

Is the compatibility with the coherent topologies clear from this description?

[Adam Topaz]

One observation is that a finite quotient is "the same thing" as a (finitely) extensive cover.

[Kevin Buzzard]

What is the problem with the topologies in Johan's argument?

[Sam van G]

Within CompHaus, the objects that are in Profinite are exactly those that are filtered limits of diagrams of finite objects (where you can choose any definition of finite that you like, for example finite coproducts of terminal objects). This is equivalent to what Johan said except that his description builds the space in a specific way, by looking at the diagram of all of its finite quotients. In my experience, when proving things -on paper- about profinite spaces, depending on the context, in some situations you want to use that specific diagram, in other situations you want to say "there is some filtered diagram that can build it and I don't care what it looks like".

[Adam Topaz]

It's not that there's a problem with Johan's argument, but with this point of view it's not clear to me how to make some of the arguments in condensed mathematics work. For example if you have some comphaus X, you get a natural map from X to the limit of all its finite quotients, which would be profinite. But when you go to prove that sheaves on CompHaus agree with sheaves on Profinite you need to resolve X by a profinite, so you need to cover X by some profinite Y. If you take the point of view that CompHaus are algebras for the codensity monad of the inclusion of Fintype into Type, then you get this "for free" by looking at the adjunction associated to this monad (and the counit would be such a cover).

[Dagur Asgeirsson]

Related to Sam's comment: In https://github.com/dagurtomas/LeanCondensed/blob/master/LeanCondensed/Discrete/Extend.lean I prove that every cofiltered diagram of finite sets with surjective transition maps which is a limit cone in Profinite is equivalent to a diagram indexed by structured arrows from its cone point to the functor FintypeCat.toProfinite (equivalent in the sense that they are related by an initial functor, i.e. have the same limit)

[Dagur Asgeirsson]

There was something similar, Profinite.extend, in LTE, but there it was not proved to be equivalent to the right Kan extension if I remember correctly

[Sam van G]

I thought some people here might also be interested in this thread: We now have a (very long and not yet Mathlib-ready, but) sorry-free proof of Stone duality for Profinite.

[Dagur Asgeirsson]

#13319 refactors the definition of LightProfinite to mirror the definition of Profinite. It also provides an equivalence of categories with the old definition, proves that LightProfinite has countable limits, and that the functor to Profinite creates countable limits.

I think this is a good change, and we don't "lose" anything because we have the equivalence of categories with the old definition. I have plans for a followup PR to provide more API to interact with light profinite sets as sequential limits of finite sets.

I would then like to go further and unify all the definitions of CompHaus, Profinite, LightProfinite and Stonean as some form of my suggested CompHausLike, but that's not quite ready yet.

[Dagur Asgeirsson]

I've also checked that this refactor doesn't break anything related to light condensed stuff in #9526

[Dagur Asgeirsson]

I think I've found some pretty good API for a unified definition of these categories, see #12930.

Some evidence for the fact that this API is good is the big negative diff, and the fact that it can be used to prove a characterisation of discrete condensed sets and light condensed sets at the same time (#13893).

Unfortunately the refactor touches 23 files and might be a bit difficult to review. Would it be better to add the new definition first without refactoring the old ones? Or any other ideas to make this easier to review?

[Yaël Dillies]

Here are a few tips I have when doing a large refactor:

1. Don't ever move AND add/delete lemmas in the same PR.
2. If you can afford to leave the old API around while adding the new API, do. You can always clean it up a later PR.
3. If you can afford to redefine the old API in terms of the new one (replacing lemma old_foo := complicated_stuff by lemma old_foo := new_foo, do. You can always clean it up a later PR.

[Dagur Asgeirsson]

Thanks that's very helpful!

I'm not sure I understand point 3. Do you mean that I should, when the new API is in place, and I've redefined the old structures in terms of the new API, start by keeping all the old lemmas, reproving them using the new API if necessary, and then in a followup PR remove the ones that are now unnecessary?

[Dagur Asgeirsson]

I will at least start by opening a separate PR which only adds the new stuff

[Yaël Dillies]

For point 3, consider the pair:

• !3#14000 adding a bunch of new lemmas in a temporary division_monoid namespace and reproving the old lemmas in terms of them
• !3#14042 deleting the old lemmas and removing the namespace from the new lemmas

[Dagur Asgeirsson]

Ok I see, this seems very reasonable, but your example is a much deeper refactor than what I'm doing. In my case I think it's a bit overkill, since this part of mathlib is not widely used.
But I think I'll at least take the approach of introducing the new API gradually, to avoid these massive diffs

[Dagur Asgeirsson]

Ok to start, there is the tower

#13904 (add CompHausLike/Basic)
#13905 (add CompHausLike/Limits)
#13907 (add CompHausLike/EffectiveEpi)
#13908 (refactor CompHaus/Basic in terms of CompHausLike)
#13909 (refactor Profinite/Basic in terms of CompHausLike)
#13911 (refactor Stonean/Basic in terms of CompHausLike)
#13912 (refactor LightProfinite/Basic in terms of CompHausLike).

In particular, I didn't touch the old limit API unless to fix errors. It will then be mostly removed and unified in #12930.

[Dagur Asgeirsson]

So basically one file gets added/refactored in each PR, and each PR only touches other files if necessary to fix errors

[Riccardo Brasca]

So the first three PRs contain the new material, right?

[Riccardo Brasca]

I mean, those are not refactoring anything

[Dagur Asgeirsson]

Yes, that’s right

[Johan Commelin]

I am really sorry that I still haven't found time to review these. And it looks like I won't have time in the next few days either.

Can I bump this on someone elses review queue?

[Dagur Asgeirsson]

I would really appreciate a review of #13905. It adds a 300-line file constructing explicit pullbacks and finite coproducts in CompHausLike P, using new typeclasses HasExplicitPullbacks etc.
I guess this is the most "controversial" material, after this is merged, #13907 is straightforward , and in the following PRs, the refactor starts.

[Johan Commelin]

I left a tiny comment and a :peace_sign:

[Dagur Asgeirsson]

Anyone up for reviewing the straightforward #13907 (the last one adding new material before the actual refactor starts)?

[Dagur Asgeirsson]

Anyone up for reviewing #13911 and #13912? Those are the remaining basic files to be refactored: Stonean and LightProfinite. The ones for CompHaus and Profinite are already merged

[Johan Commelin]

Both are now merged/borsified.

[Dagur Asgeirsson]

Thanks for the merges! The old explicit limit API is now ripped out in three chunks: #15362, #15363 and #12930 with a total diff of (+129 −1,202)

[Johan Commelin]

Final PR is borsified

[Dagur Asgeirsson]

Thanks for all the reviews!

[Riccardo Brasca]

@Dagur Asgeirsson can you please open a PR adding a bit of documentation about CompHausLike? Asking because the new definition of Profinite confused quite a lot of people at a conference I am participating. Thanks!

[Dagur Asgeirsson]

Yes, I’ll do that asap (a bit later today)

[Dagur Asgeirsson]

@Riccardo Brasca #16473

It adds a long explanation in the file CompHausLike.Basic, and a pointer to that file in CompHaus.Basic, Profinite.Basic, etc.

I also added myself as an author to these basic files so that people know to ask me if they're confused about this

[Adam Topaz]

What’s the conference?

[Riccardo Brasca]

http://conference.bicmr.pku.edu.cn/meeting/index?id=119