5
$\begingroup$

(My apologies if this is well-known: I feel that I'm missing something very obvious here.)

Basic question: Do filtered colimits exist in the effective topos?

The reason I feel I'm missing something very obvious is that Jaap van Oosten wrote en entire paper titled “Filtered colimits in the effective topos” (also pretty much reproduced as §3.8.2 of his book Realizability: An Introduction to its Categorical Side), whose title suggests that the answer should definitely be there if it's not obvious in the first place, but… I can't find anything about the existence of filtered colimits in the paper in question. There is an example (proposition 1.3 in the paper, 3.8.3 in the book) which shows that $\nabla\colon \mathrm{Set} \to \mathrm{Eff}$ doesn't preserve the colimit of the diagram of finite subsets $S \subseteq \mathbb{N}$ with inclusions between them, but that $\varinjlim(\nabla S)$ does not equal $\nabla\mathbb{N}$ doesn't tell me the former doesn't exist in $\mathrm{Eff}$. But van Oosten doesn't clarify the issue one way or another.

Extended question: Assuming the answer to the basic question is “no”, are there some interesting conditions that we can put either on the objects, or on the maps, or on the indexing system, or some combination thereof, that ensures the filtered colimit exists? For example, does the colimit of a system indexed by a totally ordered set whose transition maps are monomorphisms exist in $\mathrm{Eff}$?

$\endgroup$
1
  • 3
    $\begingroup$ A not-quite answer is that if the diagram is internalisable then a colimit (in the internal sense) exists. $\endgroup$
    – Zhen Lin
    Jun 3, 2023 at 0:24

1 Answer 1

8
$\begingroup$

There are probably easier ways to see this, but my favourite example is to look at the filtered colimit over all finite coproducts of $1$ with inclusions. We can also view this as a countable sequence $1 \,\hookrightarrow\, 1 + 1 \,\hookrightarrow\, 1 + 1 + 1 \,\hookrightarrow\, \ldots$. We can show that this colimit, if it exists, is also the coproduct of countably many copies of 1, i.e. $\coprod_{n \in \mathbb{N}} 1$. We can show in general that whenever this coproduct exists, it is necessarily a natural number object, and so since natural number objects are unique up to isomorphism, it is isomorphic to any other natural number object. If the coproduct $\coprod_{n \in \mathbb{N}} 1$ exists, we can also take any external function $\mathbb{N} \to \mathbb{N}$, including any non computable function, and view it as a morphism $\coprod_{n \in \mathbb{N}} 1 \to \coprod_{n \in \mathbb{N}} 1$ inside the category. With some more work, we can furthermore show in any lcc that e.g. if we take the external characteristic function for the halting set, then the corresponding morphism $\coprod_{n \in \mathbb{N}} 1 \to \coprod_{n \in \mathbb{N}} 1$ is also the characteristic function for the halting set in the internal logic.

In short, just by knowing that the colimit exists, we can introduce non computable functions into any lcc. In the effective topos, the only endomorphisms on the natural number object $N \to N$ are computable, and in fact we furthermore have the axiom of Church's Thesis in the internal logic: all functions $N \to N$ are computable. Hence this gives a simple example of a filtered colimit that does not exist in $\mathrm{Eff}$. But moreover, I see the tight correspondence between morphisms in the topos and computable functions as a fundamental property of $\mathrm{Eff}$ and we can see that any other lcc with this same nice property would lack the same colimit for the same reason.

$\endgroup$
5
  • 1
    $\begingroup$ (I suppose you meant to write $\coprod$ (i.e., \coprod) rather than $\prod$.) This does put a damp on the hopes of getting interesting conditions for a filtered colimit to exist. But now I wonder if $N$ can be described as something weaker-than-a-colimit-but-nevertheless-interesting in this situation $1 \to 1+1 \to 1+1+1 \to \cdots \to N$. $\endgroup$
    – Gro-Tsen
    Jun 2, 2023 at 22:09
  • $\begingroup$ I better edit to fix the prod/coprod. $\endgroup$
    – aws
    Jun 2, 2023 at 22:17
  • 3
    $\begingroup$ I always found it most useful to do everything internal to the topos - in the internal logic $N$ does just look like the coproduct of countably many $1$s. Aside from that, I don't know of any formal way to view $N$ as a generalisation of colimit. It's an interesting question. $\endgroup$
    – aws
    Jun 2, 2023 at 22:21
  • $\begingroup$ The natural numbers cannot be defined as a colimit without first having the natural numbers. This circularity is one of the reasons finitists reject it ("completed infinity"). $\endgroup$
    – Zhen Lin
    Jun 3, 2023 at 5:38
  • $\begingroup$ I tried to write a followup question to try to make sense of this answer, but I'm not sure it turned out very sensibly. $\endgroup$
    – Gro-Tsen
    Jun 3, 2023 at 9:42

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.