Re: locales such that the associated topos is subdiscrete?
CAUTION: The Sender of this email is not from within Dalhousie. 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 [For admin and other information see: http://www.mta.ca/~cat-dist/ ]
CAUTION: The Sender of this email is not from within Dalhousie. 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/ ]
CAUTION: The Sender of this email is not from within Dalhousie. Dear Peter,
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.
Thanks for pointing this out but this is not the question I raised. I was rather referring to the question Martin, you and Andy raised in the second paragraph of the proof of Cor.4.2 of the paper where you introduced triposes back in 1980. Thomas [For admin and other information see: http://www.mta.ca/~cat-dist/ ]
participants (2)
-
ptj＠maths.cam.ac.uk -
Thomas Streicher