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: free completion of a category

Patrick Nicodemus (Nov 16 2021 at 05:49):

Zhen Lin commented in a recent post that the free completion of a category $\mathcal{C}$ should be $[\mathcal{C}, \mathbf{Sets}]^{\rm op}$. In theory opposite categories are somewhat difficult to understand but a famous result of topos theory is that $[\mathcal{C},\mathbf{Sets}]^{\rm op}$ is monadic over $[\mathcal{C}, \mathbf{Sets}].$ I am wondering if anything has been made of this for the sake of concretely working with the free completion. Are there any papers out there that need the free completion of $\mathcal{C}$ for concrete or computational ends and implement this as the category of monad algebras for the "double powerset" monad on $[\mathcal{C},\mathbf{Sets}]$?

Morgan Rogers (he/him) (Nov 16 2021 at 10:08):

It seems more likely that, when needed, $[\mathcal{C},\mathrm{Set}]^{\mathrm{op}}$ is treated as the opposite of a topos. That is, arguments are made in $[\mathcal{C},\mathrm{Set}]$ and then dualized, since copresheaves are a lot more concrete than algebras for the double powerset monad.

Zhen Lin Low (Nov 16 2021 at 13:34):

Famously, the double powerset monad on the category of sets can be identified with the complete atomic boolean algebras monad, so it's possible to very concrete.

John Baez (Nov 16 2021 at 14:34):

So can objects in $[\mathcal{C}, \text{Set}]^{\text op}$ be understood as "complete atomic boolean algebra objects" in the presheaf topos $[\mathcal{C}, \text{Set}]$, or something like that?

I guess I'm really asking if we can get a sort of concrete description of algebras of the "double powerset" monad in a general topos, as objects equipped with a bunch of operations obeying a bunch of laws.

Morgan Rogers (he/him) (Nov 16 2021 at 16:02):

Zhen Lin Low said:

Famously, the double powerset monad on the category of sets can be identified with the complete atomic boolean algebras monad, so it's possible to very concrete.

This is true, but if I have the choice between viewing an object as a complete atomic boolean algebra or as a set (and I'm not otherwise motivated to take the boolean algebra perspective) the set option seems simpler :upside_down:

Graham Manuell (Nov 16 2021 at 16:29):

John Baez said:

So can objects in $[\mathcal{C}, \text{Set}]^{\text op}$ be understood as "complete atomic boolean algebra objects" in the presheaf topos $[\mathcal{C}, \text{Set}]$, or something like that?

They won't be any kind of internal boolean algebra because that requires excluded middle. I think it might be able to be defined in terms of arbitrary meets and arbitrary joins satisfying certain axioms, but I could not say exactly what those axioms are.

On the other hand, I'm not sure this approach is super helpful here, since the algebra is not be finitary and so the externalisation won't be as straightforward as the simply taking functors into some category of algebras instead of Set.

John Baez (Nov 16 2021 at 17:00):

Right. I'm not interested in it because it could be helpful for something - I'm interested because it suggests there could be a principled way of generalizing "complete atomic boolean algebras" to other toposes. This is especially interesting in non-boolean toposes, since the generalization becomes nonobvious there.

Graham Manuell (Nov 16 2021 at 17:09):

Well, I agree that is interesting. I don't know how to view them purely algebraically, but they do have a known characterisation as the frames $L$ for which both the unique map from the initial frame $\Omega \to L$ and the codiagonal $L \oplus L \to L$ preserve arbitrary meets and the Heyting arrow.

Graham Manuell (Nov 16 2021 at 17:10):

I guess this might lead to an algebraic characterisation after all, though I haven't thought through the details.

John Baez (Nov 16 2021 at 17:14):

Graham Manuell said:

Well, I agree that is interesting. I don't know how to view them purely algebraically, but they do have a known characterisation as the frames $L$ for which both the unique map from the initial frame $\Omega \to L$ and the codiagonal $L \oplus L \to L$ preserve arbitrary meets and the Heyting arrow.

If this characterization of algebras of the double powerset monad is true in Set we could hope it's true more generally, e.g. in any Grothendieck topos.

Graham Manuell (Nov 16 2021 at 18:06):

Yes, it is true in any elementary topos with natural number object.

Jens Hemelaer (Nov 16 2021 at 21:04):

So maybe the internal complete atomic boolean algebras in a topos are precisely the objects of the form $\mathcal{P}(X)$ for $X$ an object in the topos?

John Baez (Nov 16 2021 at 21:55):

Yes, that's what I'm wondering. Of course you have to really stretch the concept of "internal complete atomic boolean algebra" for this to be correct in a nonboolean topos! "Boolean" is not really the best word for it anymore, since $P(X)$ is an internal Heyting algebra that may not be boolean.

Mike Shulman (Nov 16 2021 at 22:08):

Maybe just call it a "caba".

John Baez (Nov 16 2021 at 22:15):

I guess one concrete question is: given an object $X$ in an arbitrary topos, what are some ways that $P(X)$ is better than your average internal Heyting algebra in that topos?

John Baez (Nov 16 2021 at 22:16):

In some vague sense I'd expect it should be "as complete as it can be" and "as boolean as it can be".

Mike Shulman (Nov 16 2021 at 22:16):

Or maybe "as Heyting as it can be"?

John Baez (Nov 16 2021 at 22:18):

How does it get to be more Heyting than your typical internal Heyting algebra?

Graham Manuell (Nov 16 2021 at 22:19):

It's 100% complete, since it's a frame. It is also 'constructively completely distributive'. It doesn't really need to be close to Boolean at all, though it is what is called an 'overlap algebra'. Of course, all its properties can be derived from the characterisation I gave above.

Graham Manuell (Nov 16 2021 at 22:20):

But I don't really know exactly what you are looking for.

Mike Shulman (Nov 16 2021 at 22:21):

I think CCD is what I was thinking of as "more Heyting". Maybe that doesn't actually make any sense.

John Baez (Nov 16 2021 at 22:24):

But I don't really know exactly what you are looking for.

If I knew, I'd have asked a more precise question. Thanks! - your answers help.

I'm not even sure what 100% complete means, in a topos. Oh, I can guess: in Set a poset can have all set-indexed colimits, so in a topos we can ask for an internal poset to have all object-indexed colimits.

Graham Manuell (Nov 16 2021 at 22:33):

It's probably best to think of joins and meets as maps from the powerset of a poset $X$ to $X$ itself. Yeah, I mean it is internally complete, so not indexing by external notions of sets.

Graham Manuell (Nov 16 2021 at 22:43):

I think you can define meets as the right adjoint to the map from $X$ to downsets on $X$ (viewed as the obvious subset of the powerset) sending $x$ to the principle downset generated by $x$. And similarly for joins.

Graham Manuell (Nov 16 2021 at 22:48):

I've just realised that the definition of meets I just gave could be thought of as coming from a decategorification of the free completion mentioned at the start of this thread.