home *** CD-ROM | disk | FTP | other *** search
- Newsgroups: sci.math
- Path: sparky!uunet!zaphod.mps.ohio-state.edu!caen!destroyer!ubc-cs!unixg.ubc.ca!pruss
- From: pruss@unixg.ubc.ca (Alexander Pruss)
- Subject: Re: Topos not over SET with natural number system?
- Message-ID: <1992Jul24.191021.3095@unixg.ubc.ca>
- Keywords: elementary topos, natural number system, SET
- Sender: news@unixg.ubc.ca (Usenet News Maintenance)
- Nntp-Posting-Host: unixg.ubc.ca
- Organization: University of British Columbia, Vancouver, B.C., Canada
- References: <1992Jul23.213112.5122@unixg.ubc.ca>
- Date: Fri, 24 Jul 1992 19:10:21 GMT
- Lines: 30
-
- In article <1992Jul23.213112.5122@unixg.ubc.ca> I write:
- >Can there exist a topos not defined over SET with a natural number
- >system? If so, what would be an example?
-
- [Someone noted I should have said "elementary" topos to distinguish
- from a Grothendieck topos.]
-
- Sorry to have bothered people with this.
-
- There is indeed a fairly simple topos with this property.
-
- Let Z be any set. We define the category SETZ to be the full subcategory
- of SET with objects being sets of cardinality <= P^n Z for some natural
- number n. (P^n Z= P...PZ with n P's, where for any set A, PA is its power
- set.) Then it is very easy to see SETZ is a topos.
-
- If Z is infinite, then SETZ clearly contains an infinite object, and so a
- natural number system.
-
- Now, SETZ is not defined over SET, as we can easily verify there is no
- K-indexed coproduct of 1={0} in SETZ if K is a set of cardinality strictly
- greater than any P^n Z. (E.g. K = union(P^n Z), the union being taken
- over natural n.)
-
- SETZ is a really nice topos. For Z=0, it is the degenerate topos. For
- Z finite, it is FINSET. For Z infinite it has a natural number system.
- It is never defined over SET, but nonetheless has many of the properties
- of SET, and seems to be a generalization of FINSET. It is Boolean,
- bivalent, extensional, any object A not isomorphic to 0 has an arrow
- 1-->A, and has the axiom of choice (if SET is assumed to have it).
-