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$
    – Todd Trimble
    Sep 15, 2012 at 1:22
  • 1
    $\begingroup$ Nice solution, by the way! $\endgroup$
    – Todd Trimble
    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$ Sep 16, 2012 at 16:58
  • $\begingroup$ @AndrejBauer Which topoi do LLPO fail? Is there an essential structure? $\endgroup$
    – VS.
    Dec 22, 2019 at 13:21
  • $\begingroup$ Interesting question! The analytic LLPO fails in sheaves on $[0,1]$. Let me think. $\endgroup$ Dec 23, 2019 at 14:23

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.