Limits in a category

Stream: maths

[Calle Sönne]

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]

@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]

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

[Calle Sönne]

Adam Topaz said:

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

oh does it not

[Calle Sönne]

I am talking about arbitary products

[Calle Sönne]

so not binary, but maybe its still false?

[Adam Topaz]

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

[Adam Topaz]

(yeah, I read that as binary products)

[Johan Commelin]

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

[Reid Barton]

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

[Reid Barton]

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

[Reid Barton]

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]

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]

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]

You can ignore Top.limit_cone

[Reid Barton]

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]

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]

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]

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

[Reid Barton]

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]

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]

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

[Calle Sönne]

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]

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

[Adam Topaz]

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

[Calle Sönne]

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]

Maybe they do in this situation?

[Adam Topaz]

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

[Adam Topaz]

Because profinite sets certainly don't have all colimits

[Adam Topaz]

(they're compact)

[Calle Sönne]

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]

Adam Topaz said:

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

limits

[Calle Sönne]

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]

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

[Kevin Buzzard]

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

[Calle Sönne]

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

[Reid Barton]

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

[Adam Topaz]

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

[Kevin Buzzard]

Is that always profinite?

[Reid Barton]

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

[Reid Barton]

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]

I don't recall seeing the statement about colimits

[Calle Sönne]

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]

Right

[Reid Barton]

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

[Adam Topaz]

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

[Reid Barton]

right, that's why you need the second reflector

[Reid Barton]

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

[Reid Barton]

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