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: learning: questions

Topic: Internal categories and monadicity

Vincent Moreau (Oct 01 2024 at 09:45):

Dear category theorists,

On the Internal category nlab page, in the "In a cartesian closed category" paragraph, it is written:

Theorem 4.1. Let $\mathbf{E}$ be a finitely complete cartesian closed category. Then the category $\mathbf{Cat}(\mathbf{E})$ of internal categories in $\mathbf{E}$ is also finitely complete and cartesian closed.

Proof. First suppose $\mathbf{E}$ is finitely complete. Then the category of directed graphs $\mathbf{E}^{\bullet \rightrightarrows \bullet}$ is also finitely complete, and since $\mathbf{Cat}(\mathbf{E})$ is monadic over $\mathbf{E}^{\bullet \rightrightarrows \bullet}$, it follows that $\mathbf{Cat}(\mathbf{E})$ is also finitely complete.

I don't understand how this argument works. I have the impression that the monadicity result relies on $\mathbf{E}$ being more than a finitely complete CCC, as there is no way to build the free internal category when $\mathbf{E}$ is $\mathbf{FinSet}$ for instance.

I don't really see where the general case is proven in the two references given. What do you think about all that?

Vincent Moreau (Oct 01 2024 at 09:46):

Side question: is it OK to ask that kind of question here? I have been posting a few ones and I just want to make sure this is the right place.

Nathanael Arkor (Oct 01 2024 at 10:00):

I don't know why monadicity is mentioned; the fact that Cat(E) inherits limits from E follows from the fact that Cat(E) is a category of finite limit preserving functors, in which limits are given pointwise. The remainder of the proof (or Johnstone's proof in the Elephant) look fine for cartesian closure.

Nathanael Arkor (Oct 01 2024 at 10:01):

By the way, another good reference for internal category theory is @Adrian Miranda's master's thesis: Internal Categories.

Nathanael Arkor (Oct 01 2024 at 10:03):

Vincent Moreau said:

Side question: is it OK to ask that kind of question here? I have been posting a few ones and I just want to make sure this is the right place.

Yes, this is exactly the place for them!

Vincent Moreau (Oct 01 2024 at 10:04):

Thanks!

Nathanael Arkor (Oct 01 2024 at 10:11):

Vincent Moreau said:

I don't really see where the general case is proven in the two references given. What do you think about all that?

As far as I can see, their statements both look a little different to the one stated on the nLab, in that they only emphasise the cartesian closure aspect. Johnstone's statement is this:
image.png

While the Ehresmanns' statement is:
image.png
image.png

They have stronger assumptions in their proposition statement, but they're not needed for the first bullet point (see the proof of Proposition 25).

Vincent Moreau (Oct 01 2024 at 10:25):

While I'm at it, I don't understand the use of the category $\Delta_3$ in the proof of the nlab. At least in the case of categories internal to sets, $\Delta_2$ is already dense because $[2]$ captures the composition of morphisms, so the nerve functor is full and faithful. Is $\Delta_3$ necessary for the more general situation?

Adrian Miranda (Oct 01 2024 at 10:27):

Associativity requires an equation on maps [3] --> [1].

Vincent Moreau said:

While I'm at it, I don't understand the use of the category $\Delta_3$ in the proof of the nlab. At least in the case of categories internal to sets, $\Delta_2$ is already dense because $[2]$ captures the composition of morphisms, so the nerve functor is full and faithful. Is $\Delta_3$ necessary for the more general situation?

Vincent Moreau (Oct 01 2024 at 10:29):

But associativity is property, not data, right? Therefore, I don't see why it should be captured to get a fully faithful nerve

Adrian Miranda (Oct 01 2024 at 10:32):

Ahh sorry I misunderstood the question. [3] is required to define categories internally, but I agree that it is not needed when defining functors.

Vincent Moreau (Oct 01 2024 at 10:32):

I see, thanks for the confirmation!

Vincent Moreau (Oct 01 2024 at 10:33):

I would therefore expect that the proof of the nlab can be adapted to $\Delta_2$... but perhaps it is more natural with $\Delta_3$ because $[3]$ indeed appears in the definition of internal categories

Adrian Miranda (Oct 01 2024 at 10:41):

I just checked the nLab page, and I agree with your and Nathanael's comments that finite limits and cartesian closedness are insufficient even for a left adjoint to Cat(E) --> Gph(E). One also needs list objects.

Vincent Moreau said:

Dear category theorists,

On the Internal category nlab page, in the "In a cartesian closed category" paragraph, it is written:

Theorem 4.1. Let $\mathbf{E}$ be a finitely complete cartesian closed category. Then the category $\mathbf{Cat}(\mathbf{E})$ of internal categories in $\mathbf{E}$ is also finitely complete and cartesian closed.

Proof. First suppose $\mathbf{E}$ is finitely complete. Then the category of directed graphs $\mathbf{E}^{\bullet \rightrightarrows \bullet}$ is also finitely complete, and since $\mathbf{Cat}(\mathbf{E})$ is monadic over $\mathbf{E}^{\bullet \rightrightarrows \bullet}$, it follows that $\mathbf{Cat}(\mathbf{E})$ is also finitely complete.

I don't understand how this argument works. I have the impression that the monadicity result relies on $\mathbf{E}$ being more than a finitely complete CCC, as there is no way to build the free internal category when $\mathbf{E}$ is $\mathbf{FinSet}$ for instance.

I don't really see where the general case is proven in the two references given. What do you think about all that?

Vincent Moreau (Oct 01 2024 at 12:34):

What is a list object? Is it an initial algebra for the endofunctor $A \times (-) + 1$ or is it defined in another way?

Adrian Miranda (Oct 01 2024 at 12:45):

That's correct. It can also be defined as the free monoid on A.

Vincent Moreau (Oct 01 2024 at 12:55):

I see, and this definition in terms of monoids does not require $(-) + 1$ to exist. I'm trying to build the object of finite paths out of a graph in $\mathbf{E}$ but it is not so clear to me for the moment how to rule out the lists of edges which do not form a path.

Adrian Miranda (Oct 01 2024 at 13:11):

Given a graph X_0 <-- X_1 --> X_0, the object of paths is formed by the equaliser of two maps X_0 * L(X_1) * X_0 --> L(X_0).

Calum Hughes and I are currently finishing off a preprint on colimits of internal categories in which there will be more details, but for now see Proposition 7.3 of this paper for the construction of free categories in list arithmetic pretoposes.

http://www.tac.mta.ca/tac/volumes/24/3/24-03abs.html

Vincent Moreau (Oct 01 2024 at 13:19):

Adrian Miranda said:

Given a graph X_0 <-- X_1 --> X_0, the object of paths is formed by the equaliser of two maps X_0 * L(X_1) * X_0 --> L(X_0).

Calum Hughes and I are currently finishing off a preprint on colimits of internal categories in which there will be more details, but for now see Proposition 7.3 of this paper for the construction of free categories in list arithmetic pretoposes.

http://www.tac.mta.ca/tac/volumes/24/3/24-03abs.html

Aaaah, that's very interesting: sending a list of morphisms on the list of their domains, and adding manually the codomain, and conversely sending a list of morphisms on the list of their codomains, and then adding the domain!

Adrian Miranda (Oct 01 2024 at 13:21):

Exactly!

Vincent Moreau (Oct 01 2024 at 13:21):

Thanks for this explanation!

Adrian Miranda (Oct 01 2024 at 13:22):

No worries! :)

John Baez (Oct 01 2024 at 17:12):

Vincent Moreau said:

Dear category theorists,

On the Internal category nlab page, in the "In a cartesian closed category" paragraph, it is written:

Theorem 4.1. Let $\mathbf{E}$ be a finitely complete cartesian closed category. Then the category $\mathbf{Cat}(\mathbf{E})$ of internal categories in $\mathbf{E}$ is also finitely complete and cartesian closed.

Proof. First suppose $\mathbf{E}$ is finitely complete. Then the category of directed graphs $\mathbf{E}^{\bullet \rightrightarrows \bullet}$ is also finitely complete, and since $\mathbf{Cat}(\mathbf{E})$ is monadic over $\mathbf{E}^{\bullet \rightrightarrows \bullet}$, it follows that $\mathbf{Cat}(\mathbf{E})$ is also finitely complete.

I don't understand how this argument works. I have the impression that the monadicity result relies on $\mathbf{E}$ being more than a finitely complete CCC, as there is no way to build the free internal category when $\mathbf{E}$ is $\mathbf{FinSet}$ for instance.

As others have already said, you're right: this proof needs to be fixed.

Since I'm a lowbrow sort of guy, I might try to construct binary products, equalizers and the terminal object in $\mathbf{Cat}(\mathbf{E})$ explicitly. Binary products seem really easy: given two internal categories $X$ and $Y$ I'd build their product by taking

$\mathrm{Ob}(X \times Y) = \mathrm{Ob}(X) \times \mathrm{Ob}(Y)$

and similarly

$\mathrm{Mor}(X \times Y) = \mathrm{Mor}(X) \times \mathrm{Mor}(Y)$

etc. I'd try building equalizers in a similar way: define the object of objects to be the obvious equalizer, ditto for the object of morphisms, etc. And the terminal internal category has $1 \in \mathbb{E}$ as its object of objects and $1$ as its object of morphisms.

Unless I'm missing something (always possible) the whole proof would have a kind of boringly mindless feel to it. We're just copying the limits in $\mathbf{E}$ to get those in $\mathbf{Cat}(\mathbf{E})$.

This suggests that something deeper is at work, which a more high-powered proof would exploit. Something about why the forgetful functor from $\mathbf{Cat}(\mathbf{E})$ to $\mathbf{E}^{\bullet \rightrightarrows \bullet}$ creates limits. But my main point is that the result:

$\mathbf{E}$ is finitely complete $\implies$ $\mathbf{Cat}(\mathbf{E})$ is finitely complete

doesn't feel deep: you could probably just prove it yourself.

Adrian Miranda (Oct 01 2024 at 17:20):

Agreed. All constructions for (2-)limits in Cat(E) follow by yoneda, with the same constructions as in the case E= Set. Colimits of internal categories are a bit more subtle. Coproducts and copowers by 2 are treated in the preprint below (accepted for publication in the TAC special edition for Lawvere), while coequalisers will be treated in our follow up paper which should be ready for the arXiv soon.

https://arxiv.org/abs/2403.03647

John Baez said:

Vincent Moreau said:

Dear category theorists,

On the Internal category nlab page, in the "In a cartesian closed category" paragraph, it is written:

Theorem 4.1. Let $\mathbf{E}$ be a finitely complete cartesian closed category. Then the category $\mathbf{Cat}(\mathbf{E})$ of internal categories in $\mathbf{E}$ is also finitely complete and cartesian closed.

Proof. First suppose $\mathbf{E}$ is finitely complete. Then the category of directed graphs $\mathbf{E}^{\bullet \rightrightarrows \bullet}$ is also finitely complete, and since $\mathbf{Cat}(\mathbf{E})$ is monadic over $\mathbf{E}^{\bullet \rightrightarrows \bullet}$, it follows that $\mathbf{Cat}(\mathbf{E})$ is also finitely complete.

I don't understand how this argument works. I have the impression that the monadicity result relies on $\mathbf{E}$ being more than a finitely complete CCC, as there is no way to build the free internal category when $\mathbf{E}$ is $\mathbf{FinSet}$ for instance.

As others have already said, you're right: this proof needs to be fixed.

Since I'm a lowbrow sort of guy, I might try to construct binary products, equalizers and the terminal object in $\mathbf{Cat}(\mathbf{E})$ explicitly. Binary products seem really easy: given two internal categories $X$ and $Y$ I'd build their product by taking

$\mathrm{Ob}(X \times Y) = \mathrm{Ob}(X) \times \mathrm{Ob}(Y)$

and similarly

$\mathrm{Mor}(X \times Y) = \mathrm{Mor}(X) \times \mathrm{Mor}(Y)$

etc. I'd try building equalizers in a similar way: define the object of objects to be the obvious equalizer, ditto for the object of morphisms, etc. And the terminal internal category has $1 \in \mathbb{E}$ as its object of objects and $1$ as its object of morphisms.

Unless I'm missing something (always possible) the whole proof would have a kind of boringly mindless feel to it. We're just copying the limits in $\mathbf{E}$ to get those in $\mathbf{Cat}(\mathbf{E})$.

This suggests that something deeper is at work, which a more high-powered proof would exploit. Something about why the forgetful functor from $\mathbf{Cat}(\mathbf{E})$ to $\mathbf{E}^{\bullet \rightrightarrows \bullet}$ creates limits. But my main point is that the result:

$\mathbf{E}$ is finitely complete $\implies$ $\mathbf{Cat}(\mathbf{E})$ is finitely complete

doesn't feel deep: you could probably just prove it yourself.

Vincent Moreau (Oct 01 2024 at 20:36):

Thanks for your message John! Indeed, the "usual suspects" seem to work out just fine. I have another proposition of explanation for that: internal categories are models of an essentially algebraic theory. This means that the category $\mathbf{Cat}(\mathbf{E})$ of internal categories is the category of finite limit-preserving functors

$$L_{\mathbf{Cat}} \ \longrightarrow\ \mathbf{E}$$

and we see that it is finitely complete, with the limits computed pointwise!

Nathanael Arkor (Oct 01 2024 at 22:00):

Nathanael Arkor said:

I don't know why monadicity is mentioned; the fact that Cat(E) inherits limits from E follows from the fact that Cat(E) is a category of finite limit preserving functors, in which limits are given pointwise.

This is what I said earlier :)

Vincent Moreau (Oct 01 2024 at 22:14):

Oops, indeed, how embarrassing....