Sheaf toposes and chain-complete posets
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/ ]
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/ ]
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/ ]
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/ ]
participants (3)
-
Andrej Bauer -
Fred E.J. Linton -
Sam Staton