7
$\begingroup$

Let $A$ and $B$ be objects in a topos $\mathcal{E}$ with natural numbers object $\mathbb{N}$. If there is a monomorphism $m: \mathbb{N}\rightarrow A\times B$, is it necessarily the case that there is either a monomorphism from $\mathbb{N}$ to $A$ or a monomorphism from $\mathbb{N}$ to $B$?

This is clearly true when $\mathcal{E}$ is Boolean, although the proof I've seen is more involved than one might expect. It freely uses the Boolean assumption in several places.

$\endgroup$

1 Answer 1

10
$\begingroup$

Let us call an object $A$ infinite if there is a monomorphism $\mathbb{N} \to A$. Your question then asks whether $A$ or $B$ must be infinite in order for $A \times B$ to be infinite.

From now on we argue in the internal language of a topos. I am going to show that the Lesser Limited Principle of Omniscience (LLPO), which does not hold in all toposes and is a particular instance of the Law of excluded middle, follows from the statement

For all subobjects $A, B \subseteq \mathbb{N}$, if $A \times B$ is infinite then $A$ or $B$ is infinite.

LLPO can be stated as follows: given two infinite binary sequences such that not both of them contain a 1, then one or the other does not contain a 1.

So assume the statement and suppose $f, g : \mathbb{N} \to \lbrace 0, 1 \rbrace$ are sequences as in the premise of LLPO. Define the sets $A$ and $B$ by $$A = \lbrace n \in \mathbb{N} \mid \forall k < n . f(k) = 0 \rbrace$$ and $$B = \lbrace n \in \mathbb{N} \mid \forall k < n . g(k) = 0 \rbrace$$ We claim that $A \times B$ is infinite. Define the sequences $a : \mathbb{N} \to A$ and $b : \mathbb{N} \to B$ by $$a_n = \begin{cases} n, & \forall k < n . f(k) = 0\\\\ k, & k < n \land f(k) = 1 \land \forall j < k . f(j) = 0 \end{cases}$$ and $$b_n = \begin{cases} n, & \forall k < n . g(k) = 0\\\\ k, & k < n \land g(k) = 1 \land \forall j < k . g(j) = 0 \end{cases}$$ Notice that $a_m = a_n$ and $m \neq n$ imply that $f(k) = 1$ for some $k \leq \min(m,n)$, and a similar observation holds for the other sequence. The sequence $n \mapsto (a_n, b_n)$ clearly takes values in $A \times B$. It is injective because $(a_m,b_m) = (a_n, b_n)$ and $m \neq n$ imply that both $f$ and $g$ contain a 1, contrary to the premise of LLPO. Therefore, $A \times B$ is infinite and by the statement $A$ or $B$ is infinite. If $A$ is infinite then $f$ does not contain a 1, and if $B$ is infinite then $g$ does not contain a 1.

In summary, the answer to your question is negative because the statement implies LLPO, which is not valid in every topos. In particular, LLPO is violated in the effective topos.

I do not know (yet) whether LLPO implies the statement.

An obvious question to ask is whether we can positively violate the statment, i.e., can we produce two non-infinite objects $A$ and $B$ such that $A \times B$ is infinite. I would search for such objects in the effective topos, where the question will take on a recursion-theoretic flavor.

$\endgroup$
5
  • $\begingroup$ Andrej, in the first line of the definition of $a_n$, do you want to have $f(k) = 0$ instead of $f(n) = 0$? Similarly for the first line of the definition of $b_n$. $\endgroup$ Commented Sep 15, 2012 at 1:22
  • 1
    $\begingroup$ Nice solution, by the way! $\endgroup$ Commented Sep 15, 2012 at 1:29
  • $\begingroup$ Thanks! I suspected it wasn't true in general. Fortunately I only need the result in the Boolean case. Neat solution! $\endgroup$ Commented Sep 16, 2012 at 16:58
  • $\begingroup$ @AndrejBauer Which topoi do LLPO fail? Is there an essential structure? $\endgroup$
    – VS.
    Commented Dec 22, 2019 at 13:21
  • $\begingroup$ Interesting question! The analytic LLPO fails in sheaves on $[0,1]$. Let me think. $\endgroup$ Commented Dec 23, 2019 at 14:23

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .