## Not signed in

Want to take part in these discussions? Sign in if you have an account, or apply for one below

## Site Tag Cloud

Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.

• CommentRowNumber1.
• CommentAuthorDavidRoberts
• CommentTimeMay 7th 2013
• (edited May 7th 2013)

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.

• CommentRowNumber2.
• CommentAuthorMike Shulman
• CommentTimeMay 7th 2013

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.

• CommentRowNumber3.
• CommentAuthorZhen Lin
• CommentTimeMay 7th 2013
• (edited May 7th 2013)

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

• CommentRowNumber4.
• CommentAuthorMike Shulman
• CommentTimeMay 7th 2013

But what if Set is not Boolean? (-:

• CommentRowNumber5.
• CommentAuthorDavidRoberts
• CommentTimeMay 8th 2013

Well, for my purposes I am assuming it to be so, answering my underlying question.