nLab
AT category

Idea

In a discussion with Vaughan Pratt on the categories mailing list, Peter Freyd gave a very sharp description of the commonalities and differences between abelian categories and toposes (or, in the first place, between abelian categories and pretoposes), by introducing a finitely axiomatized theory of “AT categories”. As it turns out, this theory embodies the commonalities with such precision that every AT category splits as a product of an abelian category and a pretopos.

Remarkably, the properties in common are basically exactness conditions, and the sharp dichotomy between abelian categories and pretoposes can be concentrated solely in the behavior of the initial object.

Definition

Freyd introduces some baseline assumptions on the categories in question:

• Finite completeness,

• Presence of an initial object,

• Presence of pushouts for pairs of arrows one of which is monic,

• Presence of pushouts for kernel pairs

Each of these assumptions obtains in any abelian category and in any pretopos.

Most of the AT axioms Freyd introduces can be phrased directly in terms of such limits and colimits, and these axioms have a simple logical structure: they are just Horn clauses in the predicates stipulated by these baseline assumptions. This may look like a side comment for logicians, but it may well signal that Freyd intends to invoke, if pressed for details of proofs, one of a battery of representation theorems (such as the representation theorem for regular categories) whose precise expressions involve Horn clauses.

Anyway, to follow what Freyd is saying here a bit: by making choices for each such universal construction, categories satisfying these assumptions can be considered models of a suitable essentially algebraic theory. In any case, each of these baseline assumptions can be turned into predicates (e.g., ”$(p,q)$ is a pushout pair for pairs of arrows $(f,g)$” is a predicate $P(p,q;f,g)$ for a first-order theory of categories with these baseline assumptions), and the majority of axioms Freyd writes down, in particular all of the first 8 below, are expressible as universal Horn clauses in such predicates.

The sharp dichotomy which separates “abelianness” from “toposness” is concentrated in the following definition:

Definition

Let $0$ be the initial object, and let ${\pi }_1:0\times X\to 0$, ${\pi }_2:0\times X\to X$ be the two product projections. We say $X$ is of type T if ${\pi }_1$ is an isomorphism, and type A if ${\pi }_2$ is an isomorphism.

A pretopos will turn out to be precisely an AT category in which every object is of type T, and an abelian category will turn out to be an AT category where every object is of type A.

Now here come the AT exactness axioms. Again, each of them is satisfied in every abelian category and in every pretopos, and part of Freyd’s point is that any exactness axiom satisfied in both classes of categories is a logical consequence of this set of axioms. Some of Freyd’s remarks are included in parentheses.

A category meeting the baseline assumptions above is an AT category if the following 8 axioms plus axiom “AE” are satisfied.

1. The category is an effective regular category. (“Yes this can be stated as universal Horn conditions on pullbacks and the special pushouts mentioned above.”)

2. The arrow $0\to 1$ is monic. (“Note that it follows that all maps from $0$ are monic.”)

3. If $i:A\to C$ is monic, then any pushout square

   $$\begin{array}{ccc}A& \stackrel{i}{\to }& C\\ \downarrow & & \downarrow \\ B& \stackrel{j}{\to }& D\end{array}$$\array{ A & \stackrel{i}{\to} & C \\ \downarrow & & \downarrow \\ B & \stackrel{j}{\to} & D }

   is also a pullback, and $j$ is monic.

4. The functor $0\times -$ preserves pushouts of kernel pairs, and pushouts of pairs of arrows one of which is monic.

5. If $f:B\to 0\times C$ is epic and

   $$\begin{array}{ccc}A& \to & B\\ \downarrow & & \downarrow f\\ 0& \to & 0\times C\end{array}$$\array{ A & \to & B \\ \downarrow & & \downarrow f \\ 0 & \to & 0 \times C }

   is a pullback, then it’s also a pushout.

6. In the full subcategory of type T objects, pushouts of pairs of morphisms, one of which is monic, are universal (i.e., stable under pullback).

7. Define a functor $T$ by the pushout diagram

   $$\begin{array}{ccc}0\times X& \stackrel{{\pi }_1}{\to }& 0\\ {\pi }_2\downarrow & & \downarrow \\ X& \to & TX\end{array}$$\array{ 0 \times X & \stackrel{\pi_1}{\to} & 0 \\ \pi_2 \downarrow & & \downarrow \\ X & \to & T X }

   Then $T$ preserves pullbacks.

8. Given a morphism $f:X\to Y$, if $Tf$ and $0\times f$ are isomorphisms, then so is $f$.

This is the basic list of exactness assumptions which permit a sharp comparison between pretoposes and abelian categories. From this list alone one can prove that every AT category embeds faithfully in a product of a pretopos and an abelian category. To show that every AT category is equivalent to such a product, Freyd appends the following axiom involving an existential Horn condition:

• (AE) For every object $X$, there is a map $\xi :TX\to X$ such that

  $$0\times X\stackrel{{\pi }_1}{\to }X\stackrel{\xi }{\leftarrow }TX$$0 \times X \stackrel{\pi_1}{\to} X \stackrel{\xi}{\leftarrow} T X

  is a coproduct diagram, and the canonical map $X\to TX$ is a retraction of $\xi$.

To bring actual toposes into the picture, Freyd adds some more axioms, but let’s first take stock and see what this gives us so far.

Basic consequences of the AT axioms

Proposition

For any $X$ the unique map $0\to X$ is monic.

Proof

By axiom 2, the map $0\to 1$ is monic. The pullback-preserving functor $-\times X$ preserves monos, so

$$0\times X\stackrel{!\times 1_X}{\to }1\times X\cong X$$0 \times X \stackrel{! \times 1_X}{\to} 1 \times X \cong X

(which is just the second projection ${\pi }_2:0\times X\to X$) is monic. The unique map $0\to 0\times X$ is monic since it has a retraction ${\pi }_1:0\times X\to 0$. The result follows.

Proposition

Binary coproducts exist.

Proof

Because we can take the pushout of a pair of monos $0\to X$, $0\to Y$.

Proposition

Coproducts are disjoint.

Proof

By axiom 3, the two coprojections $i_X:X\to X+Y$, $i_Y:Y\to X+Y$ are monic, and their pullback is initial.

Category of type A objects is abelian

In this section we show that the full subcategory of type A objects forms an abelian category.

Lemma

An object is of type A if and only if there exists a map to $0$.

Proof

If $X$ is of type A, then we clearly have $X\cong 0\times X\stackrel{{\pi }_1}{\to }0$. Conversely, suppose there exists $p:X\to 0$. Note that since $0\to 1$ is monic, there is at most one map $Y\to 0$ for any object $Y$. It follows quickly that maps $Y\to X$ are in natural bijective correspondence with maps $Y\to X\times 0$, so that $X\cong X\times 0$ by the Yoneda lemma.

From this lemma, it follows that the full subcategory of type A objects in an AT category $C$ is equivalent to the category $C/0$, which is the category of coalgebras for the functor $A(X)=0\times X$. Hence the category of type A objects is coreflective.

Lemma

Objects of type A are closed under binary products, finite coproducts, subobjects, and quotient objects (= cokernels of kernel pairs).

Proof

This follows from the fact that the category of type A objects is the slice category $C/0$.

Before we prove the next lemma, recall that in a category with zero objects, a kernel of an arrow $f:A\to B$ is an equalizer of the pair $f,0:A\overrightarrow{\to }B$. This is the same as a pullback

$$\begin{array}{ccc}K& \to & A\\ \downarrow & & \downarrow f\\ 0& \to & B\end{array}$$\array{ K & \to & A \\ \downarrow & & \downarrow f \\ 0 & \to & B }

Cokernels are defined dually, and can be formulated dually as certain pushouts. Since pushouts along monos exist, we can take the cokernel of any mono, and in particular the cokernel of any kernel.

Lemma

In the category of type A objects, every mono is the kernel of its cokernel, and every epi is the cokernel of its kernel.

Proof

Of course, $0$ is a zero object in the category of type A objects. If $i:A\to B$ is a mono in the category of type A objects, then the pushout

$$\begin{array}{ccc}A& \stackrel{i}{\to }& B\\ \downarrow & & \downarrow \\ 0& \to & \mathrm{coker}(i)\end{array}$$\array{ A & \stackrel{i}{\to} & B \\ \downarrow & & \downarrow \\ 0 & \to & coker(i) }

exists and is also a pullback, by axiom 3, and hence $i$ is the kernel of its cokernel. Now suppose $f:A\to C$ is an epi in the category of type A objects. Since $0\times C\cong C$, we have an epi $f:A\to 0\times C$. Then, by axiom 5, the pullback

$$\begin{array}{ccc}\ker (f)& \to & A\\ \downarrow & & \downarrow f\\ 0& \to & 0\times C\end{array}$$\array{ ker(f) & \to & A \\ \downarrow & & \downarrow f \\ 0 & \to & 0 \times C }

is also a pushout, so $f$ is the cokernel of its kernel.

Theorem

The category of type A objects is an abelian category.

Proof

Any category with zero objects, binary products and coproducts, and in which every mono is the kernel of its cokernel and every epi is the cokernel of its kernel, is in fact an abelian category. See Freyd-Scedrov, Categories, Allegories, 1.598 (p. 95).

Category of type T objects is a pretopos

Now we show that the full subcategory of type T objects is a pretopos. It is clear that $0\times 0\cong 0$ (since $0\to 1$ is monic), so $0$ is a type T object.

Lemma

If $A$ is type A and $T$ is type T, then there exists exactly one map $A\to T$. Type T objects are characterized by this property.

Proof

There is exactly one morphism $A\to 0$. Hence morphisms $A\to T$ are in bijection with maps $A\to 0\times T\cong 0$, of which there is exactly one. For the second statement, suppose that $X$ has the property that there is exactly one map $A\to X$ for each type A object. Such objects $X$ are closed under products, and $0$ is such an object; therefore $0\times X$ is such an object. On the other hand, $0\times X$ is of type A since it projects to $0$. Hence there is at most one morphism $0\times X\to 0\times X$, and it follows that $0\times X\to 0\to 0\times X$ is the identity, so that $0\times X\cong 0$. Thus $X$ is of type T.

Corollary

The initial object $0$ is strict in the category of type T objects.

Proof

Given $T$ of type T and $T\to 0$, we know $T$ is type A, and therefore there is exactly one map $T\to T$. Hence $T\to 0\to T$ is the identity, and of course so is $0\to T\to 0$. So $T$ is initial.

Corollary

The full subcategory of objects of type T is closed under products, coproducts, subobjects, and quotient objects.

Proof

Closure under products and subobjects is immediate from the lemma that characterizes type T objects in terms of maps out of type A objects. Closure under quotients and coproducts follows from axiom 4.

Theorem

The full subcategory of objects of type T is a pretopos.

Proof

The previous proposition gives finite completeness, coproducts, and quotients of kernel pairs. One of the AT axioms is that in the full subcategory of $T$ objects, pushouts along monos are stable under pullback, and the initial object is stable under pullback in the category of T objects, because it is strict there. It follows that coproducts are universal in the category of T objects. They are also disjoint by an earlier result, so the category of T objects is extensive. It is also effective regular by axiom 1, hence a pretopos.

Splitting into type A and type T objects

In this section we show that every AT category $C$ is the product of the abelian category $C_A$ of type A objects and the pretopos $C_T$ of type T objects.

Let us first observe that the coreflector

$$0\times -:C\to C_A$$0 \times {-}\colon C \to C_A

is left exact (as all coreflectors are), and

• Preserves the initial object (by axiom 2),

• Preserves pushouts of kernel pairs, and pushouts of pairs of arrows one of which is monic (axiom 4),

• And therefore also preserves coproducts.

A functor between AT categories which is left exact and which preserves such classes of finite colimits may be called a morphism of AT categories. Hence the coreflector is a morphism of AT categories.

Next let us observe that the subcategory $C_T\hookrightarrow C$ is reflective; the reflector is the functor $T$ defined above by means of a suitable pushout. The reflector clearly preserves any colimits that exist, and preserves pullbacks (by axiom 7), so

$$T:C\to C_T$$T\colon C \to C_T

is also a morphism of AT categories. Therefore we have a morphism of AT categories

$$F=⟨0\times -,T⟩:C\to C_A\times C_T$$F = \langle 0 \times {-}, T \rangle\colon C \to C_A \times C_T

and now we wish to prove, under a suitable additional axiom (also satisfied by every abelian category and every pretopos), that this is an equivalence.

Lemma

The functor $F$ is faithful.

Proof

The functor $F$ is left exact and therefore preserves kernels. By axiom 8, $F$ reflects isomorphisms. It follows immediately from these two facts that $F$ is faithful.

• Remark: With this result, Freyd’s “first task” is complete: any AT category may be faithfully represented in a product of a pretopos and an abelian category.

At this point we bring in axiom AE for its debut appearance. It may be helpful to consider that $TX$ is by definition the cokernel appearing in the exact sequence

$$0\times X\stackrel{{\pi }_2}{\to }X\to \mathrm{coker}({\pi }_2)$$0 \times X \stackrel{\pi_2}{\to} X \to coker(\pi_2)

and that axiom AE asserts that this exact sequence splits (with splitting $\xi :\mathrm{coker}({\pi }_2)\to X$), in such a way that $X$ is the coproduct of the end terms.

Proposition

The functor $F$ is full.

Suppose given maps $f:0\times X\to 0\times Y$, $g:TX\to TY$, and contemplate the diagram

$$\begin{array}{ccccc}0\times X& \stackrel{{\pi }_2}{\to }& X& \to & TX\\ f\downarrow & & & & \downarrow g\\ 0\times Y& \underset{{\pi }_2}{\to }& Y& \stackrel{\stackrel{\xi }{\leftarrow }}{\to }& TY\end{array}$$\array{ 0 \times X & \stackrel{\pi_2}{\to} & X & \to & T X \\ f \downarrow & & & & \downarrow g \\ 0 \times Y & \underset{\pi_2}{\to} & Y & \stackrel{\overset{\xi}{\leftarrow}}{\to} & T Y }

Since $X=(0\times X)+TX$, the two obvious arrows $0\times X\to Y$, $TX\to Y$ combine to give an arrow $(f,g):X\to Y$. It is straightforward to check that $0\times (f,g)=f$ (because the functor $0\times -$ kills the type T summands) and that $T(f,g)=g$.

Theorem

The functor $F$ is an equivalence.

Proof

All that is left to check is that $F$ is essentially surjective, but this is clear because given a type A object $X$ and a type T object $Y$, we have $0\times (X+Y)\cong X$ (use axiom 4 plus the fact that $0\times Y\cong 0$), and

$$T(X+Y)\cong TX+TY\cong 0+TY\cong Y$$T(X + Y) \cong T X + T Y \cong 0 + T Y \cong Y

which completes the proof.

This completes Freyd’s “second task”.

Topos-theoretic considerations

In order to beef up the type T objects to a topos, Freyd imposes some extra structure on top of the AT axioms. Since it is now the topos axioms that are in the ascendant, I will christen these categories TA categories.

Thus, a TA category is an AT category $C$ together with

• Functions $P,E:\mathrm{Ob}(C)\to \mathrm{Ob}(C)$,

• Functions $l,r:\mathrm{Ob}(C)\to \mathrm{Mor}(C)$, of the form $lX:EX\to PX$, $rX:EX\to X$,

• An operation $\Lambda$ which assigns to each pair of morphisms $f:R\to Y$, $g:R\to X$ (where $R$ and $Y$ are assumed to be type T), a morphism $\Lambda (f,g):Y\to PX$.

This data is to satisfy the following axioms:

1. $⟨lX,rX⟩:EX\to PX\times X$ is monic and $PX$, $EX$ are of type T,

2. The composite of relations

   $$Y\stackrel{\Lambda (f,g)}{\to }PX\stackrel{(lX{)}^{\mathrm{op}}}{\to }EX\stackrel{rX}{\to }X$$Y \stackrel{\Lambda(f, g)}{\to} P X \stackrel{(l X)^{op}}{\to} E X \stackrel{r X}{\to} X

   is equal to

   $$Y\stackrel{f^{\mathrm{op}}}{\to }R\stackrel{g}{\to }X,$$Y \stackrel{f^{op}}{\to} R \stackrel{g}{\to} X,

3. If

   $$\begin{array}{ccc}R& \stackrel{g}{\to }& EX\\ f\downarrow & & \downarrow lX\\ Y& \underset{h}{\to }& TX\end{array}$$\array{ R & \stackrel{g}{\to} & E X \\ f \downarrow & & \downarrow l X \\ Y & \underset{h}{\to} & T X }

   is a pullback and $R$ is of type T, then $\Lambda (f,(rX)\circ g)=h$.

Freyd: “Note that in the full category of type-T objects, $P$ yields power-objects with $E$, $l$, $r$ naming the universal relations. (The third axiom provides the uniqueness condition.)”

And: “In any abelian category the only type T object is the zero object, which forces $P=E=0$ for abelian categories.”

And finally: “It’s routine that both $0\times -$ and $T$ preserve the new structure. We can now remove the existential from AE. Define $\xi :TX\to X$ as the image of $rX$. The third task is finished with:

1. For every $X$, $0\times X\to X\stackrel{\xi }{\leftarrow }TX$ is a coproduct diagram.”

This section is likely to be rewritten and cleaned up.