Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
Does the effective topos (and realisability toposes more generally) come with a geometric morphism to $Set$? I think it doesn’t, but I’m struggling to find a proof of this fact.
You are correct, it doesn’t. Instead it comes with a geometric morphism from Set: the global sections functor has a right adjoint rather than a left adjoint.
I’m not an expert in realizability toposes, so I don’t know offhand the easiest proof that no left adjoint exists. My instinct would be to try to derive a contradiction from the existence of a coproduct of uncountably many copies of 1.
Here is the argument presented by Johnstone:
Remark F2.2.19. (b) […] $\mathbf{Eff}(\Lambda)$ cannot admit any geometric morphism to a Boolean topos, for any (nontrivial) $\Lambda$. For if such a morphism $f : \mathbf{Eff}(\Lambda) \to \mathcal{B}$ existed, we could take it to be surjective by A4.5.22; and then since all objects of the form $f^* B$ would be (decidable, and hence) modest, the cardinality of any hom-set $\mathcal{B}(B, B')$ would have to be bounded by that of $\Lambda$. But, for any set $A$, we have $\mathcal{B}(1, f_* (\nabla A)) \cong \mathbf{Eff}(\Lambda)(1, \nabla A) \cong A$.
(An assembly $(A, \alpha)$ is modest if the relation $\alpha : A \looparrowright \Lambda$ is the opposite of a partial function $\Lambda \mathrel{⇁} A$.)
But what if Set is not Boolean? (-:
Well, for my purposes I am assuming it to be so, answering my underlying question.
1 to 5 of 5