Re: Sheaf toposes and chain-complete posets

Re: Sheaf toposes and chain-complete posets

[Sam Staton]

Dear Andrej, when you say "complete" but not "chain-complete", do you
mean "directed complete"?

Here is (I think) an example that is also natural and relevant.

Do you know Andy Pitts' work (with others) on Nominal Sets? The
category of nominal sets is a sheaf topos (the "Schanuel topos", it
is actually Boolean). Andy has done some domain theory in nominal
sets to model a language with dynamic allocation of fresh names,
FreshML.

Fixing an infinite set of "atoms" A, then the category of nominal
sets is a subcategory of the category of actions of the symmetric
group on A (see reference for full definition). The set of atoms has
itself a natural group action. The finite powerset of the nominal set
of atoms, ordered by inclusion, is chain complete, but not directed
complete. Any chain of finite sets can only have finite support, and
is thus necessarily finite. But the full finite powerset is itself
directed, without an upper bound.

I hope that is of some help. Best regards, Sam.

Reference: Section 3 of On a Monadic Semantics for Freshness, M. R.
Shinwell and A. M. Pitts, Theoretical Computer Science 342, 2005.
Available from Andy Pitts' web page. NB "nominal sets" are there
called "FM-sets".

The example I mention appears in Mark Shinwell's PhD thesis, The
Fresh Approach: functional programming with names and binders. http://
www.cl.cam.ac.uk/techreports/UCAM-CL-TR-618.html.


On 27 Jul 2009, at 13:45, Andrej Bauer wrote:

> Dear categorists,
>
> I am trying to wrap my mind around the concept of an (internal)
> chain-complete poset in a sheaf topos. I am failing to come up with an
> example of a poset that is chain-complete but is not complete. The
> precise definitions of "chain-complete" in the internal language are
> as follows.
>
> Suppose (P, <=) is a poset in a topos. For C in Omega^P, let chain(C)
> be the statement
>
>   forall x, y : P, (x in C and y in C) ==> (x <= y or y <= x)
>
> Then P is chain-complete if
>
>   forall C : Omega^P, chain(C) ==> exists x : P, x is the supremum
> of C
>
> where "x is the supremum of C" means the usual thing.
>
> So what does a chain-complete poset which isn't complete look like?
>
> Since I am used to arguing intuitionistically, it would help a lot if
> there were some (possibly infinitary) logical principle or schema that
> is typical of sheaf toposes -- something expressing the local nature
> of validity. Such a principle ought to be invalid in realizability
> toposes, so perhaps it should express or imply cocompleteness (with
> respect to Set). But would that be of any help for arguing in the
> internal language?
>
> With kind regards,
>
> Andrej Bauer
>

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

Re: Sheaf toposes and chain-complete posets

[Andrej Bauer]

Dear categorists,

I should have asked a different question: what does a chain-complete
_lattice_ which is not complete look like in a sheaf topos? Is there
such a thing?

(Thanks to Fred Linton who pointed out that I could just take a flat
order and multiply it with a complete one, thus gettting a poset which
has very few interesting chains but is not at all complete.)

With kind regards,

Andrej


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

Re: Sheaf toposes and chain-complete posets

[Fred E.J. Linton]

On Mon, 27 Jul 2009 05:05:59 PM EDT, Andrej Bauer <andrej.bauer@andrej.com>
asked:

> So what does a chain-complete poset which isn't complete look like?

Take the product of any nonempty discrete poset X with the ordinal 2.
Give Xx2 the "product order" ((x, a) </= (y, b) iff x=y and a </= b).
The only non-singleton nonempty chains are the subsets {x} x 2 .
Clearly each of these is complete, Xx2 is chain-complete, and yet
Xx2 is not at all complete -- not even a semilattice either way.

HTH. Cheers, -- Fred






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

Sheaf toposes and chain-complete posets

[Andrej Bauer]

Dear categorists,

I am trying to wrap my mind around the concept of an (internal)
chain-complete poset in a sheaf topos. I am failing to come up with an
example of a poset that is chain-complete but is not complete. The
precise definitions of "chain-complete" in the internal language are
as follows.

Suppose (P, <=) is a poset in a topos. For C in Omega^P, let chain(C)
be the statement

  forall x, y : P, (x in C and y in C) ==> (x <= y or y <= x)

Then P is chain-complete if

  forall C : Omega^P, chain(C) ==> exists x : P, x is the supremum of C

where "x is the supremum of C" means the usual thing.

So what does a chain-complete poset which isn't complete look like?

Since I am used to arguing intuitionistically, it would help a lot if
there were some (possibly infinitary) logical principle or schema that
is typical of sheaf toposes -- something expressing the local nature
of validity. Such a principle ought to be invalid in realizability
toposes, so perhaps it should express or imply cocompleteness (with
respect to Set). But would that be of any help for arguing in the
internal language?

With kind regards,

Andrej Bauer


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