# Zulip Chat Archive

## Stream: maths

### Topic: Limits in a category

#### Calle Sönne (Dec 04 2020 at 09:47):

Hello! I am wondering how to proceed with the general "structure" of proving that limits exist in some category (category of Profinite sets for me). I started proving that products exists in my category since I thought proving limits exists directly would be annoying. So to prove limits exist I should only need to show that pullbacks exists (and possibly proving that products + pullbacks imply that limits exist if its not already in mathlib). Is this an "ok" method? Would there be much to gain from me proving that limits exists "explictly", like how in the category of topological spaces we have "Top.limit_cone"? Otherwise I might just do pullbacks because that seems like a much simpler case to me (and also products is already there).

#### Johan Commelin (Dec 04 2020 at 10:30):

@Calle Sönne I think it's fine to do what you propose. We've been moving towards an "implementation-agnostic" API for limits. On the other hand, if you ever want to use a construction of a limit explicitly, then Lean will feed you back whatever you fed it in the first place. The other option is to *always* use universal properties.

#### Adam Topaz (Dec 04 2020 at 10:31):

But note: existence of products and pullbacks does not imply existence of all limits

#### Calle Sönne (Dec 04 2020 at 10:31):

Adam Topaz said:

But note: existence of products and pullbacks does not imply existence of all limits

oh does it not

#### Calle Sönne (Dec 04 2020 at 10:31):

I am talking about arbitary products

#### Calle Sönne (Dec 04 2020 at 10:31):

so not binary, but maybe its still false?

#### Adam Topaz (Dec 04 2020 at 10:32):

Oh ok.... Then maybe, I can't remember exactly right now

#### Adam Topaz (Dec 04 2020 at 10:33):

(yeah, I read that as binary products)

#### Johan Commelin (Dec 04 2020 at 10:42):

at least mathlib knows that arbitrary products + equalizers implies all limits

#### Reid Barton (Dec 04 2020 at 10:43):

I think it's usually easier to just handle all limits directly though

#### Reid Barton (Dec 04 2020 at 10:45):

just because there's less category theory API to deal with then

#### Reid Barton (Dec 04 2020 at 10:45):

like a pullback involves three objects and two maps, but a general limit only involves one class of objects and one class of maps

#### Calle Sönne (Dec 04 2020 at 10:46):

Yeah the problem is that I am a bit scared of Top.limit_cone, since the topology it uses is the infimum of the induced topologies by the projection maps of the sections. But I really want to talk about the induced subset topology given by the product (so that I can get compactness etc. from the product) and (to me) it seems hard to move between these two.

#### Calle Sönne (Dec 04 2020 at 10:47):

If I am scared enough I might just do Profinite.limit_cone without referring to Top.limit_cone so that I can work with the subspace topology :joy:

#### Reid Barton (Dec 04 2020 at 10:49):

You can ignore Top.limit_cone

#### Reid Barton (Dec 04 2020 at 10:50):

Calle Sönne said:

If I am scared enough I might just do Profinite.limit_cone without referring to Top.limit_cone so that I can work with the subspace topology :joy:

Right, this is what I would recommend. But then you will have to prove the universal property again, which is a bit more work.

#### Reid Barton (Dec 04 2020 at 10:52):

If the proof ends up splitting naturally into dealing with products and with equalizers (probably better than pullbacks), then it would make sense to use that construction which I assume mathlib also has.

#### Reid Barton (Dec 04 2020 at 11:40):

Another approach to this would be to try to find the profinite sets as a reflective subcategory inside Top or inside compact Hausdorff spaces

#### Reid Barton (Dec 04 2020 at 11:44):

does the space of connected components construction https://ncatlab.org/nlab/show/totally+disconnected+space#properties preserve compact Hausdorffness?

#### Reid Barton (Dec 04 2020 at 11:49):

I think so because the "is in the same connected component of $X$" relation is closed in $X \times X$, right?

because it's the set of (x, y) such that f(x) = f(y) for every continuous f : X -> bool

#### Reid Barton (Dec 04 2020 at 11:50):

so from this you would learn not only that the category of profinite sets has limits, but also that these limits are computed as in Top and that it also has colimits

#### Kevin Buzzard (Dec 04 2020 at 12:07):

The plan had been to use Top's limits and explicitly prove that they work.

#### Calle Sönne (Dec 04 2020 at 13:03):

Reid Barton said:

Another approach to this would be to try to find the profinite sets as a reflective subcategory inside Top or inside compact Hausdorff spaces

this seems very interesting, didnt know about Stone–Čech compactification before. Would be fun to try this method at least (and feels more satisfying to me)

#### Reid Barton (Dec 04 2020 at 13:06):

I believe we already have compact Hausdorff spaces as a reflective subcategory of Top

#### Adam Topaz (Dec 04 2020 at 14:00):

A third approach is to prove that profinite sets are.... Profinite (limits of finite). Then proving limits exist is easy, right?

#### Calle Sönne (Dec 04 2020 at 14:03):

Adam Topaz said:

A third approach is to prove that profinite sets are.... Profinite (limits of finite). Then proving limits exist is easy, right?

But are they not inverse limits of finite sets? And I am not sure if colimits and limits commute

#### Calle Sönne (Dec 04 2020 at 14:03):

Maybe they do in this situation?

#### Adam Topaz (Dec 04 2020 at 14:04):

Wait, are you proving limits of profinite sets exist, or colimits?

#### Adam Topaz (Dec 04 2020 at 14:04):

Because profinite sets certainly don't have all colimits

#### Adam Topaz (Dec 04 2020 at 14:05):

(they're compact)

#### Calle Sönne (Dec 04 2020 at 14:05):

Reid Barton said:

so from this you would learn not only that the category of profinite sets has limits, but also that these limits are computed as in Top and that it also has colimits

wait then this should fail though?

#### Calle Sönne (Dec 04 2020 at 14:06):

Adam Topaz said:

Wait, are you proving limits of profinite sets exist, or colimits?

limits

#### Calle Sönne (Dec 04 2020 at 14:07):

Oh yeah you are right. I wasnt so familiar with this point of view, so I thought that profinite sets were inverse limits

#### Calle Sönne (Dec 04 2020 at 14:08):

and this might be a result thats very useful to know still.

#### Kevin Buzzard (Dec 04 2020 at 14:09):

inverse limit = limit. Yeah there was some chat a few days ago about relating these two points of view.

#### Calle Sönne (Dec 04 2020 at 14:09):

Oh really :joy: I need to get my notation right

#### Reid Barton (Dec 04 2020 at 14:09):

They do have colimits, but the colimits aren't computed as in Top

#### Adam Topaz (Dec 04 2020 at 14:14):

It's the stone Cech compactification of the topological colimit, right?

#### Kevin Buzzard (Dec 04 2020 at 14:16):

Is that always profinite?

#### Reid Barton (Dec 04 2020 at 14:19):

No, but then you also apply this space of connected components reflection as well.

#### Reid Barton (Dec 04 2020 at 14:19):

Hopefully I'm not talking nonsense because I didn't find precisely this written down anywhere. I guess one way to check would be to formalize it :upside_down:

#### Adam Topaz (Dec 04 2020 at 14:23):

I don't recall seeing the statement about colimits

#### Calle Sönne (Dec 04 2020 at 14:24):

Reid Barton said:

Hopefully I'm not talking nonsense because I didn't find precisely this written down anywhere. I guess one way to check would be to formalize it :upside_down:

you mean being a reflective subcategory?

#### Reid Barton (Dec 04 2020 at 14:25):

Right

#### Reid Barton (Dec 04 2020 at 14:25):

I'm pretty sure it is true for rather different reasons though

#### Adam Topaz (Dec 04 2020 at 14:26):

Wait how can this be true? Any compact Hausdorff is a colimit of profinites

#### Reid Barton (Dec 04 2020 at 14:26):

right, that's why you need the second reflector

#### Reid Barton (Dec 04 2020 at 14:26):

https://ncatlab.org/nlab/show/totally+disconnected+space#properties

#### Reid Barton (Dec 04 2020 at 14:26):

this is the version without compact Hausdorff, but it seems that this reflector preserves that

Last updated: May 12 2021 at 07:17 UTC