Zulip Chat Archive

Stream: maths

Topic: Limits in a category


view this post on Zulip 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).

view this post on Zulip 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.

view this post on Zulip Adam Topaz (Dec 04 2020 at 10:31):

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

view this post on Zulip 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

view this post on Zulip Calle Sönne (Dec 04 2020 at 10:31):

I am talking about arbitary products

view this post on Zulip Calle Sönne (Dec 04 2020 at 10:31):

so not binary, but maybe its still false?

view this post on Zulip Adam Topaz (Dec 04 2020 at 10:32):

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

view this post on Zulip Adam Topaz (Dec 04 2020 at 10:33):

(yeah, I read that as binary products)

view this post on Zulip Johan Commelin (Dec 04 2020 at 10:42):

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

view this post on Zulip Reid Barton (Dec 04 2020 at 10:43):

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

view this post on Zulip Reid Barton (Dec 04 2020 at 10:45):

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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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:

view this post on Zulip Reid Barton (Dec 04 2020 at 10:49):

You can ignore Top.limit_cone

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip Reid Barton (Dec 04 2020 at 11:49):

I think so because the "is in the same connected component of XX" relation is closed in X×XX \times X, right?
because it's the set of (x, y) such that f(x) = f(y) for every continuous f : X -> bool

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Dec 04 2020 at 12:07):

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

view this post on Zulip 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)

view this post on Zulip Reid Barton (Dec 04 2020 at 13:06):

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

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip Calle Sönne (Dec 04 2020 at 14:03):

Maybe they do in this situation?

view this post on Zulip Adam Topaz (Dec 04 2020 at 14:04):

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

view this post on Zulip Adam Topaz (Dec 04 2020 at 14:04):

Because profinite sets certainly don't have all colimits

view this post on Zulip Adam Topaz (Dec 04 2020 at 14:05):

(they're compact)

view this post on Zulip 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?

view this post on Zulip Calle Sönne (Dec 04 2020 at 14:06):

Adam Topaz said:

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

limits

view this post on Zulip 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

view this post on Zulip Calle Sönne (Dec 04 2020 at 14:08):

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

view this post on Zulip 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.

view this post on Zulip Calle Sönne (Dec 04 2020 at 14:09):

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

view this post on Zulip Reid Barton (Dec 04 2020 at 14:09):

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

view this post on Zulip Adam Topaz (Dec 04 2020 at 14:14):

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

view this post on Zulip Kevin Buzzard (Dec 04 2020 at 14:16):

Is that always profinite?

view this post on Zulip Reid Barton (Dec 04 2020 at 14:19):

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

view this post on Zulip 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:

view this post on Zulip Adam Topaz (Dec 04 2020 at 14:23):

I don't recall seeing the statement about colimits

view this post on Zulip 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?

view this post on Zulip Reid Barton (Dec 04 2020 at 14:25):

Right

view this post on Zulip Reid Barton (Dec 04 2020 at 14:25):

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

view this post on Zulip Adam Topaz (Dec 04 2020 at 14:26):

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

view this post on Zulip Reid Barton (Dec 04 2020 at 14:26):

right, that's why you need the second reflector

view this post on Zulip Reid Barton (Dec 04 2020 at 14:26):

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

view this post on Zulip 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