Category Theory
Zulip Server
Archive

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.


Stream: theory: category theory

Topic: Intuition for totality


view this post on Zulip Brendan Murphy (Mar 24 2024 at 05:03):

A locally small, large category C\mathcal{C} is called total if its yoneda embedding (into presheaves valued in small sets, not necessarily small themselves) admits a left adjoint, ie the representable presheaves on it form a reflective subcategory. We can equivalently phrase this in a couple ways (which in particular make sense in NBG or another language where we can't form the functor category, but can quantify over functors): any presheaf admits an initial map out to a representable presheaf (this is the universal morphism characterization of the adjunction), the weighted colimit of the identity functor by any presheaf exists (the universal property is the previous condition), all small coproducts exist and the coend c:CW(c)c\int^{c:\mathcal{C}} W(c) \cdot c exists for any presheaf WW, or the (large) colimit of any discrete fibration with small fibers CC\mathcal{C}' \to \mathcal{C} exists.

It seems like the utility of this defintion is in controlling the size of constructions, or in knowing we can take certain large colimits, so representability or adjoint functor criteria may be used. But I'm having trouble understanding/motivating the defintion to myself. I don't feel like i get the point of it as well as I do eg locally presentable categories. Maybe part of this is that the defintion involves quantifying over all large presheaves, and large presheaves on large categories feel wild/badly behaved. Does anyone know another characterization of total categories which is (subjectively) more natural? Eg we can characterize them as categories where "class X of large colimits exist" where X is something else than discrete fibrations over C\mathcal{C}, maybe something that depends less on C\mathcal{C}?

view this post on Zulip Brendan Murphy (Mar 24 2024 at 05:06):

Maybe if I had a better sense of weighted colimits it would feel more reasonable to me. The ordinary colimit of the identity functor is just the terminal object, and that's simple enough

view this post on Zulip Mike Shulman (Mar 24 2024 at 05:27):

Have you read Kelly's paper "A survey of totality for enriched and ordinary categories"? He includes some more equivalent characterizations of totality, although they may or may not be what you're looking for.

view this post on Zulip Mike Shulman (Mar 24 2024 at 05:29):

For example, CC is total if and only if it admits the weighted colimit colimWF\mathrm{colim}^W F whenever W:KopSetW:K^{\mathrm{op}} \to \mathrm{Set} and F:KCF:K\to C are such that for any cCc\in C the weighted colimit colimWC(c,F)\mathrm{colim}^W C(c,F-) exists in Set\mathrm{Set} (Theorem 5.3).

view this post on Zulip Mike Shulman (Mar 24 2024 at 05:31):

Or, CC is total if and only if it is a full reflective subcategory of some presheaf category [Bop,Set][B^{\mathrm{op}},\mathrm{Set}] (with BB not necessarily small, hence the presheaf category not necessarily locally small, although of course CC must be) (Theorem 6.3).

view this post on Zulip Mike Shulman (Mar 24 2024 at 05:33):

I don't think it is possible to characterize totality of CC in terms of the existence of a class of colimits that doesn't refer to CC in some way. Totality intrinsically involves a sort of "size condition" on CC, not just cocompleteness.

view this post on Zulip Mike Shulman (Mar 24 2024 at 05:34):

I do suspect that the difficulty you're having is part of the reason total categories have fallen out of use nowadays in favor of locally presentable ones.

view this post on Zulip Brendan Murphy (Mar 24 2024 at 05:37):

Yeah, that makes sense. I guess it's nicer to have everything controlled by small stuff and so directly reduce large (co)limits to small ones than to have to work with large (co)limits directly, but know they exist. I haven't read the Kelly paper, I feel like my enriched category theory is pretty weak and so I wasn't sure I'd be able to understand it. But I should probably take a look anyway

view this post on Zulip Mike Shulman (Mar 24 2024 at 05:38):

You can probably read most of it thinking of V=SetV=\mathrm{Set} in your head.

view this post on Zulip Mike Shulman (Mar 24 2024 at 05:38):

As long as you know what a weighted colimit is for ordinary categories.

view this post on Zulip Valery Isaev (Mar 26 2024 at 08:21):

I don't know much about total categories, but I feel they're more well behaved constructively than locally presentable ones. Is that so?

view this post on Zulip Nathanael Arkor (Mar 26 2024 at 08:56):

What aspect of locally presentable categories is badly behaved constructively?

view this post on Zulip Valery Isaev (Mar 27 2024 at 08:31):

I think almost anything involving presentable objects requires the axiom of choice. E.g., I think only finite sets are presentable in Set without AC.

view this post on Zulip Morgan Rogers (he/him) (Mar 27 2024 at 10:29):

But finite sets generate the category of sets under filtered colimits, so that's enough?

view this post on Zulip Morgan Rogers (he/him) (Mar 27 2024 at 10:31):

Infinite sets are not presentable even with AC. The collection of functions NN\mathbb{N} \to \mathbb{N} is not the colimit of functions N[n]\mathbb{N} \to [n] as [n][n] tends to infinity, since any function with infinite image (such as the successor function) is not an element of that colimit.

view this post on Zulip Morgan Rogers (he/him) (Mar 27 2024 at 10:34):

(I realise that this example only shows that they're not finitely presentable, but you can perform the same argument with the κ\kappa-filtered diagram of finite sets of a set of any cardinality)

view this post on Zulip Valery Isaev (Mar 27 2024 at 10:52):

Every object of a locally presentable category is κ\kappa-presentable for some κ\kappa. That's what I meant by being presentable.

view this post on Zulip Nathanael Arkor (Mar 27 2024 at 12:04):

If you keep track of the presentability rank, rather than just working with locally presentable categories in general, presumably this becomes less of an issue?

view this post on Zulip Morgan Rogers (he/him) (Mar 27 2024 at 12:08):

Morgan Rogers (he/him) said:

(I realise that this example only shows that they're not finitely presentable, but you can perform the same argument with the κ\kappa-filtered diagram of finite sets of a set of any cardinality)

Upon further research, it seems that this generalization actually does not hold. Suppose that XiX_i are λ\lambda-presentable, that II is a λ\lambda-small diagram and that JJ is λ\lambda-filtered and X=colimiIXiX = \mathrm{colim}_{i \in I} X_i with each XiX_i being λ\lambda-presentable in a category CC. Then:
C(X,colimjJYj)limiIC(Xi,colimjJYj)limiIcolimjJC(Xi,Yj)colimjJlimiIC(Xi,Yj)colimjJC(X,Yj)C(X, \mathrm{colim}_{j \in J} Y_j) \cong \lim_{i \in I} C( X_i, \mathrm{colim}_{j \in J} Y_j) \cong \lim_{i \in I} \mathrm{colim}_{j \in J} C( X_i, Y_j) \cong \mathrm{colim}_{j \in J}\lim_{i \in I} C( X_i, Y_j) \cong \mathrm{colim}_{j \in J} C(X, Y_j).
So the only reason you need choice is to make cardinals linearly ordered, which I'm pretty sure is not strictly necessary to the theory of presentable categories.

view this post on Zulip Morgan Rogers (he/him) (Mar 27 2024 at 12:11):

There is no choice in the above argument, only the fact that λ\lambda-filtered colimits commute with λ\lambda-small limits in Set (which you can take to be the definition of λ\lambda-filtered if you like)

view this post on Zulip Valery Isaev (Mar 27 2024 at 14:10):

Morgan Rogers (he/him) said:

There is no choice in the above argument, only the fact that $\lambda$-filtered colimits commute with $\lambda$-small limits in Set (which you can take to be the definition of $\lambda$-filtered if you like)

Hm... I didn't think about that. Maybe this works fine, but I didn't see anybody trying to develop the theory of locally presentable categories constructively using this definition.

view this post on Zulip Nathanael Arkor (Mar 27 2024 at 15:06):

The formal theory of presentability developed in @Ivan Di Liberti and @fosco's Accessibility and presentability in 2-categories is constructive. It is based on distributivity of limits over colimits rather than commutativity, but the two are closely related.

view this post on Zulip Brendan Murphy (Mar 27 2024 at 16:34):

I also thought the theory of presentable/acessible categories was nonconstructive bc of hard to control cardinal bounds and the usage of presentability as roughly "any small object argument you want to run will terminate". But I haven't read the paper, and hopefully if I read it my confusion will be cleared up

view this post on Zulip Brendan Murphy (Mar 27 2024 at 16:44):

Oh this paper is quite nice. It reminds me of https://arxiv.org/abs/2210.08582, although to be clear Ivan & Fosco's paper predates Rezk's (I just read them non chronologically) and likely the content of Rezk's paper that I'm reminded of is also in A Classification of Accessible Categories (which I also haven't read).

view this post on Zulip Brendan Murphy (Mar 27 2024 at 16:45):

One thing that's unclear to me, however, is whether we can utilize this abstract theory of presentable/acessible categories without knowing eg every cardinal is bounded by a regular cardinal? And I think this would require choice

view this post on Zulip Nathanael Arkor (Mar 27 2024 at 17:09):

Brendan Murphy said:

One thing that's unclear to me, however, is whether we can utilize this abstract theory of presentable/acessible categories without knowing eg every cardinal is bounded by a regular cardinal? And I think this would require choice

The formal theory there works for locally λ\lambda-presentable categories for fixed λ\lambda. To obtain results about locally presentable categories in general formally would require additional work (but should be possible). I would expect the theory should still be constructive, but might require more care, for instance using [[arity classes]] rather than regular cardinals.

view this post on Zulip Brendan Murphy (Mar 27 2024 at 17:11):

Gotcha, I'd be interested to see that worked out (I'd be interested to work it out but I'm not sure I have the time :P)

view this post on Zulip Brendan Murphy (Mar 27 2024 at 17:16):

In a pretty different direction, I'd be interested to see if a constructive theory can give better cardinal bounds in some cases. I was giving a talk recently where I needed to use the fact that the derived category (of complexes with quasicoherent cohomology) on a qcqs scheme is compactly generated/locally finitely presented. I thought this would be an easy consequence of the (infinity) sheaf condition for the derived category, because it's easily true in the affine case and qcqs schemes are the gluings of finite diagrams of affines, but when I tried to work out the details I couldn't make it work and the proof in the literature is hard/not formal. In general it would be nice if more results about presentable categories came with explicit cardinal bounds

view this post on Zulip Mike Shulman (Mar 28 2024 at 14:25):

Does this formal theory enable us to perform the small object argument constructively?

view this post on Zulip Nathanael Arkor (Mar 28 2024 at 16:46):

I suppose one prerequisite question is: what is the appropriate notion of weak factorisation system on an object of a suitable 2-category?

view this post on Zulip Mike Shulman (Mar 28 2024 at 16:53):

I suppose one might ask that question, but I was just thinking of taking the formal theory and specializing it to a constructive version of Cat.

view this post on Zulip Mike Shulman (Mar 28 2024 at 16:53):

E.g. internal categories in, or indexed categories over, some topos.

view this post on Zulip Nathanael Arkor (Mar 28 2024 at 16:54):

Ah, I see.

view this post on Zulip Valery Isaev (Mar 29 2024 at 10:23):

Ah, indeed, if I remember correctly the theory of locally presentable categories relies on some form of small object argument and I'm not sure that this part can be made constructive.

view this post on Zulip Nathanael Arkor (Mar 29 2024 at 10:39):

What do you by "relies upon"? It's not even mentioned in "Locally presentable and accessible categories", for instance. It seems an application of the theory of locally presentable categories, rather than part of the theory itself.

view this post on Zulip Ivan Di Liberti (Mar 29 2024 at 12:23):

The soa is key in LPAC, but it goes under the name of "orthogonal reflection".

And I agree with saying that the statement "a small orthogonality class in a LP category is reflective" is absolutely central in the theory of presentability, especially in the direction of removing any cardinal reference.

This can be indeed taken as a form of definition of LP category in a "Yoneda structure" where you have any notion of "small object". You can say and LP category is an "orthogonality class" (this is a 2-limit) "in a Psh(C)" (C small) with respect to a "small set of maps". :eyes:

view this post on Zulip Mike Shulman (Mar 29 2024 at 15:52):

It took me quite a while too to realize that the small object argument is key in "Locally presentable and accessible categories" because they don't call it that!

view this post on Zulip Reid Barton (Apr 03 2024 at 16:51):

There's some upper bound on how much of the theory of locally presentable categories can be made to work constructively, because this theory produces initial algebras for (even infinitary) algebraic theories (via sketches and the orthogonal reflection construction), which apparently need not exist even in ZF, by a paper of Blass: https://eudml.org/doc/211359

view this post on Zulip Brendan Murphy (Apr 03 2024 at 20:53):

That makes me think of the theory of class local presentability, where you lose nice things like adjoint functor theorems. I wonder if that theory would generalize better? Otoh my impression is that the real power of locally presentable categories is in size bounds and knowing that transfinite constructions terminate