Stable unions without stable images

Question

A regular category is one with finite limits and pullback-stable images (i.e. (regular epi, mono) factorizations). A coherent category is a regular category that also has pullback-stable finite unions of subobjects (monomorphisms). These two classes of categories correspond to fragments of first-order logic containing $\wedge,\top,\exists$ and $\wedge,\top,\vee,\bot,\exists$ respectively.

But what about categories corresponding to a fragment containing only $\wedge,\top,\vee,\bot$? Are there naturally-ocurring examples of categories having finite limits and pullback-stable unions of subobjects but not pullback-stable images?

Answer 1

Here's another example, inspired by aws's but not involving any computability. Let $A$ be a distributive lattice and let $\mathrm{Fam}(A)$ be the free coproduct-completion of $A$, whose objects are families $\{a_i\}_{i\in I}$ of elements of $A$ and whose morphisms $\{a_i\}_{i\in I} \to \{b_j\}_{j\in J}$ are functions $f:I\to J$ such that $a_i \le b_{f(i)}$.

Then $\mathrm{Fam}(A)$ has finite limits (given by limits in $\mathrm{Set}$ and meets in $A$) and pullback-stable finite unions (given by unions in $\mathrm{Set}$ and joins in $A$; distributivity of $A$ is needed to make these pullback-stable). Its monomorphisms are arbitrary morphisms whose underlying set-function is injective. But it doesn't have images unless $A$ is a complete lattice; the image of the unique map from any family $\{a_i\}_{i\in I}$ to the terminal object would have to be the one-element family on a join of all the $a_i$.

Answer 2

I'm not sure if this example counts as natural, but one possibility is to adjust the definition of category of assemblies to use only finite existence predicates.

An assembly is a set $X$, together with a function $E : X \rightarrow \mathcal{P}^\ast(\mathbb{N})$, which is called the existence predicate of the assembly. ($\mathcal{P}^\ast$ denotes inhabited subsets and strictly speaking the definition is more general and this is the special case for the pca $\mathcal{K}_1$). A morphism from $\langle X, E \rangle$ to $\langle Y, F \rangle$ is a function $g: X \rightarrow Y$ such that there exists a computable function $\phi_e$ such that for all $x \in X$ and all $n \in E(x)$, $\phi_e(n)$ is defined and belongs to $F(g(x))$.

Say that an assembly $\langle X, E \rangle$ has finite existence predicate if for all $x \in X$, $E(x)$ is a finite set. I claim that the full subcategory of assemblies with finite existence predicates is as required.

The initial object $\bot$, is given by the empty set. The terminal object $\top$, is given by a singleton $\{\ast\}$ together with existence predicate given by $E(\ast) = \{0\}$. Pullbacks are defined the same as for the category of assemblies.

Note that a monomorphism $g : \langle X, E \rangle \rightarrow \langle Y, F \rangle$ is in particular injective as a function $X \rightarrow Y$, so we may assume without loss of generality that $X$ is a subset of $Y$. The union of two monomorphisms $\langle X, E \rangle \rightarrow \langle Y, F \rangle$ and $\langle X', E' \rangle \rightarrow \langle Y, F \rangle$ is given by the union of underlying sets $X'' := X \cup X'$, together with existence predicate given by $E''(x) := \{ (0, n) \;|\; n \in E(x) \} \cup \{ (1, n) \;|\; n \in E'(x) \}$ (where $(,)$ denotes a computable encoding of pairs of natural numbers as natural numbers).

Now to show that the category does not have images. Let $T$ be the set of numbers $e$ such that $\phi_e$ is a total computable function. We make this into an assembly by defining existence predicate $E(e) := \{e\}$. Then consider the assembly with underlying set $\mathbb{N}^\mathbb{N}$ and existence predicate $F(f) := \{0\}$. Then I claim the morphism $T \rightarrow \mathbb{N}^\mathbb{N}$ sending a code for a total computable function to the underlying function, does not have a regular epi-mono factorisation.

In the category of all assemblies, the factorisation would be as follows. The underlying set of the object in the middle would be the set of computable functions (the actual functions, not codes for functions). The existence predicate would be given by $G(f) = \{ e \in \mathbb{N} \;|\; f = \phi_e \}$. One can show with a little work that the inclusion functor of assemblies with finite existence predicate into all assemblies preserves coequalizers, and so also regular epimorphisms. It also preserves monomorphisms and so also image factorisations. However, since image factorisations are unique up to isomorphism, this would yield an assembly with finite existence predicate which is isomorphic to the assembly described above. This then gives a contradiction, because it would allow us to compute whether or not a total computable function is equal to the function constantly equal to $0$, and so compute the halting set.