Has there been any work done on internal categories inside internal categories?

I'm familiar with $n$-fold categories, but I don't want an internal category inside the category of internal categories in a category with pullbacks, I want an internal category inside another internal category. I can think of two approaches, but I can only work out the details fully on one of them.

The first approach externalizes an internal category, then looks at an internal category inside the externalization of this internal category. In detail:

Let $\mathcal{B}$ be a category with pullbacks and a terminal object ${\bf 1}$, hence all limits, and let ${\sf C}$ be an internal category in $\mathcal{B}$ with ${\sf Fam(C)}\to\mathcal{B}$ the internal family fibration of ${\sf C}$. Consider the fiber ${\sf Fam(C)}_{\bf 1}$ of this fibration over the terminal object in $\mathcal{B}$; we view this as an 'externalized version' of ${\sf C}$, justified by the fact that in the family fibration ${\sf Fam}(\mathcal{C})\to{\bf Set}$ of an arbitrary category $\mathcal{C}$ we have $\mathcal{C}\cong{\sf Fam}(\mathcal{C})_1$. Assume that ${\sf Fam(C)}_{\bf 1}$ has pullbacks. A ${\bf reclusive\ category}$ is an internal category inside ${\sf Fam(C)}_{\bf 1}$ for some internal category ${\sf C}$ inside a category with limits.

We can justify this approach by 'externalizing one step' and setting $\mathcal{B}={\bf Set}$, observing that a reclusive category in the category of sets is an internal category inside a category with pullbacks.

The second approach attempts to directly define an internal category inside another one without first externalizing, but I run into some issues expressing internal pullbacks; we could express commuting diagrams internally, and I know Jacob's book covers internal products and equalizers so we should be able to reconstruct internal pullbacks, but I haven't worked out the details yet. So far I have the following, using arrows out of the terminal object to select the objects and arrows we need inside the internal category:

Let $\mathcal{C}$ be a category with limits, and let ${\sf C}$ be an internal category in $\mathcal{C}$. We define a ${\bf reclusive\ category}$ $\mathscr{C}$ in ${\sf C}$ to consist of the following data:

  1. An arrow $$ {\bf Ob}_\mathscr{C}:{\bf 1}\to{\sf Ob_C}. $$
  2. An arrow $$ {\bf Hom}_\mathscr{C}:{\bf 1}\to{\sf Ob_C}. $$
  3. Two arrows $$ {\sf dom}^\mathscr{C},{\sf cod}^\mathscr{C}:{\bf 1}\to{\sf Hom_C} $$ such that the following diagrams commute

  1. An arrow $$ 1^\mathscr{C}:{\bf 1}\to{\sf Hom_C} $$ such that the following diagrams commute

  1. An arrow $$ \circ^\mathscr{C}:{\bf 1}\to{\sf Hom_C} $$ ...

This is where I have to trail off with this approach, since we would need to form an internal pullback of the selected internal object of arrows with itself over the internal object of objects, but I think this approach should be justified by the fact that if we externalize one step again by setting $\mathcal{C}={\bf Set}$ we get the same result as above (although we may need to tweak the above definition to assert that the internal category $\mathcal{C}$ has internal pullbacks). Any references or assistance are appreciated.

  • 1
    $\begingroup$ It is not clear to me what a limit of a (global) diagram in an internal category should be. For instance, consider the most trivial case, namely “the” limit of the empty diagram. Should it be a global object of the internal category, i.e. a morphism $1 \to \operatorname{ob} \mathcal{C}$, or should it be a generalised object with global support, i.e. a morphism $T \to \operatorname{ob} \mathcal{C}$ such that $T \to 1$ is a (covering) epimorphism? (Of course we also impose conditions on the object of morphisms but I omit them here.) $\endgroup$ – Zhen Lin Apr 3 at 8:39
  • 3
    $\begingroup$ Do you have an example in mind? I think it would be easier to abstract the essential features of an example of interest than to just guess a useful definition starting from nothing. So far with 1-4, it seems like you are defining an internal category in the underlying ordinary category of an internal category. $\endgroup$ – Reid Barton Apr 3 at 10:06
  • $\begingroup$ @ReidBarton I don't have any particular examples in mind, just musings about 'iterated internalization' that led to this. I'm not sure what you mean by the last part of your comment; do you mean that the second approach appears to you to be just redefining an internal category in a category? The arrows out of the terminal object are meant to be viewed as global elements of the internal categories object and arrow objects, and the commutative diagrams express domains and codomains for the global objects of the hom object. $\endgroup$ – Alec Rhea Apr 4 at 6:17
  • $\begingroup$ @ZhenLin Jacobs book covers internal limits and I had assumed this would be sufficient, although I haven't digested the material yet; is the standard notion of internal limit insufficient for the limit of globally defined diagrams in the above spirit? $\endgroup$ – Alec Rhea Apr 4 at 6:36
  • $\begingroup$ Since you write reclusive four times, it can't be a typo, so why did you choose that name? $\endgroup$ – Paul Taylor Apr 4 at 20:23

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.