Subject: categories: on the axiom of infinity

From: Peter Freyd <[email-masked]>
Date: Mon, 29 Mar 2004 11:03:30 -0500 (EST)

Let  *T*  be the topos freely generated by its constants (a few
postings ago I called it the initial object in the category of topoi
and logical morphisms), let  Omega  be its subobject classifier and
let  P  denote  Omega^Omega. I wrote:

  There's a subobject, M, of  P  on which we may define the structure
  of a rig (a ring without negation) that mimics the natural numbers.
  In particular the set of global sections, that is, maps from  1  to
  M  with its inherited rig structure, is isomorphic to the standard
  natural numbers...

  [Moreover we may] construct a topos-object in  *T*  whose topos of
  global sections is isomorphic to the free topos with NNO. And, as
  for  M, an equation in the theory of topoi is internally true for
  this internal topos iff it is true for the free topos with NNO.

It occurs to me that the proofs I have in mind rest on at least three
considerations that may not be well known. (I have no idea about other
proofs.)

The first consideration stems from curiosity about the complete
algebraic theory of  Omega. In particular, what are its unary
operators? Some would phrase that: What are the "modalities" implicit
in higher-order intuitionistic logic?

There's a particular operator that keeps popping up for me.

In an arbitrary heyting algebra define  x << y  to mean that not only
is  x  less than or equal to  y, but the value of  y -> x  is as small
as it can be, that is, y -> x = x. In a complete heyting algebra
define an order-preserving, inflationary unary operation  s  by

                       sx =  inf{ y | x << y }.

E.g.: on a linearly ordered set if { y | x < y } has a least element
then that's what  sx  is. If there is no smallest element above  x,
then  sx = x (even without the completeness hypothesis). In
particular, note, there no assertion that  x << sx.

The subobject classifier in an elementary topos is complete in the
relevant sense: s  is definable. A quick description of the
construction to follow is that we're going to turn  s  into the
successor operation on an NNO.

DIVERSION: The definition I just gave is the first I came across. The
next incarnation for me was when I wanted a measure of the failure of
booleaness. In any topos, *A*, there's a largest subterminator  B
with the property that the slice category  *A*/B  is boolean. But
given any subterminator, U, we have its "closed sheaves", *A*_(U), the
full subcat of objects  A  such that  AxU --> U  is an iso. (This is a
subcategory of sheaves for a Lawvere-Tierney topology. Starting with
a space  X  then  Sheaves(X)_(U)  may be identified with  Sheaves(U'),
where  U'  denotes the complement of U.)  Note that the lattice of
subterminators in  *A*_(U)  is isomorphic to the interval of
subterminators in  *A*  from  U  up. We can define BU  to be the
largest subterminator in  *A*_(U)  such that  *A*_(U)/BU  is boolean.
The interval of subterminators in  *A*  from  U  up to  BU  is boolean
and in the relevant internal sense, BU  is the largest such
subterminator. We can, of course, translate this all to a unary
operation on  Omega.

It's the same operator  s.

When one specializes this to a space  X  it becomes historically
familiar if we dualize it it to a deflationary operator on closed
subsets. It's the operation that removes isolated points. The very
operation that got Cantor started. Hence the word "historically".

END OF DIVERSION

Back to  *T*: in the monoid  Omega^Omega  define  C  to be the
submonoid generated by  s. We're going to use  0 : 1 --> C  to denote
the name of the identity element (you might think of it as  s^0) and
we're going to use  suc : C -> C  to denote the function that sends an
element  x  to  sx.

It's easy to verify that the necessary and sufficient condition for
C,0,suc  to be an NNO is that -- in the internal sense -- it has no
fixed points. The argument works for any one-generator partially-
ordered monoid whose identity element is below the generator. Let  E
be the equalizer of  1, suc : C --> C. I'm saying that  C,0,suc  is an
NNO iff  E  is empty.

Let  V  be the negation of the image of  E --> 1. It is the largest
subterminator such that  C,0,suc  becomes an NNO in the slice category
*T*/V.

Now for the nice part. The sconing argument tells us that  V, as is
the case for any non-trivial negation, is an indecomposable projective
-- that is, the covariant functor represented by  V  is an exact
functor. And that means that  1  is an indecomposable projective in
the slice category  *T*/V. The "global-section" functor from  *T*/V
to  *Sets*  is exact. Hence (by my first theorem in this subject) it
preserves the NNO and all the definable structure thereon.

I advertised an object, not in a slice category but in  *T*. So define
M = C^V. Then it is easily verified that the global sections of  M
as defined in  *T*  are naturally isomorphic to the global sections
of  C/V  as defined in  *T*/V.

Since it has an NNO we can construct all sorts of things in  *T*/V.
We'll settle here for the free-topos-object-with-NNO. That is, there
is an object  T  in  *T*/V  with a binary partial operation that
serves as the free topos with NNO in  *T*/V. Since the global-section
functor is exact we know that it preserves free structures in great
generality (part of lore of exact functors between topoi). In
particular it carries  T  to a standard free topos with NNO .And,
finally, we know that  T^V  has that same last property as an object
in  *T*.

(Better, actually, is to take  T  to be the free topos on one object.
Every finitely presented topos is a slice thereof -- including the
free-topos-with-NNO.)

Surely this is all too easy. Yeah. I skipped over something. My point
about negations being indecomposable projectives requires them to be
non-trivial. (The covariant functor represented by  0  is not exact;
it does not preserve the coterminator.) That is, we need to show that
V  is not  0. But for that it suffices (given the defining universal
property for  *T*) to show in at least one topos that the recipe for
V  yields something nontrivial. Equivalently, we need a topos in which
V = 1. The most easily named example is the topos of  N-sets, or as I
described it a few postings ago, the topos of sets with distinguished
self-maps. This topos is two-valued, that is, Sub(1)  has just two
elements and that can be an advantage. (We know that we must show that
suc : C --> C  has no fixed points.) In fact, I find it easier to work
in the slice category  (*Sets*^N)/N. (There is, anyway, a faithful
representation of  *Sets*^N  into  (*Sets*^N)/N.) The category
(*Sets*^N)/N  is equivalent to the category of covariant set-valued
functors on the poset also denoted  N. The advantage here is just the
opposite: (*Sets*^N)/N  is generated by its non-zero subterminators
and they're all indecomposable projectives.

DIVERSION: When I first finished writing this piece I noticed for the
first time that there's a historically much better example. Take the
category of sheaves on the reals (or for that matter, any space of
geometric interest). Then follow in Cantor's footsteps.

FOOTNOTE:

One variation worth mentioning. Instead of taking  C  as the submonoid
generated by  s  take it to be the smallest up-closed submonoid, that
is, this new version of  C  will be closed with respect to sups. This
C  is trying to be a big ordinal number. Indeed, following just the
path first taken by Cantor we can find Grothendieck topoi where  C
looks like an arbitrarily large initial section of ordinals.

In the free topos with NNO this  C  seems to be none other than the
ordinal (in some relevant sense) of all recursively enumerable
ordinals.