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.)

  • 2
    $\begingroup$ Just to point out a few models where SVC fails: Monro's model with Dedekind-finite sets; the Morris model (on which I recently wrote a paper); the Bristol model (on which I recently wrote a paper); the Gitik model; any model where there is a class-length product of localized failures of choice, e.g. the model in which Fodor's lemma fails everywhere (on which I recently wrote a paper) or models where you can embed every well-orderable partial order into the cardinals (on which I wrote my first paper). While we're at it, Blass' gave a few models where SVC fails in that paper. $\endgroup$ – Asaf Karagila Aug 27 '19 at 19:43
  • 1
    $\begingroup$ Also, it is necessary to use class forcing for these kind of constructions—when starting from ZFC—because when you take a symmetric extension, the full generic extension is generic over the resulting model, so you can certainly force AC, which means that SVC holds. $\endgroup$ – Asaf Karagila Aug 27 '19 at 19:52
  • 1
    $\begingroup$ @AsafKaragila No, I'm not just asking about models of ZF where SVC fails; I'm asking about Grothendieck toposes where it fails. If you don't know what a Grothendieck topos is, you can think of it as a category-theoretic version of the forcing model over a set-sized site (mathoverflow.net/q/13480/49). Note that when we allow arbitrary sites, the result in general models only IZF rather than ZFC. $\endgroup$ – Mike Shulman Aug 28 '19 at 0:11
  • 1
    $\begingroup$ Regarding SVC holding in symmetric extensions, I am on my way to sleep, so I might write something tomorrow morning. But the gist is that symmetric extensions via set forcings only "ruin choice with a set", and it turns out that the full generic extension from whence they came can be recovered by a forcing again. Therefore SVC holds. On the other hand, when you're doing something class-sized (such as those models I've mentioned), then you cannot force choice back with just a set, since you have a proper class of counterexamples. I will maybe write something in the morning... $\endgroup$ – Asaf Karagila Aug 28 '19 at 0:16
  • 3
    $\begingroup$ @MikeShulman Yes. The problem is that, in a non-Boolean world, there's severe shortage of such objects. For example, the obvious ordering of a $2$-element set has the least-element property iff the topos is Boolean. $\endgroup$ – Andreas Blass Aug 28 '19 at 11:19

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.

  • 1
    $\begingroup$ Interesting. So it seems that WISC (which does hold in all Grothendieck toposes, and even realisability toposes, IIRC, assuming it holds in Set) really is a weaker assumption, and from one point of view a workable replacement for SVC in the non-boolean setting. $\endgroup$ – David Roberts Aug 28 '19 at 4:11
  • 1
    $\begingroup$ Great answer, thanks. This suggests the natural followup question: "Does SVC hold in all Boolean Grothendieck toposes?" Asaf's comments above suggest that perhaps the answer to this question is yes. $\endgroup$ – Mike Shulman Aug 28 '19 at 16:34
  • 1
    $\begingroup$ And the other follow up question: "Does SVC hold in any non-boolean Grothendieck topos ?" there are Grothendieck topos with very large Boolean open subtopos where it is not so clear that the same kind of arguement can be used (for example in the Stone-Cech compactification of a discrete set $D$, $D$ is a dense discrete open subspace) $\endgroup$ – Simon Henry Aug 28 '19 at 16:57
  • $\begingroup$ @MikeShulman : regarding your follow up question, I could be wrong, but I have the impression that in a Boolean Grothendieck topos every constant sheaf is a choice object (but I haven't been to prove it). That would show that they alll satisfies SVC by taking "$S$'' to be any bound $\endgroup$ – Simon Henry Aug 29 '19 at 19:17
  • 1
    $\begingroup$ Blass proved that SVC for ZF is equivalent to the existence of a forcing extension in which AC holds. I wonder whether SVC for a (perhaps Boolean) Grothendieck topos $E$ is similarly equivalent to the existence of a bounded $E$-topos satisfying AC. $\endgroup$ – Mike Shulman Aug 30 '19 at 0:17

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.