* replacement and iterated powersets
@ 2008-03-16 16:25 Paul Taylor
0 siblings, 0 replies; only message in thread
From: Paul Taylor @ 2008-03-16 16:25 UTC (permalink / raw)
To: Categories list
Maybe I should wave my hands a bit less, and actually spell out a
concrete example.
Here is how you can say that the display map X-->Nx2 in an elementary
topos with a natural numbers object is the sequence of iterated
powersets, starting with X[0,0]=N, where X[0,1] is the union of X[n,0].
In set-theoretic language, X is then the cardinal beth_{omega.2}.
Of course, the following is not a CONSTRUCTION of this display map,
just a SPECIFICATION of it: we need Replacement to say that there
EXISTS a display map that satisfies this specification.
First we define the strict arithmetical order on Nx2:
(n,0) < (m,0) if n < m
(n,0) < (m,1) always
(n,1) < (m,1) if n < m
(n,1) < (m,0) never
Nx2 is also a poset, with the reflexive order <= defined as < or =.
Let D(Nx2) be the lattice of lower subsets of Nx2 wrt <=.
Let parse: Nx2 --> D(Nx2) by parse(p) = {q | q < p}.
Now let X-->Nx2 be a discrete fibration in Pos.
This means that, whenever q<=p, there is a function X[q]->X[p],
and this system respects identities and composition.
The powerset functor of the ambient elementary topos is fibred,
so we can construct another discrete fibration
Y-->D(Nx2)
in which Y[U] = colim {Y[q] | q in U}.
In particular, if U = parse (0,1) = { (n,0) | n in N },
Y[U] is the colimit of Y[n,0] for n in N and the maps between them.
Now, we need to say that Y[parse(p)] = X[p], up to isomorphism.
But this is just the statement that
X ---------> Y
| | |
| | |
|----+ |
| |
| |
V parse V
Nx2 -------> D(Nx2)
is a pullback.
Paul Taylor
^ permalink raw reply [flat|nested] only message in thread
only message in thread, other threads:[~2008-03-16 16:25 UTC | newest]
Thread overview: (only message) (download: mbox.gz / follow: Atom feed)
-- links below jump to the message on this page --
2008-03-16 16:25 replacement and iterated powersets Paul Taylor
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox;
as well as URLs for NNTP newsgroup(s).