Subobject of a product

Question

In $\mathbf{Set}$, if $A$ and $B$ are nonempty sets, and $B'$ is a proper subset of $B$, then $A\times B'$ is a proper subset of $A\times B$. Is this true in any topos which is not degenerate? I mean, if $\mathcal{E}$ is a topos (not a degenerate topos), $A$ and $B$ are non-initial in $\mathcal{E}$ and $m:B'\rightarrowtail B$ is a subobject of $B$ which is not $1_B$ (or an isomorphism), then $1\times m:A\times B'\rightarrowtail A\times B$ is different from $1_{A\times B}$? If so, how to prove it? I have the impression it is true, but I'm not able to prove it or disprove it.

Answer 1

This is not true in general. Here are some counterexamples:

• The topos is the "two point topos" $\mathbf{Set} \times \mathbf{Set}$, $A = (\{ 0 \}, \emptyset)$, $B = (\emptyset, \{ 0 \})$, $B' = (\emptyset, \emptyset)$.
• The topos is the category of sheaves of sets on $\mathbb{R}$, $A = h_{(0, 2)}$, $B = h_{(1, 3)}$, $B' = h_{(1, 2)}$. (Here, if $U$ is an open subset of $\mathbb{R}$, $h_U$ is the unique sheaf whose sections over $V$ are $\{ 0 \}$ if $V \subseteq U$, or $\emptyset$ otherwise. You can then check that there is a unique isomorphism $h_U \times h_V \simeq h_{U\times V}$.)

What you can prove is: if there exists some test object $X$ such that $\operatorname{Hom}(X, A) \ne \emptyset$ and $\operatorname{Hom}(X, B') \ne \operatorname{Hom}(X, B)$ (where we treat $\operatorname{Hom}(X, B')$ as being a subset of $\operatorname{Hom}(X, B)$ via composition with the given monomorphism $B' \hookrightarrow B$), then $A \times B' \ne A \times B$.

Inversely, if for every $X$ in some generating set of the topos, we have that either $\operatorname{Hom}(X, A) = \emptyset$ or $\operatorname{Hom}(X, B') = \operatorname{Hom}(X, B)$, then $A \times B' = A \times B$. (Then in the case of the topos being the category of sheaves of sets on some topological space $S$, and the generating set being the set of $h_U$ for $U \subseteq S$ open, this reduces to: if for every $U$, either $A(U) = \emptyset$ or $B'(U) = B(U)$, then $A \times B' = A \times B$. Similar statements would work for a category of presheaves of sets, or for a category of sheaves on a Grothendieck site.)

---

I don't know if your treatment of topos theory includes anything about the internal language. If so, then one possible statement you can make about equality of a product in an intuitionistic type theory would look something like:

$$A : Type, B : Type, B' : P(B) \vdash (Full_A \times B' = Full_A \times Full_B) \leftrightarrow [(\exists x:A, \top) \rightarrow B' = B].$$