Failure of SVC in Grothendieck toposes

Question

The axiom SVC (for "small violations of choice") asserts that there is a set $S$ such that for every set $X$ there is a choice set $A$ such that $X$ is a subquotient of (i.e. admits a surjection from a subset of) $A\times S$.

The original formulation of Blass (Injectivity, projectivity, and the axiom of choice) took $A$ to be an ordinal and the subquotient to be a surjection, which are equivalent in the presence of excluded middle; but the above version seems arguably more natural in intuitionistic logic. Blass showed that many models of set theory satisfy SVC, including permutation and symmetric models, $L(T)$, and ${\rm HOD}(T)$, but that SVC is not a consequence of ZF because it can fail in a class-forcing model.

In Avoiding the axiom of choice in general category theory, Makkai remarks (p171) that "direct topos-theoretic translates" of SVC do not hold in all Grothendieck toposes. This is intriguing because Grothendieck toposes are a rough category-theoretic correspondent of (ordinary, set-based, intuitionistic) forcing models; and if SVC can be violated in an ordinary forcing model, why did Blass have to recourse to a class-forcing model to prove its independence? Unfortunately, Makkai gives no examples or explanation.

So: what is an example of a Grothendieck topos (defined over a base model of ZFC) in whose internal logic the SVC fails? (An ordinary forcing model in which it fails would be interesting enough, although since a forcing model doesn't necessarily coincide exactly with its corresponding topos it might not quite answer the question yet.)

Answer 1

It seem to me that the problem that Makkai has in mind is that the existence of non-trivial choice objects is in conflict with non-booleaness.

The core of the arguement, is the following lemma, which essentially follows from Diacunescu's proof that $AC \Rightarrow LEM$:

Lemma: Let $A$ be a choice object in a topos, then internally:

$$ \forall x,y \in A, \forall U \in \Omega, (U \Rightarrow (x=y)) \cup U $$

Remark: that is basically a rephrasing of lemma D4.5.11 of P.T.Johnstone sketches of an elephant.

Proof: Let $A$ be a choice object and $x, y \in A$. Let $U$ be any proposition, consider the set $1 \coprod_U 1$ and the relation that send the first component to $x$ and the second to $y$ (and to both for element that are in both component). It is an entire relation to $A$, so there is function $1 \coprod_U 1 \rightarrow A$ included in that relation, in particular which takes values in $\{x,y\}$. I'm calling $a$ and $b$ the "two" elements of $1 \coprod_U 1$, I have four case to deal with regarding the values of $a$ and $b$ by this functions, but in each of them you can either prove $U$ or $U \Rightarrow (x,y)$:

• $a \mapsto x$ and $b \mapsto y$ then $U \Rightarrow (x=y)$

• $a \mapsto y$ then $U$

• $b \mapsto x$ then $U$ $\square$

Geometrically speaking, this is a pretty rough restriction on what can choice objects be ! it means that if $A$ is a choice object in a topos $\mathcal{T}$, and $a,b$ are two section of $A$ on $X$, then the closed complement of $(x=y)$ in $\mathcal{T} / X$ is Boolean. So either $A$ is very close to be subterminal, or the slices of $\mathcal{T}$ have some large boolean closed subtoposes. (this is the conflict I was referring to at the begining)

But one can do better:

Proposition: Let $\mathcal{T}$ be a Grothendieck topos which:

• Is nowhere boolean, i.e. no non-degenerate slice of $\mathcal{T}$ is boolean,

• satisfies SVC,

then $\mathcal{T}$ is degenerate. For example, $Sh([0,1])$ do not satisfies SVC.

Note that a nowhere boolean topos is a topos where LEM is internally false, in the sense that the interpretation of "$\forall U, U \cup \neg U$" in the internal logic is $\bot$ (the initial object).

We start with another lemma:

Lemma: In a nowhere boolean topos, if $A$ is a choice object and $D$ is decidable object (i.e. internally $\forall x,y \in D, x=y \cup x \neq y$) then one can internally show that:

$$ \texttt{Any partial map $A \rightarrow D$ is constant} $$

Indeed, consider internally a partial map $f:A \rightarrow D$, for each $a , a'$ in the domain of definition of $f$, either $f(a)=f(a')$ or $f(a) \neq f(a')$, but $f(a) \neq f(a')$ implies $a \neq a'$, which internally implies LEM by the previous lemma, which is false as $\mathcal{T}$ is nowhere boolean. Hence the result.

One can now prove the proposition: If one assumes further that $\mathcal{T}$ satisfies SVC, it means that every decidable object of $\mathcal{T}$ is a subquotient of the object $S$ (as the lemma above implies that the partial map $S \times A \rightarrow D$ is constant in the $A$-direction). But if $\mathcal{T}$ is non degenerate, for $\kappa$ large enough (larger than the size of the site and the size of $S$), the object $p^* \kappa$ is locally decidable and of size $\kappa$, so it cannot be a subquotient of $S$.

Edit: My apologies for the needlessly non mathematical and complicated first answer. I think I found the theorem I was after.