Re: locales such that the associated topos is subdiscrete?

[ptj@maths.cam.ac.uk]

On Jun 10 2020, Thomas Streicher wrote:

>As I was just told by Matias Menni an answer to my question is also
>provided in Prop.6.3.5 of Pieter Hofstra's Thesis.
>
>Maybe I should explain a bit why I asked this question. In
>arxiv:2005.06019 Jonas Frey and I have characterized triposes over a
>base topos SS as regular functors F from SS to a topos EE such that
>
>1. every object of EE appears as subquotient of some FI
>2. F^*Sub_EE admits a generic family.
>
>What we had to leave as an open question whether triposes over SS = Set
>inducing the same topos are equivalent. In Hyland, Johnstone and Pitts's
>paper introcing triposes this question was aked for localic toposes
>and remained unanswered since the last 40 years.
>Krivine's work on classical realizability has come up with an
>alternative characterization of boolean triposes over Set and he has
>shown that F : Set->EE is the inverse image part of a localic g.m. iff
>F preserves 2. But it is still open whether (boolean) triposes F : Set->EE
>with EE loclic are nevessarily isomorphic to Delta : Set -> EE.
>
>BTW if one drops condition 2 there is a simple answer. For natural
>numbers n > 0 the functors F_n : Set->Set sending X to X^n are all
>triposes in this weaker sense and pairwise not isomorphic. As explained
>in my Paper with Jonas these generalized triposes are precisely those
>introduced by Andy Pitts in his 1999 paper "Tripos Theory in Retrospect".
>In many respects this weaker notion is more natural. The only
>disadvantage is that less is expressible in the internal language of
>the base topos SS.
>
>Thomas
>
>

This is NOT an open question, despite being stated as such in Jaap van
Oosten's book; indeed, I knew the answer before Ieke raised the question at
Jaap's PhD viva (but Ieke never bothered to ask me ...). There is a proof
in my paper "Geometric morphisms of realizability toposes", TAC 28 (2013),
241.

Peter Johnstone


[For admin and other information see: http://www.mta.ca/~cat-dist/ ]