Large "internal" categories and "finite" products

Question

The question is basically "do we really have a good way to talk about large categories internally in an elementary topos?"

An internal small category in a topos $E$ is just a category object in $E$.

Until now I assumed that when we want to talk about a "large" categories internally in an elementary topos $E$ we would use a stack for some appropriately chosen topology on $E$. This seems to be the commonly held point of view in every text that deals with this.

If $E$ is a Grothendieck topos, we can use the canonical topology and this works very well, which is why I never really questioned this. But for an elementary topos, using the coherent topology works decently well, but we run into a big problem with how it interacts with notions like finiteness:

For a small internal category $C \in \operatorname{Cat}(E)$ I can show "by induction" that (internally) if $C$ has a terminal object and binary products then it has finite products. Where by finite products I mean products indexed by any (Kuratowski) finite decidable object.

But if $C$ is a large category, it seems very unclear that one can do the same thing! (Or if you know how to do it, that would answer my question!)

Keep in mind that an elementary topos can have non-standard finite objects, that aren't (locally) finite coproducts of the terminal object. So these internally finite limits aren't really externally finite and something that is just a stack for the coherent topology has I think no reason to have them?

Of course, it is possible to show this sort of things for concretely defined large internal categories, like "the category of sets" or a "category of sheaves on an internal site", but don't know how to give a good definition of an "internal large category" that allows to prove this sort of results (basically being able to use induction when construction objects of the topos).

Can we come up with a good notion of "internal large category" in an elementary topos $E$ (maybe as a stack on $E$ satisfying some additional condition) that:

• includes the usual examples, like the categories of set, groups, fields, sheaves, etc…

• can be manipulated internally like a (large) category would — for example the Elephant is supposed to mostly do things that are internally valid, but it uses large categories in many places, I'd like to be able to be able to convince myself that this notion would allow to properly internalize all this.

• We can prove results like "if a category has binary products and a terminal objects then it has finite products".

For example, in set theoretic foundation that doesn't seem to be a problem: if one defines classes as formulas, then we can still construct objects and morphisms by induction without problems.

Answer 1

I think for your specific problem it suffices to add a compatibility condition between the locally internal category $\mathcal{C}$ and the NNO.

First, let me describe the case where $\mathcal{C}$ is essentially discrete, i.e. $\mathcal{C}$ is the analogue of a large set. For simplicity I will assume that $\mathcal{E}$ is locally small and $\mathcal{C}$ is fibrewise small. Then $\mathcal{C}$ is equivalent to a presheaf on $\mathcal{E}$, so we can think of it as an object in $[\mathcal{E}^\textrm{op}, \textbf{Set}]$. The compatibility condition we should demand is simply that the Yoneda embedding $\mathcal{E} \to [\mathcal{E}^\textrm{op}, \textbf{Set}]$ send the NNO in $\mathcal{E}$ to a primitive recursive NNO in some suitable subcategory of $[\mathcal{E}^\textrm{op}, \textbf{Set}]$ containing the representables and $\mathcal{C}$. It is not clear to me exactly what "suitable" should mean here – at minimum we should ask for all morphisms between representable presheaves to be included but I am not sure we can ask for it to be a full subcategory in general. (In NBG, we would need to pay attention to definability.)

The above can be rewritten in "elementary" form, avoiding the use of $[\mathcal{E}^\textrm{op}, \textbf{Set}]$ or even size assumptions: it means, for every object $T$ in $\mathcal{E}$, every object $a$ in the fibre $\mathcal{C} (T)$, and every suitable $\mathcal{E}$-indexed functor $f : h_N \times h_T \times \mathcal{C} \to \mathcal{C}$, there is a unique object $R (f, a)$ in the fibre $\mathcal{C} (N \times T)$ such that pulling back along $\langle z \circ {!}, \textrm{id}_T \rangle : T \to N \times T$ gives $a$ and pulling back along $s \times \textrm{id}_T : N \times T \to N \times T$ gives $f (s \circ p_0, p_1, R (f, a))$, where $p_0 : N \times T \to N$ and $p_1 : N \times T \to T$ are the respective projections. (I am pretending $\mathcal{C}$ is fibrewise discrete. If $\mathcal{C}$ is fibrewise essentially discrete then insert "up to unique isomorphism" in the appropriate places.)

For the case where $\mathcal{C}$ is not essentially discrete, the idea is the same: we want the NNO in $\mathcal{E}$ (which is automatically primitive recursive because $\mathcal{E}$ is cartesian closed) to still have the universal property with respect to $\mathcal{C}$ after embedding it in the 2-category of $\mathcal{E}$-indexed categories. Writing this out in elementary form is laborious but I hope you can figure out what I mean.

The point, ultimately, is that we want to use primitive recursion to construct $n$-ary products in $\mathcal{C}$ for any internal natural number $n$ in $\mathcal{E}$ (i.e. a morphism $n : T \to N$ in $\mathcal{E}$). Given $n$ objects $b$ in $\mathcal{C}$ (i.e. an object in the fibre $\mathcal{C} (K)$ where $K = \{ (m, t) : m < n (t) \} \subseteq N \times T$), define an indexed functor $f : h_N \times h_T \times \mathcal{C} \to \mathcal{C}$ as follows (omitting details): $$f (m, t, c) = \begin{cases} c \times b (m, t) & \text{ if } m < n (t) \\ c & \text{ otherwise} \end{cases}$$ Taking $a$ to be the unit in the fibre $\mathcal{C} (T)$, we get an object $R (f, a)$ in the fibre $\mathcal{C} (N \times T)$. Pulling back along $\langle n, \textrm{id}_T \rangle : T \to N \times T$ gives an object in the fibre $\mathcal{C} (T)$: this is the desired $n$-ary product.

Of course, there was nothing specific to the cartesian product in $\mathcal{C}$ in the above; the construction will work for any left-unital binary operation.

Answer 2

I believe the correct way to work with "internal large category" over an elementary topos in a way which also allows one to do those constructions makes use of a notion of definability seen in fibrations and their internal logic. When dealing with products, for example, we will want to assert that "the family of objects $X_i$ has a product" is a definable notion.

Given an elementary topos $\mathcal{B}$, we can view a large category over $\mathcal{B}$ as a grothendieck fibration $p : \mathbb{E} \to \mathcal{B}$ satisfying some conditions which make it a stack for e.g. the coherent topology.

A collection of objects $P \subseteq \operatorname{obj}(\mathbb{E})$ is said to be definable when

1. $P$ is "closed under substitution", meaning that whenever $f : Y \to X$ is a cartesian arrow and the codomain $X$ is in $P$, the domain $Y$ is also in $P$.
2. For each object $I$ of $\mathcal{B}$ and $X$ of $\mathbb{E}$, the functor $\mathcal{B}^{op} \to \mathbf{Set}$ given by $$J \mapsto \{u : J \to I \mid u^*(X) \in P\}$$ is representable. Explicitly, this means that there is a monomorphism $\theta_X : \{X \in P\} \to I$ with $\theta_X^*(X) \in P$ such that each $u : J \to I$ with $u^*(X) \in P$ factors uniquely through $\theta_X$.

This means that for each $I$-indexed object $X$ there is a predicate $(i \mapsto X(i) \in P) : I \to \Omega$, and such predicates will allow us to use the internal logic of $\mathcal{B}$ when reasoning about the property expressed by $P$. (The condition above is given as Lemma 9.6.2 in Jacob's Categorical logic and type theory; the notion is due to Benabou.)

Given a $p : \mathbb{E} \to \mathcal{B}$, one can construct a fibration $p' : \mathbb{E}' \to \mathcal{B}$ where the fibre over $I$ consists of $I$-indexed families of indexed families of objects of the "large category" $p : \mathbb{E} \to \mathcal{B}$. (The morphisms of $\mathbb{E}'$ do not matter too much; the notion of a definable subcollection depends on only the cartesian morphisms.) Now let $P$ denote the collection of those objects of $\mathbb{E}'$ which define a family that have a product -- definability of $P$ means we can form subsets in $\mathcal{B}$ based on when families of objects in the large category have a product.

When $p : \mathbb{E} \to \mathcal{B}$ is a fibration for which $P$ is definable, then for a sequence of objects $(A_i)_{i \in \mathbb{N}}$ of $\mathcal{B}$, the definition $\{n : \mathbb{N} \mid \prod_{i < n} A_i \text{ exists}\}$ actually defines a ($A_i$-parametrised family of) subset(s) of $\mathbb{N}$ in $\mathcal{B}$, and induction in $\mathcal{B}$ on this subset ensures in the usual way that if $\mathbb{E}$ has nullary and binary products then it has all finite products.

When using this technique, one has to separately postulate definability of each of the concepts they are using -- for example, I couldn't do induction on $n$ for the statement "all $n$ary products exist", as the subfamily of $\mathcal{B}$ (in the codomain fibration $\mathcal{B}^\to \to \mathcal{B}$) on objects $A$ for which all $A$-ary products exist wasn't postulated to be definable.

(The situation is of course simpler in an autological topos, as every subcollection of every large category definable in the internal logic of the topos (including over objects, which is what we need here) is definable in the sense of fibrations. There are, however, some pathological examples of fibration-definable predicates which aren't definable in the internal logic of the topos -- the two notions of definability don't coincide.)

Answer 3

This is an extended Comment, because I am sure that Simon can fill in the details to give a full Answer.

I don't believe that either Replacement or Infinity (a Natural Numbers Object) is needed.

The relevant notion of Finiteness is surely that given by Kuratowski, along with its associated Induction. Simon will be happy with the French original but I have also made an English translation. We use that intuitionistically nowadays, but decidable equality is needed for this Question and Kuratowski used Excluded Middle anyway. We don't need $\mathbb N$.

Given a small or internal category that is sufficiently rich, say with (internal) stable disjoint sums, its object-of-objects can be cut down to a Natural Numbers Object for the external category.

The analogy with Replacement is that it is often incorrectly stated (including by me) that this is about having "large" (co)limits, for example to form $\bigcup_0^\infty{\mathcal P}^n\emptyset$. However, the issue there is not forming the (col)limit but the family whose (co)limit is required. I think it is the same with this Question.

So, as Simon says, we start with a "large" category presented as a stack. That is, as a fibration ${\mathcal C}\to{\mathcal E}$ for which the fibre over $A+B$ is equivalent to the product of the fibres over $A$ and $B$. Then the binary products and coproducts in $\mathcal C$ (if they exist) are given by the left and right adjoints to substitution, with the relevant Beck--Chevalley conditions (although there are simpler ways of expressing this).

Now a family of objects in $\mathcal C$ is expressed as an object of the fibre over the relevant finite coproduct in~$\mathcal E$.

We use Kuratowski induction to show that the interated binary (co)products yield the correct (co)product for any (decidable Kuratowski-)finite family.