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 ? 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) […] cannot admit any geometric morphism to a Boolean topos, for any (nontrivial) . For if such a morphism existed, we could take it to be surjective by A4.5.22; and then since all objects of the form would be (decidable, and hence) modest, the cardinality of any hom-set would have to be bounded by that of . But, for any set , we have .
(An assembly is modest if the relation is the opposite of a partial function .)
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