f f (1)

1

ad c

d

‚ c

EA

A

t

commutes.

A PE-structure N = (N, 0, s) is a natural number object or NNO (or ob-

ject of natural numbers or natural numbers object) if for any PE-structure (A, a, t)

there is a unique morphism t(’) a: (N, 0, s) ’ (A, a, t). If we write (suggestively)

’

n (’)

t (a) for t a(n) when n ∈ N , then the de¬ning properties of a morphism of

PE-structure means that

(i) t0 (a) = a, and

(ii) tsn (a) = t —¦ tn (a).

It follows immediately that if we identify the natural number n with the global

element s —¦ s —¦ s · · · s —¦ 0 (s occurring in the expression n times) of N, then expressions

like tn (a) are not ambiguous. However, now tn (a) is de¬ned for all elements n of

N, not merely those global elements obtained by applying s one or more times to

0.

In this section, we will derive some basic properties of natural number objects

and prove a theorem (Theorem 6 below) due to Freyd that characterizes them

by exactness properties. The proof is essentially the one Freyd gave; it makes

extensive use of his embedding theorems (Section 7.1).

We begin with Proposition 1 below, which says in e¬ect that any PE-structure

contains a substructure consisting of all elements tn (a). Note that this is a state-

ment about closure under a “countable” union in any topos, so it will not be a

surprise that the proof is a bit involved. Mikkelsen [1976] has shown that inter-

nal unions in PA, suitably de¬ned, always exist. (Of course, ¬nite unions always

exist). That result and a proof of Proposition 1 based on it may be found in

Johnstone [1977].

Proposition 1. If (A, a, t) is a PE-structure, then there is a substructure A of

A for which the restricted map a, t : 1 + A ’ A is epi.

’

The notation a, t is de¬ned in Section 1.8. A PE-structure (A , a , t ) for

which a , t is epi will be called a Peano system.

7.5 Natural Number Objects 259

Proof. We begin by de¬ning a natural transformation r: Sub(’ — A) ’ Sub(’ —

’

A) which takes U ⊆ A — B to

U © (Im(idB — a) ∪ (idB — t)(U ))

where (idB — t)(U ) means the image of

id — t

U )’ B — A ’’ B ’

’ ’ ’’ B — A

’

That r is natural in B follows easily from the fact that pullbacks commute

with coequalizers, hence with images. Note that if A ⊆ A then rA = A if and

only if A ⊆ Ima ∪ tA .

The function r induces an arrow also called r: PA ’ PA. Let E be the

’

equalizer of r and idPA . De¬ne C by the pullback

E E E—A

C

(2)

c c

E E PA — A

∈A

Here ∈ A is de¬ned in Exercise 2 of Section 2.1. In rest of the proof of

Proposition 1, we will repeatedly refer to the composites C ’ E and C ’ A

’ ’

of the inclusion with the projections.

In the following lemma, A ⊆ A corresponds to cA : 1 ’ PA.

’

Lemma 2. The following are equivalent for a subobject A )’ A.

’

(i) A ⊆ Ima ∪ tA —¦

(ii) rA = A

(iii) cA : 1 ’ PA factors through E by a map u: 1 ’ E.

’ ’

(iv) A can be de¬ned as a pullback

EC

A

(3)

c c

EE

1

for which the inclusion A )’ A = A ’ C ’ E — A ’ A, the last map being

’ ’ ’ ’

projection.

260 7 Representation Theorems

Proof. That (i) is equivalent to (ii) follows from the fact that in a lattice, A©B =

B if and only if B ⊆ A. That (ii) is equivalent to (iii) follows from the de¬nition

of E: take B = 1 in the de¬nition of r.

Assuming (iii), construct v: A ’ C by the following diagram, in which the

’

outer rectangle is a pullback, hence commutative, and the bottom trapezoid is

the pullback (2).

E E A=1—A

A

d d

dv d idA

u — idA

d d

‚

d c d

‚

E E E—A EA (4)

C

c

c

© c

E E PA — A

∈A

The last part of (iv) follows immediately from the preceding diagram.

Now in the following diagram, II, III, IV and the left rectangle are pullbacks

and III is a mono square. Hence I and therefore the top rectangle are pullbacks

by Exercise 12, Section 2.2.

p1 E

E E 1—A 1

A

u

u — idA II

I

c

c c

E E E—A EE (5)

C p1

III IV

c c c

E E PA — A E PA

∈A

Thus (iii) implies (iv).

Given (iv), let u: 1 ’ E be the bottom arrow in (3). Then in (5), III is a

’

pullback and so is the rectangle I+II, so I is a pullback because II is a mono

square. Hence the rectangle I+III is a pullback. Clearly rectangle II+IV is a

pullback, so the outer square is a pullback as required.

Let D be the image of C ’ E — A ’ A. We will show that D is the

’ ’

subobject required by Proposition 1.

7.5 Natural Number Objects 261

Lemma 3. The statement

(A) D ⊆ Ima ∪ tD

is true if and only if

(B) the map e: P1 ’ C in the following pullback is epi.

’

e EC

P1

(6)

c c

E1+A EA

1+C

Proof. We use Freyd™s near-exact embedding Theorem 7 of Section 7.1. By

Lemma 2, the statement (A) is the same as saying that two subobjects of A

are equal, a statement both preserved and re¬‚ected by a near-exact faithful func-

tor. (Note that the de¬nition of r involves almost all the constructions preserved

by a near-exact functor). Since statements (A) and (B) are equivalent in the

category of sets (easy), they are equivalent in a power of the category of sets

since all limits and colimits are constructed pointwise there. It thus follows from

the near-exact embedding theorem that (A) is equivalent to (B).

Now we will do another transference.

Lemma 4. Suppose that for every global element c: 1 ’ C the map f : P2 ’ 1

’ ’

in the pullback

f E1

P2

c (7)

C

c c

1+C E1+A EA

is epic. Then (B) is true.

Proof. We ¬rst observe that by a simple diagram chase, if e: P ’ C is not epi,

’

then neither is the left vertical arrow in the following pullback diagram.

E P —C

P

e — idC (8)

c c

E C —C

C

(c, idC )

262 7 Representation Theorems

Now if e in (6) is not epi, its image in the slice E /C is not epi either. The

observation just made would then provide a global element of C in a diagram of

the form (7) in which the map P ’ 1 is not epic. The lemma then follows from

’

the fact that all constructions we have made are preserved by the logical functor

E ’ E /C.

’

Lemma 5. (B) is true.

Proof. We prove this by verifying the hypothesis of Lemma 4. Let c be a global

element of C. De¬ne C by requiring that

EC

C

(9)

c c

cE EE

1 C

be a pullback, and P3 by requiring that the top square in

E 1+C

P3

c c

E 1+C

P2

(10)

c

f 1+A

c c

EC EA

1

be a pullback. The bottom square is (7) with c replaced by the global element

of C induced by c and the de¬nition of C . This square is easily seen to be a

pullback, so the big rectangle is a pullback.

Because g —¦ h epi implies g epi, it su¬ces to show that P3 ’ 1 is epic. We

’

can see that by factoring the big rectangle in (10) vertically:

E P4 E 1+C

P3

c c c

EC EA

1

Here P4 is de¬ned so that the right square is a pullback. The middle arrow is

epi by Lemma 2 and Lemma 3, so the left arrow is epi as required.

7.5 Natural Number Objects 263

By Lemma 5, D satis¬es property (i) of Lemma 2. By Lemma 2, any subobject

A which has that property factors through C, hence through its image D. Since

Ima ∪ tD also has property (i) of Lemma 2 (easy), it must be that D = Ima ∪ tD.

This proves Proposition 1.

Theorem 6. [Freyd] A PE-structure (A, a, t) for which

(i) a, t is an isomorphism and

(ii) the coequalizer of idA and t is 1

is a natural number object, and conversely.

The proof will make use of

Proposition 7. [The Peano Property] A PE structure (A, a, t) which satis¬es

requirements (i) and (ii) of Theorem 6 has no proper PE-substructures.

Proof. Let (A , a , t ) be a substructure. By going to a subobject if necessary we

may assume by Proposition 1 that the restricted a , t : 1 + A ’ A is epi. Since

’

this proposition concerns only constructions preserved by exact functors, we may

assume by Corollary 6 of Section 7.1 that the topos is well-pointed, hence by

Proposition 2 of the same section that it is Boolean.

Let A be the complement of A in A. If the topos were Set, it would follow

from the fact that a, t is an isomorphism on 1 + A and an epimorphism to A

on 1 + A that

(—) tA ⊆ A

Since sums, isomorphisms, epimorphisms and subobjects are preserved by

near-exact functors, using the near-exact embedding of Theorem 7 of Section 7.1,

(*) must be true here. Thus t = t + t where t and t are the restrictions of t to