Re: locales such that the associated topos is subdiscrete?

Re: locales such that the associated topos is subdiscrete?

[Jens Hemelaer]

I do not have a reference, but I think these are precisely the complete boolean algebras.

Glue two copies of the locale X along an open subset U, and call the result  Y. Then Y can be seen as an object of Sh(X). The intersection of the two copies of X inside Y is equal to U (from one of Giraud's axioms).

On the other hand, we can write Y as a sum of open subsets of X (the "terms" of Y). And we can similarly write X as a sum of open subsets ("terms") such that each term of X gets mapped into a term of Y. Now we can compute U as the sum of those terms of X that are mapped to the same term of Y along the two inclusions in Y. The disjoint union of the other terms of X then form the complement of U.

Best regards,
Jens


---------- Forwarded message ---------
From: <streicher@mathematik.tu-darmstadt.de<mailto:streicher@mathematik.tu-darmstadt.de>>
Date: Tue, 9 Jun 2020 at 00:21
Subject: categories: locales such that the associated topos is subdiscrete?
To: <categories@mta.ca<mailto:categories@mta.ca>>


Toposes Sh(B) of sheaves over a cBa B have the property that every object
appears as sum of subterminals. Does any one know a more elementary
characterization of those cHa's A such that every object of Sh(A) appears
as sum of subterminals?
Maybe it is precisely the cBa's but I do not see how to prove it...

Thomas



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

locales such that the associated topos is subdiscrete?

[streicher]

Toposes Sh(B) of sheaves over a cBa B have the property that every object
appears as sum of subterminals. Does any one know a more elementary
characterization of those cHa's A such that every object of Sh(A) appears
as sum of subterminals?
Maybe it is precisely the cBa's but I do not see how to prove it...

Thomas



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

Re: locales such that the associated topos is subdiscrete?

[Thomas Streicher]

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/ ]

Re: locales such that the associated topos is subdiscrete?

[ptj]

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/ ]

Re: locales such that the associated topos is subdiscrete?

[Thomas Streicher]

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/ ]