12
$\begingroup$

It's a ZFC theorem of Freyd, any small complete category is a preorder. Freyd's theorem continues to hold in any Grothendieck topos. But Hyland showed it fails in some elementary toposes.

I don't actually know, but I suspect that Hyland's topos examples don't readily translate into models of ZF — toposes don't play well with replacement. So

Question: Does Freyd's theorem hold in ZF?

That is, in ZF is every small complete category a preorder?

$\endgroup$
1
  • 5
    $\begingroup$ An article by Claire Kouwenhoven-Gentil and Jaap van Oosten gives a way how to construct a model of IZF, an intuitionistic version of ZF, from the effective topos. So I think the problematic part is not Replacement. (To be fair, however, their construction uses an inaccessible cardinal.) $\endgroup$
    – Hanul Jeon
    Jul 20, 2019 at 18:13

1 Answer 1

20
$\begingroup$

Yes, Freyd's theorem holds in ZF. The theorem relies on excluded middle, choice does not play a role. Just to be sure, let's work with excluded middle but without choice.

Theorem: A small-complete small category is a preorder.

Proof. Let $C$ be a small-complete small category, with $C_0$ the set of objects and $C_1$ the set of morphisms. Consider any $x, y \in C_0$. We need to show that the set of morphisms $C(x,y)$ contains at most one element. For this purpose, suppose $r_0 : x \to y$ and $r_1 : x \to y$. By excluded middle it suffices to show that $r_0 \neq r_1$ leads to a contradiction. So assume $r_0 \neq r_1$, and define $z = \prod_{C_1} y$, the $C_1$-fold product of $y$'s. Note that a morphism $h : x \to z$ is given as a $C_1$-indexed family $h = \langle h_f \rangle_{f \in C_1}$ of morphisms $h_f : x \to y$.

Define the map $i : \{0,1\}^{C_1} \to C_1$ by $$i(c) = \langle r_{c(f)}\rangle_{f \in C_1} : x \to z.$$ we claim that $i$ is injective, which is impossible because it would give us a surjection $C_1 \to \{0,1\}^{C_1}$ by excluded middle, contradicting Cantor's theorem (which is constructive). To see that $i$ is injective, suppose $i(c) = i(d)$. Then $r_{c(f)} = r_{d(f)}$ for all $f \in C_1$, but since $r_0 \neq r_1$ it follows that $c(f) = d(f)$ for all $f \in C_1$ (no excluded middle here because equality on $\{0,1\}$ is decidable), hence $c = d$. $\Box$

In the above proof there two applications of excluded middle: concluding $r_0 = r_1$ from $\lnot\lnot (r_0 = r_1)$, and obtaining a surjection $C_1 \to \{0,1\}^{C_1}$ from an injection $\{0,1\}^{C_1} \to C_1$. As far as I can tell, both are necessary. And we never used choice.

$\endgroup$
1
  • 7
    $\begingroup$ Also note we never used replacement, the proof works in any Boolean topos. $\endgroup$ Jul 20, 2019 at 18:32

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.