You're reading the public-facing archive of the Category Theory Zulip server.
To join the server you need an invite. Anybody can get an invite by contacting Matteo Capucci at name dot surname at gmail dot com.
For all things related to this archive refer to the same person.
Bernd Losert (Feb 03 2024 at 14:31):Are there any theorems characterizing which categories have Set-like directed colimits, i.e. directed colimits that are constructed as quotients of sums?
Morgan Rogers (he/him) (Feb 03 2024 at 17:17):The fact that you can present a colimit as a quotient of a coproduct is dual to the result that you can express any limit as a subobject of a product: it's true as soon as the respective (co)limits exist, with no further requirements, since the proof is just to check the required universal property.
Bernd Losert (Feb 03 2024 at 17:27):@Morgan Rogers (he/him) Do you have a reference to this result?
Morgan Rogers (he/him) (Feb 03 2024 at 17:28):For limits I'm pretty sure it's in Categories for the Working Mathematician or Riehl's Categories in context.
Madeleine Birchfield (Feb 03 2024 at 17:31):Morgan Rogers (he/him) said:
The fact that you can present a colimit as a quotient of a coproduct is dual to the result that you can express any limit as a subobject of a product: it's true as soon as the respective (co)limits exist, with no further requirements, since the proof is just to check the required universal property.
Is there an analogue of this result for limits and colimits in -category theory?
Morgan Rogers (he/him) (Feb 03 2024 at 17:35):I believe so, but I'll need someone else to give appropriate pointers for that.
Bernd Losert (Feb 03 2024 at 17:39):@Morgan Rogers (he/him) Are you refering to the construction of limits using products and equalizers?
Morgan Rogers (he/him) (Feb 03 2024 at 17:40):That's the one!
Paolo Perrone (Feb 03 2024 at 17:42):A particular instance of that (stalks of a sheaf) is explained quite well on the Stacks project.
Bernd Losert (Feb 03 2024 at 17:42):Ah, so those equalizers end up being subobjects. I did not realize.
Morgan Rogers (he/him) (Feb 03 2024 at 17:43):This is by the result that equalizers are monos, which is also entirely general!
Bernd Losert (Feb 03 2024 at 20:57):Another question: If I have a sequence of right adjoint functors , then I can construct a directed colimit in by dropping down to via , constructing the colimit in , and then applying the left adjoints, right?
Reid Barton (Feb 03 2024 at 21:24):It depends! This is not a general fact about adjoints.
Bernd Losert (Feb 03 2024 at 23:28):Really? I thougth left adjoints preserve colimits.
Morgan Rogers (he/him) (Feb 03 2024 at 23:35):They do, but the thing you end up with will not typically be a colimit of the original diagram.
Morgan Rogers (he/him) (Feb 03 2024 at 23:37):What you really want is for the functors to create colimits, which is a stronger property (and even then the colimit will usually not be constructed by simply applying the left adjoints)
Bernd Losert (Feb 04 2024 at 09:23):Hmm... so what is the relationship between having a left adjoint and creating/lifting/reflecting colimits?
Morgan Rogers (he/him) (Feb 04 2024 at 09:44):If the functors (right adjoints) are full and faithful, the unit of the overall adjunction will be an isomorphism, so your original construction works; this is the exception to what I said above. There is a general result that monadic functors create limits, and so dually comonadic functors create colimits, but those would be functors with right adjoints (worth noting that being comonadic is not preserved by composition but the property of creating (co)limits is).
Bernd Losert (Feb 04 2024 at 12:46):Morgan Rogers (he/him) said:
What you really want is for the functors to create colimits, which is a stronger property (and even then the colimit will usually not be constructed by simply applying the left adjoints)
This confuses me. If the left adjoint can't be used to obtain the colimits, how do you obtain them then? Do you have to investigate the proof of "U creates colimits" to figure out what the construction is?
Morgan Rogers (he/him) (Feb 04 2024 at 13:42):You typically do! For monadic functors you really work with algebras to construct the limits, for instance
Bernd Losert (Feb 04 2024 at 13:54):Morgan Rogers (he/him) said:
You typically do! For monadic functors you really work with algebras to construct the limits, for instance
This is troublesome. Unless there is some kind of central repository or reference for all of category theory, how am I going to find out what the construction is when I read "U creates colimits"?
Bernd Losert (Feb 04 2024 at 13:57):By the way, I think "creates" is too strong. For example, U : Top → Set does not create colimits, but I know how to lift colimits in Set to colimits in Top via the final topology.
Patrick Nicodemus (Feb 04 2024 at 17:02):Can you just post the theorem you're having trouble with? I am optimistic that if somebody here gives you a clear construction of the "created limit" you will be more confident about proving it yourself in the future and it will not take you so much time as to be a significant burden
Patrick Nicodemus (Feb 04 2024 at 17:04):In theory yes people should give the construction. In practice because the answer is uniquely determined (not just up to isomorphism but up to equality of limit cones) there are extremely strong constraints that guide the search for a solution and make it possible to solve it without prior knowledge
Patrick Nicodemus (Feb 04 2024 at 17:04):At this point I'm genuinely curious what your theorem is that apparently is not immediately connected to the standard proof that monadic functors create limits.
Bernd Losert (Feb 04 2024 at 18:38):Patrick Nicodemus said:
Can you just post the theorem you're having trouble with?
There is no theorem yet. In my research, I am working with categories Ord, Conv, M-Set and combinations of them and I need to describe how to construct the colimit in all these combinations. At the moment, I literally have to refer to the construction in Set and explain how to modify the proof to get the construction in e.g. M-OrdConv, which I find kind of silly.
Kevin Arlin (Feb 04 2024 at 19:17):If a functor creates limits, then in practice the limits in its domain are constructed by constructing them in the codomain and then adding obvious structure to lift, as in the category of groups. It’s a good observation that the forgetful functor out of topological spaces does not create limits. The possible of initial and final topologies actually makes this forgetful functor what is literally called a topological functor in honor of this case. All in all I don’t really understand what exactly it is you’re finding kind of silly—that if you work in a category that hasn’t been studied much, you might have to say a few sentences about what its colimits are if you want to provide an explicit construction?
Bernd Losert (Feb 04 2024 at 19:24):I find it silly because I feel that there should be a better way of explaining how to construct colimits. Let's suppose I want to formalize my results in proof assistant like Lean. I can't really say "just tweak the proof from the Set case like this" in Lean. I need a better approach.
Kevin Arlin (Feb 04 2024 at 19:35):Hmm, I’m not really sure what you mean my tweaking the Set proof. To construct colimits in M-Set, we should observe that M acts naturally on the colimits of the underlying sets of a diagram and check the universal property. For convergences spaces, put the coarsest convergence on the colimits of underlying sets consistent with the convergences on the spaces in the diagram. For orders, take the transitive closure of the relation induces on the colimit, etc. You can give some of the same proofs for many base categories at once, most easily in the case of M-Sets. These kinds of things are done in Lean all the time. Maybe you’d get some more clarity by poking around in the category theory part of Mathlib.
Bernd Losert (Feb 04 2024 at 19:59):I’m not really sure what you mean my tweaking the Set proof.
What you wrote afterwards is exactly what I mean.
These kinds of things are done in Lean all the time. Maybe you’d get some more clarity by poking around in the category theory part of Mathlib.
Really? I was poking around today in fact and I didn't find anything useful for my needs. I will ask in the Lean Zulip for pointers.
John Baez (Feb 04 2024 at 20:07):I wouldn't personally mess around with Lean for this, though of course tastes very. If someone tells me "you can give some of the same proofs for many base categories at once, most easily in the case of M-Sets" I would try to figure out what features of Set, MSet, etc. make the proof work, and write down the proof using assumptions that capture these features It would be a matter of copying the proof for Set but generalizing it as we go.
Patrick Nicodemus (Feb 04 2024 at 23:57):@Bernd Losert I agree with Kevin that you shouldn't have to tweak the proof in Set. Instead you should be able to use the construction in Set as a lemma.
Let U be the forgetful functor from Top to Set and let X be a functor valued in Top regarded as a diagram. Let Z, gamma : UX => Z be the colimit (and its cocone) of UX. There is a category whose objects are cocones with domain X and which live over (Z, gamma). The colimit of X is exactly the initial cocone in this category. This works for any so called topological functor U. By this interpretation I don't think that we are modifying the construction of the colimit Z, instead we are using it as a lemma, a construction on top of which we add additional structure
Morgan Rogers (he/him) (Feb 05 2024 at 06:59):What Patrick said works whenever U preserves colimits, but the construction of the initial object will depend on further hypotheses which are not unique. When the functor creates colimits, the "category whose objects are cocones under X which live over (Z,gamma)" is contractible (there is essentially only one choice as long as you can find it), whereas in Top the initial object exists because the fiber over Z is a complete lattice and we can find at least one object in it using the fact that an adjoint preserves the fiber (that is, Z with the discrete topology is an object living over Z).
Beyond imposing the non-constructive hypothesis that "the initial object in ... exists", I don't see a common underlying construction here. (EDIT: This is the same reason that there are several independent Adjoint Functor Theorems.)
Bernd Losert (Feb 05 2024 at 08:52):@Patrick Nicodemus What you wrote is basically the sort of thing I was asking for: If you have a forgetful functor U : C → Set, are there any theorems that say how to build the directed colimit in C based on the directed colimit in Set. If U is monadic or topological, the answer seems to be yes. I need one more theorem to cover the case where C is Pos or something like Pos.
Graham Manuell (Feb 05 2024 at 11:20):Well if C is Pos then U is still topological, so you dont need one more theorem for that. The monadic and topological cases are also both subsumed by the theory of [[solid functors]].
Bernd Losert (Feb 05 2024 at 11:48):Graham Manuell said:
Well if C is Pos then U is still topological, so you dont need one more theorem for that. The monadic and topological cases are also both subsumed by the theory of [[solid functors]].
According to Joy of Cats, Examples 21.2, Pos is not topological. But thanks for reminding me about solid functors.
Patrick Nicodemus (Feb 05 2024 at 12:33):There is the theory of fibrations and opfibrations as well. We have a general theorem how to construct colimits in the total category of an opfibration from colimits in the base category if the total category has all colimits of the right shape and reindexing functors preserve them. Sorry I'm on my phone and don't have paper to check whether posets form an opfibration
Madeleine Birchfield (Feb 05 2024 at 15:25):Bernd Losert said:
Morgan Rogers (he/him) Are you refering to the construction of limits using products and equalizers?
Morgan Rogers (he/him) said:
That's the one!
So is this just for finite limits and colimits or does this also extend to the infinitary case as well?
Morgan Rogers (he/him) (Feb 05 2024 at 15:30):It extends to the infinitary case (checking this is a good exercise)
Graham Manuell (Feb 05 2024 at 16:18):Bernd Losert said:
Graham Manuell said:
Well if C is Pos then U is still topological, so you dont need one more theorem for that. The monadic and topological cases are also both subsumed by the theory of [[solid functors]].
According to Joy of Cats, Examples 21.2, Pos is not topological. But thanks for reminding me about solid functors.
Oh. Sorry. I was thinking of preorders. Anyway, the functor is still solid.
Reid Barton (Feb 05 2024 at 19:33):I just wanted to add that it is not the case in general that right adjoints preserve directed colimits. It is true notably that the forgetful functor for a finitary algebraic theory preserves directed colimits. It is also true for topological spaces, even though they aren't the models of a finitary algebraic theory.
Kevin Arlin (Feb 05 2024 at 19:36):Madeleine Birchfield [said]
So is this just for finite limits and colimits or does this also extend to the infinitary case as well?
Any limit is a reflexive equalizer of a (possibly infinite) product.
Bernd Losert (Feb 07 2024 at 10:14):I am seeing in a lot of articles that it's enough for U : C → Set to detect directed colimits to construct a colimit in C from a directed colimit in Set (as long as the proof has the construction). And in the cases I am interested in, this construction gives me the directed colimit I am actually interested in.
Morgan Rogers (he/him) (Feb 07 2024 at 10:41):What does it mean to "detect" a colimit?
Bernd Losert (Feb 07 2024 at 11:15):Given functors D : I → C and F : C → D, F detects colimits of D if colim (F ∘ D) exists implies colim D exists.
Bernd Losert (Feb 07 2024 at 20:03):Kevin Arlin said:
For orders, take the transitive closure of the relation induces on the colimit..
Do you have a reference showing the construction of directed colimits of posets?
Bernd Losert (Feb 07 2024 at 20:09):Also, I think the transitive closure just gives you a preorder, not a partial order.
Kevin Arlin (Feb 07 2024 at 20:11):Sure, you take the transitive closure and then identify mutually comparable objects to get antisymmetry, you’re right. I have trouble respecting the difference between preorders and posets sometimes.
Kevin Arlin (Feb 07 2024 at 20:13):Directed colimits of posets are trivial: the induced relation on the colimit of underlying sets is already transitive. No idea what might be a reference for this, but it’s a very common phenomenon as many important categories are locally finite presentable.
Bernd Losert (Feb 07 2024 at 20:17):Kevin Arlin said:
Sure, you take the transitive closure and then identify mutually comparable objects to get antisymmetry, you’re right. I have trouble respecting the difference between preorders and posets sometimes.
So basically "take the colimit in Pre and then apply the free Pre → Pos functor".
Kevin Arlin (Feb 07 2024 at 20:17):Incidentally, the correction on general colimits of posets is an instance of a very useful and common phenomenon. Posets are a reflective subcategory of preorders, which means a full subcategory such that for any preorder there’s a map into a poset through which every map from to any poset factors uniquely. In any such situation, the reflective subcategory has limits computed exactly as in the supercategory (created by the inclusion functor, formally) and colimits constructed by constructing them in the supercategory, then applying the reflection functor. This reflection functor is the “identify objects that are comparable to each other” operation from above in the case of posets. Very often the inclusion functor also creates directed colimits, as here.
Kevin Arlin (Feb 07 2024 at 20:17):Ah yes, “take the colimit of preorders and then apply the free poset functor” is exactly what I was explaining just as you posted it.
Kevin Arlin (Feb 07 2024 at 20:18):It’s a lot like what you were hoping for at the top of the thread—it’s just that it only works when the forgetful functor is fully faithful.
Bernd Losert (Feb 07 2024 at 20:18):Kevin Arlin said:
Directed colimits of posets are trivial: the induced relation on the colimit of underlying sets is already transitive. No idea what might be a reference for this, but it’s a very common phenomenon as many important categories are locally finite presentable.
It's trivial enough that even I have a explicit proof of it, but I would like to just have a reference - otherwise I am going to have to spell it out in the paper I am writing.
Bernd Losert (Feb 07 2024 at 20:37):@Kevin Arlin What a tick... what relation are we taking the transitive closure of?
Bernd Losert (Feb 07 2024 at 20:37):In my proof, I construct a partial ordering directly - no futzing around with closures and free constructions.
Kevin Arlin (Feb 07 2024 at 20:39):You shouldn’t have to futz around with directed colimits, if that’s what you mean—as I said there’s no need for a closure in that case, and as I probably didn’t say clearly, the directed colimit taken as in preordered sets is already a poset, so no need for a free construction either. Both steps are for general colimits, where you certainly will need them.
Bernd Losert (Feb 07 2024 at 21:01):Since I don't have a reference regarding directed colimits of preorders, I am forced to construct the partial order directly for the directed colimit. The construction is basically the one on the Wikipedia page (https://en.wikipedia.org/wiki/Direct_limit) but instead I define if and only if . Then you can use that to define the partial ordering on the quotient of the union.
Kevin Arlin (Feb 07 2024 at 21:03):Yes, that sounds like the same idea I’m describing. You could see whether this is given as an example in Adamek and Rosicky’s book on locally presentable categories, it’s just not the kind of thing that would predictably appear in a paper since nobody would ever claim to be the first to prove it.
Kevin Arlin (Feb 07 2024 at 21:04):If it’s in there they’ll probably just assert that it works the way you say, in any case, but that can still be nice sometimes.
Bernd Losert (Feb 26 2024 at 23:26):Morgan Rogers (he/him) said:
If the functors (right adjoints) are full and faithful, the unit of the overall adjunction will be an isomorphism, so your original construction works; this is the exception to what I said above. There is a general result that monadic functors create limits, and so dually comonadic functors create colimits, but those would be functors with right adjoints (worth noting that being comonadic is not preserved by composition but the property of creating (co)limits is).
Sorry about bringing this up again. So say A is a full, isomorphism-closed, reflective subcategory of B and let U : A → B be the embedding. Given a diagram D : I → A such that the colim U ∘ D exists, then F (colim U ∘ D) ≅ colim (F ∘ U ∘ D) ≅ colim D, where the first ≅ follows from F preserving colimits and the last ≅ follows from the full, isomorphism-closed part, right?
Because A is full, isomorphism-closed and reflective, U is monadic. Being monadic means that U creates all colimits that exist in B and are preserved by UF and UFUF. But in the F (colim U ∘ D) ≅ colim D "proof", I didn't make use of the fact that UF and UFUF preserve colimits, so something is not right.
Morgan Rogers (he/him) (Feb 27 2024 at 10:22):What do you think is not right? Reflective categories are a special case where you don't need to use monadicity to construct the limits and colimits because the simpler description that you gave works out. Note that it's not necessarily the case that preserves any given colimits: a colimit in need not be a colimit in .
Bernd Losert (Feb 27 2024 at 13:15):Thanks for the response. I get it now. I guess I was to aiming to say that U creates colimits, but that's not necessarily the case and in fact I think it is enough for my use case that U just lifts colimits uniquely.
Bernd Losert (Feb 27 2024 at 15:59):By the way, does "isomorphism-closed" translate to some property of the reflector or the inclusion? It seems to be a stronger condition.
Mike Shulman (Feb 27 2024 at 16:00):It means the inclusion is an [[isofibration]].
Morgan Rogers (he/him) (Feb 27 2024 at 16:01):It's a very weak requirement: closing under isomorphisms gives an equivalent subcategory, so it's just for convenience.
Bernd Losert (Feb 27 2024 at 16:04):Got it.