The Trace Factorisation of Stable Functors

Paul Taylor

1998

Abstract

A functor is stable if it has a left adjoint on each slice. Such functors arise as forgetful functors from categories of models of disjunctive theories. A stable functor factorises as a functor with a (global) left adjoint followed by a fibration of groupoids; Diers [D79] showed that in many cases the corresponding indexation is a well-known spectrum. Independently, Berry [B78,B79] constructed a cartesian closed category of posets and stable functors, which Girard [G85] developed into a model of polymorphism; the proof of cartesian closure implicitly makes use of this factorisation. Girard [G81] had earlier developed a technique in proof theory involving dilators (stable endofunctors of the category of ordinals), also using the factorisation.

Although Diers [D81] knew of the existence of this factorisation system, his work used an additional assumption of preserving equalisers. However Lamarche [L88] observed that examples such as algebraically closed fields can be incorporated if this assumption is dropped, and also that (in the the search for cartesian closed categories) evaluation does not preserve equalisers. We find that Diers’ definitions can be modified in a simple and elegant way which also throws light on the General Adjoint Functor Theorem and on factorisation systems.

In this paper the factorisation system is constructed in detail and related back to Girard’s examples; following him we call the intermediate category the trace. We also consider natural and cartesian transformations between stable functors. We find that the latter (which must be the morphisms of the “stable functor category”) have a simple connection with the factorisation, and induce a rigid adjunction (whose unit and counit are cartesian) between traces.

1 The Trace Factorisation

1.1 Candidates

Stable functors generalise the well-known concept of a functor with a left adjoint, but it turns out to be easier to express this generalisation in terms of the older idea of a universal map from an object to a functor.

Example 1.1 Let S be the forgetful functor from X = Gp to Y = Set and Y ∈ Y. Then u : Y → SX universal map from Y to S if for any (function) v : Y → SX′′ there is a unique (group homomorphism) h : X → X′′ such that v = u; Sh.

Of course there are lots of examples like this one. In this case, X is the free group on (generators) Y and u is the inclusion of the generators; for any set Y, X exists and is unique up to isomorphism. Notice that X, and not just SX, is part of the data defining u.

Diers generalised this idea to cover numerous examples (mostly involving rings and order structures) in which there may be several “free” structures, but which are still in some intuitive sense universal.

Example 1.2 Let X = IntDom, the category of integral domains and monomorphisms, and Y = CRng, the category of commutative rings and homomorphisms. Any map from a ring to an integral domain factors through the quotient by some prime ideal, but there may be many prime ideals. However the quotient remains the “smallest” integral domain for which the given prime ideal is the kernel, so we need a universal property which restricts attention to a particular class of integral domains.

Diers said that u : Y → SX_{0} is diagonally universal from the object Y to the functor S if for any triple of maps v : Y → SX′ in Y and f : X_{0} → X and g : X′ → X in X, such that the square

Y  \overline{u} SX_{0}

.............. Sh

[figure: SX′; v; Sg; SX; Sf]

commutes, there is a unique h : X_{0} → X′ such that v = u; Sh. As a corollary, f = h; g.

One (albeit abstruse) way of seeing how this condition arises is to recall (say from the proof of the Adjoint Functor Theorem, section 1.3) that in order to construct a left adjoint for S we need to find an initial object in each comma category Y ↓ S. If Y preserves all limits then (ignoring size questions) the initial object is simply the limit of Y ↓ S. However in Diers’ case S only preserves connected limits, so we only have initial objects in each component; the condition above ensures that v : Y → SX′ lies in the same component as the intended universal map. Components are connected via “zig-zags”, but it is easy to see that this property (with one zig-zag) is equivalent to the more general version.

This definition reduces to the original notion of universality if we let X be the terminal object of X and this is preserved by S.

Now one can go one stage further than this. The intuition which suggests that a quotient by a prime ideal should be universal also demands the same of adjoining a root of a polynomial to a field.

Example 1.3 Let X = Fld[\sqrt{−1}] be the category of fields in which x^{2} + 1 splits and S be its inclusion in Y = Fld, the category of all fields (and homomorphisms). Let Y be a field not of characteristic 2 in which this polynomial is irreducible and X_{0} = Y [\sqrt{−1}], for example Y = ℝ and X_{0} = ℂ. Then the inclusion u : Y → SX_{0} has the above property, except that there are two maps h with v = u; Sh, only one of which satisfies f = h; g.

Hence we are led to the following tighter definition. The new terminology, which indicates that u is only one of many for given Y, is suggested by coproduct candidates (1.4.4). It also avoids confusion with Diers’ term diagonally universal for a functor, although we shall not need the latter in this paper.

Definition 1.4 The map u : Y → SX_{0} in Y is said to be a candidate if for any triple of maps v : Y → SX′ in Y and f : X_{0} → X and g : X′ → X in X, such that the square

Y  \overline{u} SX_{0}

.............. Sh

[figure: SX′; v; Sg; SX; Sf]

commutes, there is a unique h : X_{0} → X′ such that both u; Sh = v and h; g = f. Note: we shall have many diagrams similar to this with dotted fill-ins; it is important to note that we intend the lower triangle to commute “without S”, i.e. h; g = f and not just Sh; Sg = Sf.

Exercise 1.5 Suppose that u : Y → SX is a candidate for S : X → Y and v : Z → T Y is for T : Y → Z. Show that v; T u is a candidate for T S : X → Z. Show also that a map is a candidate for the identity iff it is invertible. □

1.2 Stable Functors

Now in this process of generalisation we have left one thing behind: existence. This was easy in the first example, because u was unique.

Definition 1.6 A functor S : X → Y is stable if every morphism w : Y → SX in Y (where X ∈ X) can be expressed as w = u; Sf where u : Y → SX_{0} is a candidate and f : X_{0} → X in X. From the definition of candidacy, it is immediate that this factorisation is unique up to unique isomorphism h.

Examples 1.7 The forgetful functors Gp → Set, IntDom → CRng and Fld[\sqrt{−1}] → Fld are stable, as is any function between domains which denotes a sequential algorithm. The first two of these functors preserve equalisers: we call them discretely stable for reasons which will become apparent.

Exercise 1.8 Show that if S : X → Y and T : Y → Z are stable then so is T S : X → Z, and that every candidate w : Z → T SX for T S is uniquely (up to isomorphism) of the form v ; T u with u and v candidate for S and T respectively. □

Lemma 1.9 Suppose S : X → Y is stable and let X ∈ X. Then S restricts to a functor X /X → Y/SX which has a left adjoint. Proof The restriction takes x : X′ → X to Sx : SX′ → SX and similarly on commutative triangles. For the left adjoint, let w : Y → SX in Y/SX. By hypothesis w = u ; Sf with u : Y → SX′ a candidate. Comparing this with Example 1.1.1, u is universal (in the original sense) from w ∈ Y/SX to (the restriction of) S, and so is the unit of an adjunction; this takes w : Y → SX to f : X′ → X. □

Now we shall show that the converse is true. First we need a lemma which allows us to shift attention from one slice to another.

Lemma 1.10 Let S : X → Y and ξ : X_{0} → X_{1} in X be such that that the functors S_{0} : X /X_{0} → Y/SX_{0} and S_{1} : X /X_{1} → Y/SX_{1} have left adjoints. Then the morphism

Y  \overline{u} SX
[figure: y; Sx]
SX_{0}

SX_{1} \begin{matrix}Sξ \\  \end{matrix}

is universal for S_{0} iff it universal for S_{1}. Proof In both cases the unit of the adjunction at Y exists and is unique up to unique isomorphism, so it suffices to assume that u is the unit for S_{1} and show that it has the universal property for S_{0}. Suppose that v : Y → SZ is a morphism over SX_{0}, where z : Z → X_{0}, i.e.

v ; Sz = y

Then it is also one over SX_{1}, and so there is a unique h : X → Z with v = u; Sh over SX_{1}, i.e. a unique simultaneous solution of

u; Sh = v  and  h; z ; ξ = x; ξ

but it still remains to show that we may cancel the ξ. Now y : Y → SX_{0} is another morphism over SX_{1}, and so there is a unique x′ : X → X_{0} such that

u; Sx′ = y  and  x′ ; ξ = x; ξ

Clearly x′ = x satisfies these equations, but x′ = h; z does too, so h; z = x as required. Hence we conclude that h is the unique mediator with respect to S_{0} as well as for S_{1}. □

From this we can prove the factorisation property.

Proposition 1.11 A functor S : X → Y is stable (i.e. has the factorisation property) iff its restriction to each slice has a left adjoint. Proof We have already proved “only if”. Consider first the slice by X_{1}. We may write w = u;Sx, where u is universal for S_{1} : X /X_{1} → Y/SX_{1} and x : X_{0} → X_{1}. Putting ξ = x : X_{0} → X_{1} in the lemma, u is also universal for S_{0} : X /X_{0} → Y/SX_{0}.

Now suppose that the square

Y  \overline{u} SX_{0}

.............. Sh

[figure: SX′′; v; Sg; SX′; Sf]

commutes in Y. We may regard this as simply a pair of maps u : Y → SX_{0} and v : Y → SX′′ in the slice Y/SX′. Now using the lemma again with ξ = f (but in the opposite direction), u is universal for S′ : X /X′ → Y/SX′, and so there is a unique fill-in h : X_{0} → X′′ over X′ (i.e. f = h; g) with v = u; Sh. □

Now it is well known that functors with left adjoints preserve limits, but that the converse involves a mysterious “solution set condition”. Although stable functors clearly only preserve a restricted class of limits, we shall find that in this setting the solution set condition becomes much more natural.

Definition 1.12 A wide pullback is a diagram d : I → X (or its limit, according to context) such that I has a terminal vertex. Thus ordinary (binary) pullbacks are wide pullbacks, and any cofiltered limit diagram is equivalent (for constructing limts) to a wide pullback diagram, but equalisers, binary products and terminal objects are not.

Exercise 1.13 Stable functors preserve wide pullbacks and monos. □

Exercise 1.14 Show how to calculate the limit of an arbitrary finite diagram with a terminal vertex by repeated use of (ordinary) pullbacks, and hence wide pullbacks in terms of pullbacks and cofiltered limits. □

1.3 Factorisation through Candidates

We now aim to show that if S preserves wide pullbacks then the factorisation property w = u; Sf holds, where u is a candidate. Forgetting this last requirement for the moment, consider all possible factorisations w = u′ ; Sf′; these form a category whose morphisms are as illustrated:

SX_{1}  X_{1}
[figure: u_{1}; f_{1}]
Y  X
[figure: u_{2}; f_{2}]
[figure: SX_{2}; Sh; X_{2}; h]

Clearly the factorisation is through a candidate iff the corresponding object of this category is initial. We obtain the initial object as the wide pullback of all the others, or at least a cofinal subdiagram of them, and we need this diagram to be indexed by a set.

Definition 1.15 S : X → Y satisfies the solution set condition if for every w : Y → SX the (possibly large) category of factorisations has a small full cofinal subcategory. This means that for any given factorisation u_{2};Sf_{2} there is a factorisation u_{1};Sf_{1} in the subcategory with h : (1) → (2), and between any two factorisations in the subcategory there is only a set of morphisms.

Of course if we already know that the functor is stable, the singleton subdiagram consisting of the candidate factorisation will suffice, so that the condition is trivially necessary, whilst the remaining details of sufficiency are left as an exercise.

Theorem 1.16 Let S : X → Y be any functor. Then the following are equivalent:

(α) S is stable, i.e. the factorisation property holds;

(β) S has a left adjoint on each slice;

and if X has all small wide pullbacks,

(γ) S preserves wide pullbacks and satisfies the solution set condition. □

Notice, incidentally, that (α) and (γ) are directly equivalent, whereas to prove (β) it is necessary to choose the values of the left adjoint, or, as we have formulated it, the factorisations w = u; Sf, from the isomorphism classes. Of course any two left adjoints are uniquely isomorphic, but it would nevertheless be nice to be able to avoid having to make this choice, which in fact becomes more complicated and less canonical in the case of stable functors. The presentation in terms of candidates, the spectrum and the trace provides a way of working without such choices.

The factorisation theorem is highly reminiscent of the following

Definition 1.17 Let C be any category and E, M ⊂ C two classes of maps in C such that

(i) E and M both contain, and are both closed under composition with, all isomorphisms of C,

(ii) any map f of C can be written as f = e; m with e ∈ E and m ∈ M, and

(iii) if the square

Y  [figure: e] X

.............. h

[figure: X′′; v; ⊂; m; X′; f]

commutes in C, where e ∈ E and m ∈ M, then there is a unique h : X → X′′ such that e; h = v and h; m = f

Then we say that (E, M) is a factorisation system for C.

Exercise 1.18 Show that the inclusion functor M ⊂ C is stable, where E is the class of candidates. Conversely, any stable functor which is surjective on objects and faithful (injective on morphisms) is of this form.

Warning 1.19 There is a clash of terminology here. A stable factorisation system is one such that in the pullback

[figure: Y′; e′; I′; m′; X′; Y; e; I; ⊂; m; X; f]

if e ∈ E and m ∈ M (with f arbitrary) then also e′ ∈ E and m′ ∈ M. This is particularly important in the best-known case (epi-mono factorisation), because for instance we need it to interpret existential quantification in categorical logic. Is there a corresponding notion of stably stable functor?

1.4 Polycolimits

We shall now consider when certain basic structural functors are stable. This leads us to generalisations of colimits which some authors have (mistakenly) taken as the definition of stable domains. The prefix “poly” was suggested by Lamarche, who was the first to observe that Diers’ “multi” work could be generalised in the way in which we have done it in this paper.

Lemma 1.20 The terminal projection !_{X} : X → 1 is stable iff every object X ∈ X has some map I → X where I ∈ X is a polyinitial candidate, i.e. for every f : I → X and g : X′ → X

I

[figure: h]

[figure: X′; g; X; f]

there is a unique h : I → X′ such that h; g = f. If X has this property then π_{0} : X × Y → Y is also stable. Proof Easy special case of candidacy of u : • = !_{X} (I) in 1 = {•}. □

Observe that this property is vacuously satisfied by the empty category, although the polyinitial family is then empty. The family for the disjoint union of several categories with this property is simply the disjoint union of the respective families. Indeed each component has a polyinitial candidate, which is unique up to isomorphism, but unlike (ordinary) initial objects this may have nontrivial isomorphisms. In fact the polyinitial family is a groupoid.

Example 1.21 A poset X has a polyinitial family iff every component has a least element. Hence being a polyinitial candidate is intermediate between being least and minimal: we may say that it is locally least. □

Stability of the terminal projection !_{X} : X → 1 provides the simplest example to illustrate the necessity of the solution set condition.

Example 1.22 On denotes the ordered class of ordinals (well-founded linearly ordered sets). On^{op} has all small limits (calculated as unions of ordinals) and the terminal projection preserves them, but the solution set condition fails and there is no (poly)initial object. □

Definition 1.23 Let X, Y ∈ X. A polycoproduct candidate is an object C ∈ X together with a pair of maps ν_{0} : X → C and ν_{1} : Y → C such that given another pair n_{0} : X → Z′ and n_{1} : Y → Z′ which is compatible in the sense that we are also given f : C → Z and g : Z′ → Z such that ν_{i} ; f = n_{i} ; g, there is a unique h : C → Z′ making the whole diagram commute.

X  \overline{ν_{0}} C
[figure: n_{0}; f]
Z
ν_{1}  [figure: g]
[figure: Y; n_{1}; Z′; h; . . . . . . . . . . . . . . . . . . . . . . . .]

Similarly we define polycolimit candidates and in particular polycoequaliser candidates.

Example 1.24 Let X be a poset. We say C is a minimal upper bound or mub of a set I ⊂ X if I ≤ C and if I ≤ Z′ ≤ C then Z′ = C. The pair I has a complete set of mubs if whenever I ≤ Z then there is some mub C with C ≤ Z. Then

(a) I has a polycoproduct (or multijoin) family iff it has a complete set of mubs, and the mub C ≤ Z is unique.

(b) X has multijoins of all subsets iff every slice of X is a complete lattice, i.e. it has wide pullbacks. □

Exercise 1.25 In the category Fld, construct all polycoproduct candidates of a pair of finite extensions of ℚ. [Hint: form their tensor product as vector spaces and decompose this as a direct sum.] Describe the result in terms of roots of polynomials, and hence determine necessary and sufficient conditions for the polycoproduct to be discrete or connected.

Exercise 1.26 Show that Δ : X → X × X is stable iff X has polycoproducts, and Δ : X → X^{⇉} is stable iff X has polycoequalisers. More generally Δ : X → X^{I} is stable iff X has polycolimits of type I, where X^{I} is the category of diagrams of type I, i.e. all functors from I to X. □

Exercise 1.27 Suppose u_{i} : X_{i} → S_{i}Z_{i} (i = 1, 2) are candidates for S_{i} : Z → X_{i} and that (ν_{i} : Z_{i} → Z) is a polycoproduct candidate in Z. Then u = ⟨u_{1} ; S_{1}ν_{i}, u_{2} ; S_{2}ν_{2}⟩ is a candidate for ⟨S_{1}, S_{2}⟩ : Z → X_{1} × X_{2}. [Hint: Use candidacy to give mediators h_{i} : Z_{i} → Z′′, and the coproduct candidate to give h : Z → Z′′; this is actually a special case of Exercise 1.1.5.] □

Proposition 1.28 The category whose objects are categories with polyinitial and binary polycoproduct families and whose morphisms are stable functors has binary products and a terminal object. Proof It only remains to show the factorisation property for ⟨S_{1}, S_{2}⟩ : Z → X_{1} × X_{2}. Any map w : ⟨X_{1}, X_{2}⟩ → ⟨S_{1}, S_{2}⟩Z of X_{1} ×X_{2} is of the form w = ⟨u_{1} ;S_{1}f_{1}, u_{2} ;S_{2}f_{2}⟩, where u_{i} : X_{i} → S_{i}Z_{i} are candidates for S_{i} and f_{i} : Z_{i} → Z. Let Z′ be a polycoproduct candidate with ν_{i} : Z_{i} → Z′ and f = [f_{1}, f_{2}] : Z′ → Z, so that f_{i} = ν_{i} ; f. One can show that u = ⟨u_{1} ; S_{1}ν_{i}, u_{2} ; S_{2}ν_{2}⟩ is a candidate, and w = u; ⟨S_{1}, S_{2}⟩f. □

1.5 The Spectrum and the Trace

For fixed Y ∈ Y, we define the S-spectrum, Spec_{S}(Y), to be the collection of all candidates Y → SX. The term is justified by Diers’

Example 1.29 With S : IntDom → CRng, the S-spectrum of a ring is its Zariski spectrum, i.e. the set of (quotient projections corresponding to) prime ideals.

Diers [D84] defines a topology on the S-spectrum which in this case gives the Zariski topology. We cheated a bit there, because we identified isomorphic quotient maps. We should instead

take the category whose objects are candidates u : Y → SX and whose morphisms h : u′ → u are X -morphisms h : X′ → X such that u = u′ ; Sh.

Proposition 1.30 Spec_{S}(Y) is a groupoid, i.e. a category in which every morphism is invertible. Moreover if X and Y have equalisers then S preserves them iff the groupoid is discrete, i.e. the identity is the only endomorphism of any object, and isomorphic objects are uniquely so. Proof The first part is immediate from the definition of candidacy. The second is an exercise.

□

A good example of a groupoid is the set of paths in a topological space: the common definition of the Fundamental Group (the set of loops) of a connected space depends arbitrarily on a choice of basepoint. If we select a particular point in each component and take the fundamental group, we obtain a groupoid which has just one object in each connected component, which we may view as a family of groups. These two groupoids are weakly equivalent: any choice of basepoints determines a functor from the smaller to the larger which is full, faithful and essentially surjective, but to obtain a (pseudo)inverse we need also to choose a path from each point to the chosen basepoint of its path-component.

From the point of view of abstract theory the larger groupoid is preferable because it avoids these choices, which may in subsequent constructions also involve natural isomorphisms with attendant coherence conditions. However if we wish to do calculations (e.g. [T89]) it is more useful to consider a groupoid to be a family of groups (with repetitions according to the components). For an extensive discussion of the rôle of groupoids in topology and elsewhere, see [Br].

Example 1.31 Let p be a polynomial (say over ℤ) and X the category of fields in which p splits. Let S : X → Y be the forgetful functor to the category of all fields. Then the S-spectrum of a field is the Galois group of the polynomial over the field, i.e. the group of automorphisms of the extension splitting p.

In the case of a discrete groupoid, we may regard the morphism-set as an equivalence relation on the object-set, and the number (but not the size) of components is an invariant under categorical equivalence; hence we treat a discrete groupoid as the set of its components. A homomorphism of discrete groupoids gives rise to a function between the sets of components.

Varying Y, we can look for a functor, Spec_{S} : Y → Gpd^{op}. For suppose y : Y′ → Y and u : Y → SX is a candidate; then we can apply the factorisation property to get y ; u = u′ ; Sx for some candidate u′ : Y′ → SX′ and x : X′ → X. Unfortunately this is only defined up to isomorphism, and we must make do with a “pseudofunctor” with coherences.

Exercise 1.32 Express the fundamental theorem of Galois Theory in terms of this pseudofunctor.

Exercise 1.33 It is common to define adjoint functors C ⊣ H by the pleasantly symmetrical condition that morphisms Y → HX in Y and CY → X in X are in natural bijection. Show how to make Spec_{S} into a “polyfunctor” whose result is not a single object but a groupoid of objects of X and formulate the corresponding notion that it is polyadjoint to S, including naturality. What corresponds to the unit and counit?

Both spectra and polyadjoints seem a very complex way of presenting the data. A better approach is to collect everything together into a single category.

Definition 1.34 The trace of a stable functor S : X → Y is the category T for which:

• The objects are the triples T = (X, Y, Y →^{u} SX) where u is a candidate.

• The morphisms from T_{1} = (X_{1}, Y_{1}, Y_{1} →^{u_{1}} SX_{1}) to T_{2} = (X_{2}, Y_{2}, Y_{2} →^{u_{2}} SX_{2}) are the pairs t = (X_{1} →^{x} X_{2}, Y_{1} →^{y} Y_{2}) such that the square

[figure: Y_{1}; u_{1}; SX_{1}; X; Y_{2}; y; u_{2}; SX_{2}; Sx; X_{2}; x]

commutes. Note that x, and not just Sx, is part of the data.

There are two obvious functors C : T → X and F : T → Y, which simply extract the first and second components of the objects and morphisms.

This structure is more complex than the one Girard calls the trace. The reason is that in his examples every object can be expressed uniquely as a colimit of colimit-irreducibles, and because of the following result we need only consider the irreducible objects of the trace.

Lemma 1.35 ⟨C, F ⟩ : T → X × Y creates colimits. Proof Let u_{i} : Y_{i} → SX_{i} be vertices of a diagram in T and X = colim X_{i} and Y = colim Y_{i}. Since Y is a colimit there is a mediating map u : Y → SX (it is not necessary that S preserve the colimit), so consider

[figure: Y_{i}; Y; SX′′]

[figure: ..................................; ..............]

[figure: SX_{i}; u_{i}; SX; u; Sf; SX′; Sg]

Then we have h_{i} : X_{i} → X′′ and hence a mediating map h : X → X′′ as required. It is easy to show that this is unique. □

Observe that the trace is closed under composition with isomorphisms on either side. In fact it is useful to formalise this as follows:

Notation 1.36 For a category X,

(a) let X̃ be the groupoid whose objects are those of X and whose morphisms are the isomorphisms of X;

(b) let X^{≅} be the category of functors from • ≅ • (which has two vertices, their identities and a pair of mutually inverse arrows) to X; this has objects all isomorphisms Y ≅ Y′ of Y, and morphisms commutative squares.

Exercise 1.37 Show that Y^{≅} is trace of the identity on Y. There is a canonical weak weak equivalence Y → Y^{≅} which has two obvious pseudo-inverses but is not an isomorphism. Show that either functor Y^{≅} → Y is a (non-split) fibration (and an opfibration) for which the fibre over Y is equivalent to Aut_{Y}(Y). □

Proposition 1.38 Let S : X → Y be a stable functor; then its trace carries an action of Ỹ on the left and X̃ on the right:

(Y′ →^{y} Y) · (Y →^{u} SX) · (X →^{x} X′) = (Y′ ^{y;u;Sx} SX′)

If T : Y → Z is another stable functor then the trace of T S : X → Z is given by tensor product over Ỹ. The unit of the tensor product at Ỹ is Y^{≅}. Proof The action speaks for itself. Recalling exercises 1.1.5 and 1.2.3, candidates w : Z → T SX factor as w = v; T u, where u : Y → SX and v : Z → T Y are candidates for S and T respectively. This factorisation is unique up to isomorphism in the sense that if w = v′; T u′ is another one (via Y′) then v′ = v ; T h and u′ = h^{−1} ; u for some (unique) h : Y ≅ Y′. Hence candidates for T S correspond bijectively to equivalence classes of pairs of candidates for S and T, which are precisely the objects of the tensor product. The remaining details are left as an exercise. □

Just as the groupoid of paths avoids the choice of basepoint and canonical paths from it to other points, so the trace of a functor which “has” a left adjoint (for example which satisfies the conditions of the adjoint functor theorem) avoids the choice of the adjoint. This observation is both a potential pitfall and a tidy way of accounting for structures which exist only in an “up to isomorphism” sense.

1.6 The Trace Factorisation

In this and the next section we shall show that the trace of a stable functor is the intermediate object for a factorisation system.

Lemma 1.39 There is a functor H : X → T such that S = F H, and a natural transformation ϵ : CH → id_{X}. Proof Applying the decomposition to the identity,

SX  \overline{u} SX′

[figure: id]

SX \begin{matrix}Sx \\  \end{matrix}

where x : X′ → X and u is a candidate. Now put HX = (X′, SX, u), so F HX = SX and CHX = X′, and ϵ_{X} = x.

For the effect of H on morphisms, let ξ : X_{1} → X_{2} in X, where id_{X_{1}} = u_{1} ; Sx_{1} and id_{X_{2}} = u_{2} ; Sx_{2}. Then the rectangle

[figure: SX_{1}; Sξ; SX_{2}; u_{2}; SX′_{2}]

.................................. Sk

[figure: SX′_{1}; u_{1}; Sx_{1}; SX_{1}; Sξ; SX_{2}; Sx_{2}]

commutes, since the maps SX_{1} → SX_{1} and SX_{2} → SX_{2} are identities. By candidacy of u_{1} there is a unique fill-in k : X′_{1} → X′_{2} such that Sξ ; u_{2} = Sk ; u_{1} and k ; x_{2} = x_{1} ; ξ. The first expresses the fact that Hξ = (k, Sξ) : (X′_{1}, SX_{1}, u_{1}) → (X′_{2}, SX_{2}, u_{2}) is a morphism, whilst the second says that ϵ : CH → id is natural, since CHξ = k and F Hξ = ξ. □

Observe that the components X′ = CHX and u of HX = (X′, SX, u) and x = ϵ_{X} are only defined up to isomorphism: we have to make a Choice from the isomorphism class for each X.

Exercise 1.40 If H′ and ϵ′ : CH′ → id is another choice, then there is a unique natural isomorphism τ : CH′ → CH such that ϵ′ = τ ; ϵ and ⟨τ, id⟩ : H′ ≅ H. (The second component has to be id_{S} : F H′ = F H.) □

Lemma 1.41 There is a unique map η_{T} : T → HCT for each T = (X, Y, v) ∈ T such that Cη_{T} ; ϵ_{CT} = id_{X} and F η_{T} = v. Proof Using candidacy of (the vertical) v in the commutative square

[figure: Y; v; SX; u; SX′]

.................................. Sh

[figure: SX; v; Sid_{X}; SX; Sϵ_{X}]

there is a unique h : X → X′ such that v ; u = v ; Sh and h; ϵ_{X} = id. With

η_{T} = (h, v)

so that Cη_{T} = h and F η_{T} = v, the first equation says that η_{T} is a morphism, and the second is the triangular identity. □

Exercise 1.42 Show that η is natural. □

Lemma 1.43 η_{HX} ; Hϵ_{X} = id_{HX} for each X ∈ X. Proof Consider the commutative diagram

[figure: SX′; Sx; SX; u; SX′]

[figure: id; ..................................; Sh]

[figure: SX; u; SX′; u′; SX′′; u′; Sx′; SX′; Sx; SX; Sx]

[figure: ..................................; Sk; id]

[figure: SX′; u; id; SX′; Sx′]

where u and u′ are universal and u ; Sx = id_{SX}. The lower and upper rectangles have diagonal fill-ins, k and h, whilst the whole diagram has a fill-in which must be k ; h = id_{X′}. Now

η_{HX} ; Hϵ_{X} = (k, u) ; (h, Sx) = (id_{X′}, id_{SX}) = id_{HX}

as required. □ To sum up,

Proposition 1.44 Any stable functor S : X → Y admits a decomposition S = F H where H : X → T has a left adjoint C and F : T → Y is a fibration in which every map is horizontal, or equivalently in which the fibres are groupoids. Any functor with a left adjoint and any fibration of groupoids may occur in this way. Proof The fibration F corresponds to the indexation Spec_{S}, whose fibres are groupoids, i.e. all vertical maps are invertible and every map is horizontal. If S has a left adjoint C then for each Y ∈ Y there is a unique (up to unique isomorphism) candidate u : Y → SX, namely the unit of the adjunction at Y, and so in this case S = F H where C ⊣ H and F is an equivalence. On the other hand, if S is a groupoid-fibration then u : Y → SX is a candidate iff it is invertible (exercise), whence H is an equivalence. □

This is not quite satisfactory, because the class of groupoid fibrations is not closed under (strong or weak) equivalence (it is under isomorphism). The following example illustrates that these 2-categorical quibbles often have important algebraic content.

Exercise 1.45 Let X and Y be groups and S : X → Y any group homomorphism. Then S is stable, and in its factorisation S = F H, H is an equivalence. However S is a fibration iff it is surjective. □

The following is more appropriate:

Definition 1.46 An isotomy (Greek: “equal cuts”) is a functor which restricts to a weak equivalence on each slice (cf. Lemma 1.2.4).

Lemma 1.47 A S : T → Y is an isotomy iff

(i) it is essentially surjective on slices, i.e. for every y : Y → F T in Y there is some T′ ∈ T , with t : T′ → T in T and u : F T′ ≅ Y in Y such that F t = u; y. We call t : T′ → T a lifting of the map y : Y → F T.

(ii) and it is full and faithful on slices, i.e. for t_{1} : T_{1} → T and t_{2} : T_{2} → T, for every g : F T_{1} → F T_{2} such that g ; F t_{2} = F t_{1} there is a unique f : t_{1} → t_{2} such that F f = g and f ; t_{2} = t_{1}. We call f the lifting of the triangle.

Then in (i), any two liftings of a given map are isomorphic, but not uniquely so. Proof (i) and (ii) are just the definition of a weak equivalence. For the last part, suppose u_{1} : F T_{1} ≅ Y and u_{2} : F T_{2} ≅ Y; then apply (ii) to g = u_{1} ; u_{2}^{−1} and its inverse to get f : T_{1} ≅ T_{2}.

□

Corollary 1.48 A fibration in which every fibre is a groupoid is an isotomy, as is any equivalence and any composite of isotomies. Conversely any isotomy is equivalent to a groupoid-fibration. Proof Use the factorisation. □

This characterisation and the following two properties are what we shall use most.

Exercise 1.49 Isotomies reflect isomorphisms and create wide pullbacks. □

1.7 Universality of the Factorisation

In order to complete the proof that functors with left adjoints and isotomies provide a factorisation system (Definition 1.3.3) we need to show a diagonal fill-in property. However, since we are working in a 2-category, there is a more general (“lax”) property, which is the technical basis of our work in the final section.

Definition 1.50 Let C′ : T′ → X and H′ : X → T′ be adjoint (C′ ⊣ H′), F : T → Y an isotomy and A : X → T and B : T′ → Y any two stable functors. Then a diagonal is a functor Φ : T′ → T together with a natural transformation α̃ : Φ → AC′ and a natural isomorphism ω : F Φ → B. Two diagonals (Φ_{1}, α̃_{1}, ω_{1}) and (Φ_{2}, α̃_{2}, ω_{2}) are isomorphic if there is a natural isomorphism τ : Φ_{1} → Φ_{2} such that α̃_{1} = τ ; α̃_{2} and ω_{1} = F τ ; ω_{2}.

This is illustrated by the following diagram:

T′

[figure: C′] ∖ [figure: H′]  [figure: B]

X \begin{matrix}⇐ \\ = \\ = \\ = \\ = \\ = \\ = \\ α \end{matrix} = ≅ ; ω ⇒ Y

[figure: A; F]

TΦ

In fact after we have achieved our initial purpose, we shall only be interested in the case where A also has a left adjoint. In this case it is more convenient to consider the adjoint transpose α of α̃.

Lemma 1.51 Φ is a stable functor. Moreover if B is an isotomy, so is Φ. Proof We must show that it has a left adjoint (respectively, it is an equivalence) on each slice. But there it is isomorphic to F^{−1}B for some choice of inverse for the isotomy F on the slice. □

Proposition 1.52 The equation

F α̃ = ω ; Bη′ ; ϕ_{C′}

where η′ is the unit of C′ ⊣ H′, determines a bijection between natural transformations ϕ : BH′ → F A and isomorphism classes of diagonals. Proof Let T′ ∈ T′ and consider

T′  \overline{η′_{T′}} H′C′T′  T′

[figure: F ΦT′; ω_{T′} ; ≅; BT′; Bη′_{T′}; BH′C′T′; ϕ_{C′T′}; F AC′T′; Y; B]

[figure: ΦT′; α̃_{T′}; AC′T′; T; F]

where α̃_{T′} : ΦT′ → AC′T′ is obtained by lifting the map Bη′_{T′} ; ϕ_{C′T′} along the isotomy and the given equation is satisfied. This is determined up to isomorphism, but is otherwise arbitrary, i.e. τ_{T′} : Φ_{1}T′ ≅ Φ_{2}T′ subject to the equations defining isomorphism of diagonals.

Functoriality of Φ and naturality of α̃, ω and τ demand some care. For each T′ ∈ T′ we make an arbitrary Choice of ΦT′ ∈ T and α̃_{T′} : ΦT′ → AC′T′ such that F α̃_{T′} = η′_{T′} ; ϕ_{C′T′}. Now for a morphism t′ : T′_{1} → T′_{2} the rectangle

[figure: F ΦT′_{1}; ω_{T′_{1}}; BT′_{1}; Bη′_{T′_{1}}; BH′C′T′; ϕ_{C′T′_{1}}; F AC′T′_{1}; F ΦT′_{2}; ω_{T′_{1}} ; Bt′ ; ω_{T_{2}}^{−1}; ω_{T′_{2}}; BT′_{2}; Bt′; Bη′_{T′_{2}}; BH′C′T′; BH′C′t′; ϕ_{C′T′_{2}}; F AC′T′_{2}; F AC′t′]

commutes. Three sides are already images of maps under F,

[figure: ΦT′_{1}; α̃_{T′_{1}}; AC′T′_{1}; ΦT′_{2}; . . . . . . . . . . . . . . . .; α̃_{T′_{2}}; AC′T′_{2}; AC′t′]

and so there is a unique lifting Φt′ : ΦT′_{1} → ΦT′_{2} of the “triangle” such that F Φt′ = ω_{T′_{1}} ; Bt′; ω_{T_{2}}^{−1}. Hence α̃ and ω are natural essentially by definition, and (using uniqueness) Φ is easily shown to be functorial. Naturality of τ : Φ_{1} → Φ_{2} is similar.

We can recover ϕ from (Φ, α̃, ω) because in the following diagram,

[figure: BH′X; Bη′_{H′X}; BH′C′H′X; BH′ϵ′_{X}; BH′X; F ΦH′X; ω_{H′X}; F α̃_{H′X}; F AC′H′X; ϕ_{C′H′X}; F Aϵ′_{X}; F AX; ϕ_{X}]

the left-hand square commutes by construction and the right-hand one by naturality of ϕ, the top row being an identity by C′ ⊣ H′ (of which the counit is ϵ′). If α̃ and ω are natural then so is ϕ, by composition; moreover this diagram now shows that the processes ϕ ↦ α and α ↦ ϕ are inverse. □

Corollary 1.53 If ϕ is an isomorphism then so is δ = α̃_{H′} ; Aϵ′ : ΦH′ → A. Proof F δ_{X} in the previous diagram is invertible, and isotomies reflect isomorphisms. □

Theorem 1.54 With E = {functors with left adjoints} and calM = {isotomies}, we have a factorisation system (in an “up to isomorphism” sense). Proof Every equivalence and every composite of functors with left adjoints has a left adjoint, and likewise with isotomies, and we have shown how to factorise arbitrary stable maps. The preceding corollary says that if the square (1.3.3(iii)) commutes up to isomorphism ϕ then a diagonal Φ exists, uniquely up to (unique) isomorphism τ, such that the triangles commute up to isomorphisms ω and δ. □

Corollary 1.55 Any factorisation of a stable map into a functor with a left adjoint and an isotomy is weakly equivalent to the standard trace which we have constructed, and in this T = (CT, F T, F η_{CT}). Proof There is a standard diagonal (Φ, α̃, ω) from an arbitrary factorisation to the standard one, where α and ω are identities and Φ is a weak equivalence. □

As we demonstrate the properties of stable functors, it is helpful to bear in mind what can be done with ordinary ones. In some cases it might be argued that (to deal with a more difficult subject) we have simply used more ingenuity, and that the same ideas would work just as well with traditional category or domain theory. As a rule, we find that the ideas do work, up to a point, but they only work properly in the stable context.

Exercise 1.56 Show that any functor S factorises (in a more or less similar way to this) as a functor with a left adjoint followed by a fibration. The intermediate object, Y ↓ S, we call the Scott-trace because it is essentially what is involved in his information systems [S82]. The trace of a composite X → Y → Z is given by tensor product over Y.

However this is not a factorisation system, because the diagonals are not unique. In a factorisation system, E ∩ M consists exactly of the isomorphisms (equivalences), but there are nontrivial fibrations with left adjoints, for instance the display of an indexed domain.

2 Applications

2.1 Continuity

In the majority of mathematical and computing applications, stable functors arise as forgetful functors between categories of models of finitary theories, and so preserve filtered colimits [ML, p207]. In the poset case these are known as directed joins (written ⋁ ; ), and there is an established computer science tradition (which we shall adopt) of calling functions which preserve them (Scott- )continuous. We shall often take our categories to have, and our functors to preserve, small filtered colimits; in particular we shall need pullback against morphisms in stable categories to (exist and) be continuous functors.

One ought, however, to be aware that there are important examples of theories involving ℵ_{0}-ary operations, notably metric spaces and indeed anything involving ℝ. For these cases, we replace “finite” by “countable” and ω by ω_{1} throughout the discussion; in particular the functors preserve colimits of ω_{1}- but not ω-sequences. Having said that, we shall stick to the finitary case from now on.

Lemma 2.1 Let Y have small filtered colimits and G : X → Y be a functor such that G : X /X → Y/GX is continuous for each X ∈ X. Then G is itself continuous. Proof Let X = colim^{↑} X_{i} be a filtered colimit in X, and Y = colim^{↑} GX_{i} the colimit of the image in Y, so that there is a mediating map y : Y → GX from the colimit to the cocone GX_{i} → GX. Consider Y/GX: by hypothesis on G : X /X → Y/GX, the cocone GX_{i} → GX is colimiting in this slice. Now the mediator y : Y → GX makes GX_{i} → Y into a cocone in Y/GX, and so there is a mediating map from the colimit, i.e. x : GX → Y. Now it is easily shown using the universal properties that x and y are mutually inverse. □

Corollary 2.2 Let F : T → Y be an isotomy, where T has small filtered colimits and Y is a stable category, i.e. it has small filtered colimits and its slices belong to a specified class which is closed under categorical equivalences. Then T and F are stable. Proof Equivalences preserve filtered colimits and have left adjoints. □

Exercise 2.3 Why is it necessary to assume that Y in the lemma, and both Y and T in the corollary, have filtered colimits, but not that the isotomy F preserves them?

Exercise 2.4 Generalise these results to colimits and polycolimits.

Lemma 2.5 If S = F H is continuous then so is H. Proof Let X = colim^{↑} X_{i}, where id_{X_{i}} = u_{i} ; SX_{i} defines HX_{i}.

[figure: SX; u; SX′; Sx; SX; SX_{i}; u_{i}; SX′_{i}; Sx_{i}; SX_{i}]

Let X′ = colim^{↑} CHX_{i} and id_{X} = u ; Sx be the mediating maps, using continuity of S. By the previous lemma, u is a candidate and so by uniqueness of factorisation HX = (X′, SX, u). □

Proposition 2.6 If S is continuous then so is the pseudofunctor Spec_{S} : Y → Gpd^{op}. Proof In other words, it maps a filtered colimit Y = colim^{↑} Y_{i} in Y to a cofiltered limit of groupoids. Specifically, (X, Y, u) ∈ Spec_{S}(Y) corresponds to the compatible family (X_{i}, Y_{i}, u_{i}) ∈ Spec_{S}(Y_{i}), where y_{i} ; u = u_{i} ; Sx_{i} and x_{i} : X_{i} → X and y_{i} : Y_{i} → Y are the colimiting cocones; in fact (X, Y, u) = colim^{↑}(X_{i}, Y_{i}, u_{i}) in T . Making this argument, or indeed the statement, rigorous would require a tortuous discussion of coherence for pseudofunctors. □

The reader will have guessed that S and F stand for “stable” and “fibration” respectively; the origin of C and H is the

Definition 2.7 A homomorphism is a continuous functor with a left adjoint, called a comparison. A comparison which is full and faithful is called an embedding, and its adjoint a projection.

Embedding and projection are standard in computer science, whilst the (perhaps unfortunate) term homomorphism migrated [T87] from the theory of continuous lattices and locally finitely presentable categories. Comparisons in domain theory behave like instances of the order relation inside domains, as we shall see in the next section.

Definition 2.8 Y ∈ Y is finitely presentable if whenever f : Y → colim^{↑}_{i∈I} Z_{i} in Y, there is some (not unique) i_{0} ∈ I and g : Y → Z_{i_{0}} such that f = g ; z_{i_{0}} where z_{i_{0}} : Z_{i_{0}} → colim^{↑}_{i∈I} Z_{i} belongs to the colimiting cocone.

Exercise 2.9 If u : Y → SX is a candidate, S is continuous and Y is finitely presentable then X is also finitely presentable. More abstractly, isotomies and embeddings create, and comparisons preserve, finite presentability. □

2.2 Stability with Equalisers

Our objective is to deal mainly with the notion of stability which does not involve equalisers, i.e. that due to Lamarche, who has observed that we do not obtain cartesian closure in Diers’ version. However it is quite easy to see what restriction needs to imposed to recover the case with equalisers. Recall that a discrete fibration has every fibre a set, so we make the

Definition 2.10 An isotomy F : T → Y is discrete if it reflects identities, i.e. if t : T → T with F t = id_{F T} then t = id_{T}.

Lemma 2.11 Discrete isotomies create equalisers. Proof Let f, g : T_{1} ⇉ T_{0} in T and suppose that the equaliser e : Y → F T_{1} of F f, F g : F T_{1} ⇉ F T_{0} exists in Y. Then the square on the left commutes

[figure: Y; e; F T_{1}; F T_{1}; e; F g; F T_{0}; F f; T; u; T_{1}; T_{1}; v; g; T_{0}; f]

and so we can lift one e to u and since F is full and faithful there is a unique v lifting the other (a priori not the same). Now u : T → T_{1} and v : T → T_{1} are two different liftings of the same e : Y → F T_{1}, and hence are isomorphic, i.e. u = t; v for some automorphism t of T_{1} with F t = id_{F T_{1}}. Since F is discrete we must have t = id_{T_{1}} and hence u = v. I claim this is the equaliser of the given pair; for if w : T′ → T_{1} satisfies w ; f = w ; g then we have a unique mediating map y : F T′ → Y = F T with y ; e = F w, and this can be lifted to a (unique) mediating map T′ → T as required. □

Exercise 2.12 Show that discreteness is necessary. Hint: consider the unique function from the two-element group to the trivial group. □

Proposition 2.13 Suppose X and Y have equalisers. Then S : X → Y preserves equalisers iff F : T → Y is a discrete isotomy. Proof We already know that functors with left adjoints and discrete isotomies preserve equalisers. Conversely let t be an automorphism of T = (X, Y, Y →^{u} SX) ∈ T such that F t = id_{F T}; then t = (id, f) for some f : X → X. Hence the composites

[figure: Y; u; SX; id; Sf; SX]

are equal, so that if we let

[figure: X′′; ⊂; g; X; id; f; X]

be the equaliser (which is preserved by S) there is a (unique) v : Y → SX′′ making the square

Y  \overline{u} SX

.............. Sh

[figure: SX′′; v; Sg; SX; Sid_{X}]

commute. Then there is some (unique) h : X → X′′ such that (u; Sh = v and) h; g = id_{X}. Hence g is epi and f = id_{X}. □

Lemma 2.14 Any diagonal between functors preserving equalisers also does so. Proof In Definition 1.7.1, B preserves and F creates them. □

Theorem 2.15 With E = {functors with left adjoints} and calM = {discrete isotomies}, we have a factorisation system for discretely stable maps. □

Exercise 2.16 Show that equalisers and (ordinary) pullbacks suffice to construct any finite connected limit, and hence that equalisers, pullbacks and cofiltered limits, or equalisers and wide pullbacks, suffice for arbitrary connected limits (cf. Exercise 1.2.9). □

Exercise 2.17 Show that any equaliser may be computed using pullbacks, the cofiltered limit of an ω-sequence and the fixed-point set of an involution, i.e. (the equaliser with the identity of an) automorphism h of an object such that h; h = id. [Hint: repeatedly take pullbacks, and compare odd and even terms of the ω-limit.]

Exercise 2.18 If the polycoequaliser of a parallel pair f, g : X ⇉ Y in X is nonempty then it has an equaliser, and this is preserved by any stable functor out of X. [Hint: let Z = Y ×_{Q} Y and E = X ×_{Z} Y.] □

Corollary 2.19 If X has a terminal object then every stable functor S : X → Y preserves equalisers. □

Question 2.20 Is the converse true, i.e. if the equaliser of a parallel pair is preserved by all stable functors then it has a nonempty polycoequaliser?

2.3 Girard’s Examples

Diers gives so many examples of the trace factorisation as a kind of spectrum, and the connection between his work and ours is sufficiently clear, that it is unnecessary to give mathematical examples here. The present author actually discovered the factorisation for himself by generalisation of Girard’s work, but since it is far from obvious how Berry and Girard’s trace relates to ours, we shall now present it in Girard’s form.

In these examples, “stable” means continuous as well, but not necessarily discrete. Hence if u : Y → SX is a candidate and Y is finitely presentable then so is X (Exercise 2.1.9). In fact in each case finitely presentable is the same as finite (in the representation), and every object is a filtered colimit of finite ones.

Definition 2.21 A qualitative domain [G85] is a family, X, of subsets X of an arbitrary set (which is written |X | = ⋃ X) such that

(i) if X′ ⊂ X ∈ X then X′ ∈ X

(ii) if X = ⋃ ; X_{i} with X_{i} ∈ X then X ∈ X.

[If in addition,

(iii) if ∀x_{1}, x_{2} ∈ X.{x_{1}, x_{2}} ∈ X then X ∈ X

then we call X a coherence space [GLT]; in this case the domain is determined by the set |X | together with a binary relation, x_{1} ⌢ ⌣ x_{2} ⟺ {x_{1}, x_{2}} ∈ X.] We consider a qualitative domain to be a category with objects X and morphisms the subset inclusions X′ ⊂ X.

Lemma 2.22 Let S : X → Y be a monotone function between qualitative domains. Then (a) S is continuous iff SX = ⋃ ; {SX′ : X′ ⊂ X finite}

and if this holds then

(b) S is stable iff whenever X_{1} ∪ X_{2} ∈ X we have S(X_{1} ∩ X_{2}) = SX_{1} ∩ SX_{2}

in which case

(c) Y ⊂ SX is a candidate iff X is minimal for this inclusion. Proof [a] is standard and means that we only need test [b] for finite X; then X /X = P(X), which is finite, so preserving pullbacks, i.e. finite limits in slices, suffices to give a left adjoint. Finally for [c], using pullbacks it is easy to show that if Y ⊂ SX_{0} then there is a unique minimal X ⊂ X_{0} with Y ⊂ SX. (Note that since X is a poset, we may forget the name, u, of the inclusion.)

□

Since slices of qualitative domains are complete atomic Boolean algebras, it is easy to show that X is minimal with Y ⊂ SX iff X = ⋃_{y∈Y} X_{y} where X_{y} is minimal with y ∈ SX_{y}. Hence we have the

Proposition 2.23 The trace of a stable function S : X → Y is isomorphic to the qualitative domain given by

|T | = {(X, y) | y ∈ SX, where X is minimal such (and finite)}
T  = {T ⊂ |T | |⋃{X | (X, y) ∈ T } ∈ X }

The isomorphism is given by (X, Y, u) ↔ {(X_{y}, y) : y ∈ Y }. Also

SX = {y ∈ |Y| | (X′, y) ∈ |T | ∧ X′ ⊂ X}
CT = ⋃{X | (X, y) ∈ T }
F T = {y | (X, y) ∈ T }
HX = {(X′, y) | (X′, y) ∈ |T | ∧ X′ ⊂ X}

The formulae for |T | and SX are as given by Girard in [G85, §1.4] and [GLT, §8.5]. □

A natural transformation ϕ : S′ → S is simply the condition that S′X ⊂ SX for all X ∈ X; it is cartesian iff S′X′ = S′X ∩ SX′ for all X′ ⊂ X ∈ X. As we shall see in lemmas 3.1.4 and 3.1.6, a natural transformation ϕ is cartesian iff it has the property that u′ is a candidate for S′ iff u′; ϕ_{X} is a candidate for S. In this case, X is minimal with y ∈ S′X iff it is also minimal with y ∈ SX. In other words,

Lemma 2.24 ϕ : S′ → S is cartesian iff |T′| ⊂ |T | and T′ = {T ∈ T | T ⊂ |T′|}. □

Proposition 2.25 [X → Y], the category of stable functors and cartesian natural transformations from X to Y is isomorphic to the qualitative domain with

|[X → Y]| = {(X, y) | X ∈ X , y ∈ |Y|, with X finite}
[X → Y] = \{S ⊂ |[X → Y]| | \begin{matrix}(X_{1}, y_{1}), ..., (X_{k}, y_{k}) ∈ S ∧ X_{1} ∪ ... ∪ X_{k} ∈ X \\ ⇒ & \{y_{1}, ..., y_{k}\} ∈ Y \\ (X_{1}, y), (X_{2}, y) ∈ S ∧ X_{1} ∪ X_{2} ∈ X & ⇒ & ⊥ \end{matrix} \}

The correspondence is that the objects (coherent sets) of this qualitative domain are exactly the traces, |T |, of stable functions. □

In [GLT] it is shown that coherence spaces model linear logic and polymorphism in a very clear way. By imposing an order relation on |X | (with the condition that each ↓ x be finite) and allowing X ∈ X only if it is down-closed in this order, we arrive at the event structure representation [CGW] of Berry’s dI-domains [B78,B79].

Definition 2.26 A quantitative domain [G88] is a category of the form Set^{A}, where A is a set. The objects of Set^{A} are A-indexed families of sets, or bags from A, i.e. sets or “vectors” of A-elements with multiplicity.

We shall show that stable functors Set^{A} → Set^{B} have power series expansions, although as they stand these domains and stable functors do not form a cartesian closed category.

Suppose S : Set^{A} → Set^{B} is stable, (X_{a}) ∈ Set^{A} and b ∈ B. Then elements w ∈ (SX⃗)_{b} are morphisms w : 1_{b} → (SX⃗), where 1_{b} is the singleton in the b component and empty elsewhere. Now by the factorisation property, such maps correspond to equivalence classes of pairs (u, x⃗) where u : 1_{b} → Sn⃗ is a candidate and f : n⃗ → X⃗. The notation n⃗ = (n_{a}) is used because the object is finite (and empty in all but finitely many components). The maps f : n⃗ → X⃗ are just elements of X⃗n⃗ = ∏_{A} X_{a}^{n_{a}}. In Girard’s notation (loc. cit., definition II.7), this gives a normal form w = (u; n⃗; f; X⃗)_{S}.

Proposition 2.27 Let S : Set^{A} → Set^{B} be a stable functor between quantitative domains; write d_{b,n⃗} for the set of candidates u : 1_{b} → Sn⃗. Then Aut(n⃗) acts on d_{b,n⃗} on the right, faithfully on each orbit; let c_{b,n⃗} be the set of orbits. Then

SX⃗ ≅ ∑_{n⃗} c_{b,n⃗} × X⃗n⃗

and conversely every functor of this form is stable. Proof By Proposition 1.5.10 we may write SX⃗ as a tensor product, where Aut(n⃗) acts on X⃗n⃗ on the left; but the action is faithful on orbits because of Corollary 2.2.10 and Proposition 1.5.2. □

Taking the case A = B = 1, it would appear that [Set → Set] ≃ Set^{ℕ}. However this is not the case, because the stable functor SX = X^{2} has two automorphisms, namely the identity and the “switch”, but the corresponding object 1_{2} ∈ Set^{ℕ} has only one automorphism. In fact the error was in replacing d_{b,n⃗} with its Aut(n⃗)-action by its set of orbits, and in fact cartesian transformations correspond bijectively to functions which preserve this action. However, as we have shown, not all actions are allowed: only those which are faithful on orbits, and we find [Set → Set] has no terminal object. We may describe higher function spaces in terms of groupoid actions, but the faithfulness conditions become more complicated [T89] (see also [Jy87] and [L90] for a different point of view on quantitative domains).

The third example (although historically Girard’s first [G81]) combines some of the features of both qualitative and quantitative domains. In fact Diers also cites linear orders as an example of a disjunctive theory, and Johnstone [Jh89] studied dilators from a categorical point of view, albeit not the same one as ours.

Definition 2.28 A linear order is a set X equipped with a relation < which is transitive and trichotomous, i.e. for each x, y ∈ X, exactly one of x < y, x = y or y < x holds. Write LOrd for the category of linear orders and strictly monotone functions, i.e. < is preserved and the maps are mono. A dilator is a continuous stable functor S : LOrd → LOrd.

In fact Girard was more interested in the case where dilators send ordinals to ordinals, which have (by definition) no non-trivial cofiltered limits, and it suffices to assume that dilators preserve (filtered colimits and) pullbacks. He showed that if a dilator sends countable ordinals to ordinals then it sends all ordinals to ordinals.

Unlike qualitative and quantitative domains, we shall not give an explicit formula for the effect of a dilator, but we shall prove Girard’s “normal form theorem” (loc. cit., 3.3.12).

Proposition 2.29 Let S : LOrd → LOrd be a dilator which preserves ordinals and ξ, ζ ∈ On with ζ < Sξ. Then there is a (least) number n ∈ ℕ, a sequence ξ_{0} < ξ_{1} < ⋯ < ξ_{n−1} < ξ of ordinals and an ordinal ζ_{0} ∈ Sn such that ζ = Sf(ζ_{0}) where f : i ↦ ξ_{i}. Proof Let ξ = X considered as an object of LOrd and w : 1 → SX be the morphism corresponding to ζ ∈ Sξ. By the factorisation property, w = u; Sf where u : 1 → Sn is a candidate (n is finite by continuity), corresponding to ζ_{0} ∈ Sn, and f : n → ξ, which corresponds to the sequence ⟨ξ_{i} = f(i) : i ∈ n⟩. □

Girard proved (loc. cit., Proposition 2.3.15) without recognising it that every natural transformation between dilators is cartesian.

3 Cartesian Transformations

3.1 Functors of Two Variables

So far in this paper we have been concerned with the examination of the trace of, essentially, a single functor, with only superficial regard to natural transformations. The rich mathematical applications which Diers found for this idea were undoubtedly the very reason why he paid only superficial regard to the class of all stable functors between two categories. (In [D80] he proved an analogue of Gabriel-Ulmer duality [GU], but 2-structure features only in the closing paragraphs, where he takes it for granted that it must be general natural transformations.) Indeed, although I suspect that cartesian transformations between stable functors have application to Number Theory, I have no examples at the moment.

We therefore have to turn to Berry for our motivation, which is to investigate cartesian closed 2categories of categories and stable functors. We require the evaluation functor ev : [X → Y]×X → Y to be stable, for which (unlike continuity) it is not sufficient that it be stable in each argument separately. In fact it must preserve the pullback square on the left:

[figure: ⟨S′, X′⟩; ⟨id_{S′}, ξ⟩; ⟨S′, X⟩; ⟨S, X′⟩; ⟨ϕ, X′⟩; ⟨id_{S}, ξ⟩; ⟨S, X⟩; ⟨ϕ, X⟩; S′X′; S′ξ; S′X; SX′; ϕ_{X′}; Sξ; SX; ϕ_{X}]

giving the square on the right (which expresses naturality of ϕ).

Definition 3.1 ϕ : S′ → S is a cartesian transformation if the naturality square is a pullback.

In fact we do not need to consider function-spaces but only products to come across this phenomenon, and so in this section we shall turn to functors out of a product, i.e. functors of two variables. It is well-known that a functor of two arguments is jointly (Scott-)continuous iff it is separately so, but in the case of stability there is an additional condition.

Definition 3.2 A functor S : X × Y → Z has orthogonal arguments if for any x : X′ → X in X and y : Y′ → Y in Y the square

S(X′, Y′) \overline{\begin{matrix}S(x, id_{Y′}) \\  \end{matrix}}S(X, Y′)

[figure: S(X′, Y); S(id_{X′}, y); S(x, id_{Y}); S(X, Y); S(id_{X}, y)]

is pullback in Z.

We aim to show that this is all we need in addition to separate stability to obtain joint stability, but it is simpler to see it first for functors which just preserve pullbacks.

Exercise 3.3 Show that the category whose objects are categories with pullbacks and whose morphisms are functors preserving pullbacks has finite products. Using the diagram

[figure: S(X_{1}, Y_{1}); S(id_{X_{1}}, y_{13}); S(X_{1}, Y_{3}); S(x_{13}, id_{Y_{3}}); S(X_{3}, Y_{3})]

[figure: S(X_{1}, Y_{2}); S(id_{X_{1}}, y_{12}); S(id_{X_{1}}, y_{24}); S(X_{1}, Y_{4}); S(id_{X_{1}}, y_{34}); S(x_{13}, id_{Y_{4}}); S(X_{3}, Y_{4}); S(id_{X_{3}}, y_{34})]

[figure: S(X_{2}, Y_{2}); S(x_{12}, id_{Y_{2}}); S(id_{X_{2}}, y_{24}); S(X_{2}, Y_{4}); S(x_{12}, id_{Y_{4}}); S(x_{24}, id_{Y_{4}}); S(X_{4}, Y_{4}); S(x_{34}, id_{Y_{4}})]

show also that a functor of two arguments preserves pullbacks jointly iff it preserves them separately and its arguments are orthogonal. □

Suppose that the arguments of S : X × Y → Z are orthogonal, and fix y : Y′ → Y in Y. It is convenient to make the abbreviations S = S(−, Y), S′ = S(−, Y′) and ϕ_{−} = S(id_{−}, y). This returns us to the special case of evaluation, since ϕ : S′ → S is a cartesian transformation.

Lemma 3.4 Let S, S′ : X → Z be functors and ϕ : S′ → S a cartesian transformation. Then u′ : Z → S′X in Z is a candidate for S′ iff u = u′ ; ϕ_{X} : Z → SX is a candidate for S. Proof Consider the following diagram:

Z  \overline{u′} S′X

[figure: t; v; S′h; S′f]

S′X′′  \overline{\begin{matrix}S′g \\  \end{matrix}}S′X′

SX \begin{aligned}ϕ_{X} \\ &  \end{aligned}

[figure: Sh; Sf]

[figure: SX′′; ϕ_{X′′}; Sg; SX′; ϕ_{X′}]

We are given f, g and either t or v.

[⇒] Given v, let t mediate the pullback and define h by candidacy of u′; then it mediates for u. Conversely h determines t = u′ ; S′h.

[⇐] Given t, put v = t; ϕ_{X′′} and define h by candidacy of u, so that f = h; g. Then v = u′; S′h both mediate for the pullback. But any h which makes the diagram commute mediates for u. The same diagram appears independently in [L88], but is used there in more restricted circumstances. □

Corollary 3.5 If S : X × Y → Z has orthogonal arguments then u′ : Z → S(X, Y′) is a candidate for S(−, Y′) iff u′ ; S(id_{X}, y) is a candidate for S(−, Y). □

Lemma 3.6 The converse of Lemma 3.1.4 is also true, assuming that S′ is stable: if postcomposition with ϕ preserves candidacy then it is cartesian. Proof We chase the same diagram again, using stability of S′ to factorise one of the sides of an arbitrary commutative square as u′ ; S′f. Define h by candidacy of u and put t = u′ ; S′h; conversely t determines h by candidacy of u′. □

Lemma 3.7 Let S : X × Y → Z be a functor with orthogonal arguments. Then u : Z → S(X, Y) is a candidate for S iff it is for both S(−, Y) and S(X, −). Proof “Only if” is obvious. Let ⟨f, g⟩ : ⟨X, Y ⟩ → ⟨X′, Y′⟩ and ⟨x, y⟩ : ⟨X′′, Y′′⟩ → ⟨X′, Y′⟩. By

Z  \overline{u}

[figure: S(X′, Y); S(f, id_{Y}); S(X, Y)]

[figure: S(id_{X′}, k)]

[figure: S(X′, Y′′); S(id_{X′}, y); S(X′, Y′); S(id_{X′}, g); S(f, id_{Y′}); S(X, Y′); S(id_{X}, g)]

[figure: S(h, id_{Y′})]

[figure: v; S(X′′, Y′′); S(x, id_{Y′′}); S(id_{X′′}, y); S(X′′, Y′); S(x, id_{Y′})]

Corollary 3.1.5, u ; S(id_{X}, g) is a candidate for S(−, Y′), so considering the square with vertices Z, S(X, Y′), S(X′, Y′) and S(X′′, Y′), there is a unique h : X → X′′ such that

f = h; x  and  u; S(h, g) = v ; S(id_{X′′}, y)

where we remember that S(id_{X}, g) ; S(h, id_{Y′}) = S(h, g) = S(h, id_{Y}) ; S(id_{X′′}, g). Similarly there is a unique k : Y → Y′′ such that

g = k ; y  and  u; S(f, k) = v ; S(x, id_{Y′′})

Then we have a pair of meditors from the square with vertex Z to the marked pullback, and another pair from S(X, Y), which must respectively be equal:

v = u; S(h, k)  and  (f, g) = (h, k) ; (x, y)

i.e. (h, k) is a fill-in. Conversely the components of any fill-in serve as the fill-ins h and k. □

Lemma 3.8 Let S : X ×Y → Z be a functor which is stable in each argument and has orthogonal arguments. Then S is jointly stable. Proof Let w : Z → S(X, Y) in Z; we make repeated use of the factorisation property. By stability of S(−, Y), let

w = v ; S(x, id_{Y})

where v : Z → S(X′, Y) is a candidate for S(−, Y) and x : X′ → X. Then by stability of S(X′, −), let

v = u; S(id_{X′}, y)

where u : Z → S(X′, Y′) is a candidate for S(X′, −) and y : Y′ → Y. By stability of S(−, Y′), let

u; S(x, id_{Y′}) = u′ ; S(x′, id_{Y′})

where u′ : Z → S(X′′, Y′) is a candidate for S(−, Y′) and x′ : X′′ → X. Now put

v′ = u′ ; S(id_{X′′}, y)

By corollary 3.1.5 this is a candidate for S(−, Y), and

w = v′ ; S(x′, id_{Y})

This gives two factorisations of w, so there is a unique h : X′ ≅ X′′ such that

x = h; x′  and  v′ = v ; S(h, id_{Y})

Finally u′ = u; S(h, id_{Y′}) is a candidate for both S(X′′, −) ≅ S(X′, −) and S(−, Y′) and hence by lemma 3.1.7 for S itself. The required factorisation is then w = u; S(x, y). □

Theorem 3.9 A functor of several (but finitely many) variables is jointly stable iff it is separately stable and has (pairwise) orthogonal arguments. □

Exercise 3.10 What additional condition is needed for stability of infinitary functors? □

3.2 The Trace-Diagonal of a Cartesian Transformation

By lemmas 3.1.4&6, a natural transformation is cartesian iff postcomposition with it preserves candidacy. In the poset case, as we saw with qualitative domains in lemma 2.3.4, this makes the trace of the smaller function simply a subset of that of the larger, so viewing the trace of a stable function representing a computational process as a set of “input-output patterns”, the Berry order is precisely the inclusion of such sets. It is unfortunate that it is not obvious that these two naturally defined orders are the same: our general proof looks like just a technical corollary, and Berry [B79] in fact made two separate definitions which he only claimed to be equivalent in the special case of dI-domains.

This notion of “inclusion” between traces is one which we have in fact already formulated as a diagonal for arbitrary natural transformations (i.e. the pointwise order). In that context it appears to be rather complicated, requiring a 2-cell α̃ (or alternatively α, its adjoint transpose under C ⊣ H). However when the natural transformation ϕ is cartesian, we find that α is invertible:

T_{0}
[figure: C_{0}; F_{0}]
X ≅^{α}  ≅^{ω} Y
[figure: C; F]
T^{Φ}

and this is the sense in which there is an “inclusion” of traces. Most of this section is concerned with the very strong properties of this “inclusion”.

Lemma 3.11 If ϕ is cartesian and the trace is standard then there is a standard diagonal

Φ(X, Y, u′) = (X, Y, u′ ; ϕ_{X})  and  Φ(x, y) = (x, y)

for which α_{T′} = id_{X} and ω_{T′} = id_{Y}. Moreover Φ is a discrete isotomy. Proof Verify using Proposition 1.7.3 that this is a diagonal corresponding to ϕ. Manifestly Φ is faithful and reflects identities, so by Lemma 2.2.2 it creates equalisers. □

Exercise 3.12 Show both directly and using this lemma that if ϕ : S′ → S is cartesian and S preserves equalisers then so does S′. □

This is quite typical of what we shall find: “a subfunction of a good functor is good”. The functor Φ is full (as well as faithful) iff ϕ is mono, in which case we are more justified in calling it an inclusion.

Proposition 3.13 Suppose the natural transformation ϕ : S′ → S has diagonal (Φ, α̃, ω). Then ϕ is cartesian iff α is invertible. Moreover if the traces are standard, we may then take α and ω to be identities. Proof By corollary 1.7.6 there is a standard diagonal Φ_{s} : T → T_{0} where T_{0} is the standard trace of S. This has identity 2-cells and Φ_{s}Φ : T′ → T_{0} has the same 2-cells as Φ. Corollary 1.7.6 also provides a standard diagonal Φ′_{s} : T′ → T′_{0}.

[⇒] Let Φ_{0} : T′_{0} → T_{0} be the standard diagonal and Φ_{00} = Φ_{0}Φ′_{s} : T′ → T_{0}, which has identity 2cells. Since Φ and Φ_{00} correspond to the same cartesian transformation, they are isomorphic, and in fact α itself is the isomorphism.

[⇐] Suppose we are given u′ : Y′ → S′X′ which is a candidate; then (X′, Y′, u′) ∈ T′_{0}. Since Φ′_{s} is essentially surjective, there is some T′ ∈ T′ such that ⟨x, y⟩ : Φ′_{s}T′ ≅ (X′, Y′, u′) ∈ T′_{0}. Then ΦT′ = T = (X, Y, u) ∈ T where α_{T′} : X ≅ C′T′, ω_{T′} : Y ≅ F′T′. Then the following square commutes, in which the vertical maps are isomorphisms:

Y  \overline{u} SX

[figure: F′T′; ω_{T′} ≅; F′η;_{T′}; S′C′T′; ϕ_{C′T′}; SC′T′; Sα_{T′} ≅]

[figure: Y′; y ≅; u′; S′X′; S′x ≅; ϕ_{X′}; SX′; Sx ≅]

Since by definition u is a candidate, so is u′;ϕ_{X′}, and hence by Lemma 3.1.6 ϕ is cartesian. □

In terms of the spectrum, for each Y ∈ Y, ϕ induces (by postcomposition) a faithful functor

Spec_{ϕ}(Y) : Spec_{S′}(Y) ⟶ Spec_{S}(Y)

It is instructive to consider the discrete case, so that Spec_{S}(Y) is just an equivalence relation. Then Spec_{S′}(Y) defines a sparser relation: it is a partial equivalence relation because there are fewer objects involved, but unless ϕ is mono it also makes fewer identifications between objects. The induced function between the quotient sets is then an arbitrary function, being mono if and only if ϕ is. It is nevertheless useful to think of S′ as a subfunction of S for any cartesian ϕ : S′ → S, because it is defined by a subtheory.

Exercise 3.14 Suppose that ψ is cartesian. Show that ϕ; ψ is cartesian iff ϕ is. □

Lemma 3.15 Φ is full (as well as faithful) iff ϕ is mono. Proof [⇒] Suppose w_{1} ; ϕ_{X} = w_{2} ; ϕ_{X}, in which we may put w_{1} = u′_{1} ; S′x_{1} and w_{2} = u′_{2} ; S′x_{2}. Then

u_{1} ; Sx_{1} = u′_{1} ; ϕ_{X′_{1}} ; Sx_{1} = u′_{1} ; S′x_{1} ; ϕ_{X} = u′_{2} ; S′x_{2} ; ϕ_{X} = u′_{2} ; ϕ_{X′_{2}} ; Sx_{2} = u_{2} ; Sx_{2}

by naturality of ϕ, and so by diagonal universality of u_{1} and u_{2} there is a unique h : X′_{1} ≅ X′_{2} such that

u_{2} = u_{1} ; Sh  and  x_{2} = h^{−1} ; x_{1}

The first equation makes ⟨h, id⟩ : Φ⟨X_{1}, Y, u′_{1}⟩ → Φ⟨X_{2}, Y, u′_{2}⟩ a morphism, and so by hypothesis ⟨h, id⟩ : ⟨X_{1}, Y, u′_{1}⟩ → ⟨X_{2}, Y, u′_{2}⟩ is also, i.e. u′_{2} = u′_{1} ; S′h. But then

w_{2} = u′_{2} ; S′x_{2} = u′_{1} ; S′h; S′(h^{−1}⟨;x_{1}) = u′_{1} ; S′x_{1} = w_{1}

as required.

[⇐] Let ⟨x, y⟩ : Φ⟨X_{1}, Y, u′_{1}⟩ → Φ⟨X_{2}, Y, u′_{2}⟩ be a morphism. Then the square on the left commutes and that on the right is a pullback:

Y_{1}

[figure: y ; u′_{2}; ..............; u_{1}]

S′X_{1} \overline{\begin{matrix}ϕ_{X_{1}} \\  \end{matrix}}SX_{1}

[figure: S′X_{2}; S′x; ϕ_{X_{2}}; SX_{2}; Sx]

Let v : Y_{1} → S′X_{1} be the mediator. But then v ; ϕ_{X_{1}} = u_{1} = u′_{1} ; ϕ_{X_{1}} and ϕ_{X_{1}} is mono, so v = u′_{1}. Hence also u′_{1} ; S′x = y ; u′_{2}, i.e. ⟨x, y⟩ : ⟨X_{1}, Y, u′_{1}⟩ → ⟨X_{2}, Y, u′_{2}⟩ is a morphism. □

3.3 Subfunctions of the Identity

Pencil and paper calculation with “Hasse diagrams” may suggest that it is more difficult to compute the stable function-space of a domain than the pointwise version. However stable domains, as we shall see, are characterised by the complexity of their slices and of their polycolimits, and although (at the moment) it seems not an easy matter to find the latter, the slice of a functionspace by an arbitrary stable functor is the same as that of its trace by the identity. This is a property not shared by the pointwise function-space.

Fixing a particular stable functor S_{0} : X → Y, we may use the correspondence between diagonals and cartesian transformations to investigate the slice [X → Y]/S_{0} of the (possibly rather large^{1}) category of stable functors from X to Y and cartesian transformations between them. First we need an intrinsic characterisation of the functors which may arise as diagonals (so far we know that they are discrete isotomies). We shall start by looking at the case of the identity, and since we want an answer up to equivalence it doesn’t matter if we take a nonstandard trace (cf. Exercise 1.5.9).

Lemma 3.16 Let M : T_{0} → T_{0} be stable and κ : M → id be cartesian. Then the comparison and isotomy parts of any trace factorisation of M, and any diagonal corresponding to κ are isomorphic functors. In particular each of them is both a comparison and an isotomy.

1As we shall only be demonstrating equivalences between this and other similar categories, and not manipulating it as a category of the same kind as X and Y themselves, we shall disregard size questions in this paper. In fact there are genuine difficulties of size in proving that the evaluation functor is stable, to solve which we need to restrict stable categories to be locally presentable. This being a substantial piece of work in itself, we defer it to another paper [T91].

Proof In the diagram on the right,

[figure: T_{0}; C_{0}; F_{0}; X  Y; C; F; T; Φ; T_{0}; id; id; T_{0}  T_{0}; Φ; Φ; T; Φ]

the two triangles commute up to isomorphism. □

Conversely, given a comparison and an isotomy (C_{0}, F_{0}) : T_{0} → X × Y and a functor Φ which is both a comparison and an isotomy, by composition we may form the pair with C = C_{0}Φ and F = F_{0}Φ as on the left. In other words,

Lemma 3.17 Let S_{0} : X → Y be a stable functor with trace T_{0} and Φ : T → T_{0} be an isotomy which has a right adjoint. Then there is a stable functor S : X → Y with trace T , and a cartesian transformation ϕ : S → S_{0} whose diagonal is Φ. □

Since diagonals are isotomies, we shall have [X → Y]/S_{0} ≃ [T_{0} → T_{0}]/id if we can show that any diagonal which corresponds to a cartesian transformation has a (continuous) right adjoint. To construct this we need pullbacks, as we can see from another important special case. Put X = 1, so that (stable) functors X → Y are simply objects and (cartesian) transformations are morphisms of Y.

Exercise 3.18 Show that the standard trace of a stable functor from a singleton with value Y ∈ Y is the slice Y/Y and that the standard diagonal corresponding to y : Y′ → Y is the “forgetful” functor y_{!} : Y/Y′ → Y/Y given by postcomposition with y. Observe that this is, by definition, an isotomy. □

Lemma 3.19 y_{!} has a right adjoint (called y^{∗}) for every y : Y′ → Y in Y iff Y has pullbacks.

Y/Y′  ⇆ Y/Y
(W →^{w} Y′)  ↦ (W ⟶^{w;y} Y) = y_{!}W
y^{∗}V = (V ×_{Y} Y′ →^{π_{0}} Y′) ← (V →^{v} Y)

The unit, ι_{W} = ⟨id, w⟩ : W → W ×_{Y} Y′, and counit, κ_{V} = π_{0} : V ×_{Y} Y′ → V, are both cartesian. □ For the continuous case, we shall need the

Definition 3.20 A category Y is pullback-continuous if the functor y^{∗} (exists and) is continuous for each morphism y : Y′ → Y of Y. Observe that if F : T → Y is an isotomy and Y is pullback-continuous then so is T .

This generalises meet-continuity in lattices, but it is misleading to say that “pullbacks are continuous” (as we can say that “meet is continuous” in the poset case), since the notion of pullback is contravariant in one of its three arguments. There is a way of stating this idea, but it requires stronger hypotheses, in particular that pullbacks also preserve coequalisers (cf. warning 1.3.5). The use of this definition is illustrated by the important

Lemma 3.21 Any subfunction of a continuous functor into a pullback-continuous category is continuous. Proof Let S : X → Y be continuous, Y pullback-continuous and ϕ : S′ → S cartesian. Suppose X = colim^{↑} X_{i} in X with colimiting cocone x_{i} : X_{i} → X. Then in the pullback square

[figure: S′X_{i}; S′x_{i}; S′X; SX_{i}; ϕ_{X_{i}}; Sx_{i}; SX; ϕ_{X}]

the lower side is a typical map in a colimiting cocone, and hence so is its image ϕ_{X}^{∗}(Sx_{i}) = S′x_{i}. □

To justify our comment that this idea does not work in the pointwise version, recall that we are interested in diagonals which share the properties of both forgetful functors out of the trace.

Exercise 3.22 Show that for the Scott trace (exercise 1.7.7) the diagonal Φ : Y ↓S′ → Y ↓S given by (w′ : Y → S′X) ↦ (w′ ; ϕ_{X}) for any natural transformation ϕ : S′ → S has a right adjoint Θ given by pullback along ϕ_{X}. However, Φ is a fibration iff ϕ is cartesian.

Continuity of Θ in this case also requires pullbacks to be continuous in the stronger sense which we have mentioned.

3.4 Rigid Adjunction between Traces

We shall now show that the (standard) diagonal Φ : T′ → T corresponding to a cartesian transformation ϕ : S′ → S has a (continuous) right adjoint Θ for which the unit ι : id → ΘΦ and counit κ : ΦΘ → id are cartesian.

Lemma 3.23 There is a functor Θ : T → T′ and a natural transformation κ : ΦΘ → id such that

[figure: F ΦΘT; F′η′_{ΘT}; S′C′ΘT; S′Cκ_{T}; S′CT; F T; F κ_{T}; F η_{T}; SCT; ϕ_{CT}]

is a pullback. Θ is unique up to isomorphism. Proof Let T = (X, Y, u) ∈ T , so CT = X, F T = Y and F η_{T} = u. Form the pullback

[figure: Y′; w′; S′X′; S′x; S′X; Y; y; u; SX; ϕ_{X}]

in Y, factorising the top map through a candidate w′. Put ΘT = (X′, Y′, w′), so w′ = F′η′_{ΘT}. Also w = w′ ; ϕ_{X′} : Y′ → SX′ is a candidate for S, and so ΦΘT = (X′, Y′, w). Finally put κ_{T} = (x, y), with x = Cκ_{T} and y = F κ_{T}; this is a morphism because

w; Sx = w′ ; ϕ_{X′} ; Sx  definition of w
= w′ ; S′x; ϕ_{X}  naturality pf ϕ
= y ; u  above rectangle

When we substitute in the pullback defining Y′ we get the required diagram. Functoriality and uniqueness of Θ and naturality of κ follow from the general properties of pullbacks and candidates.

□

As with Lemma 1.6.1, we have to make an arbitrary choice of ΘT and κ_{T} (from the isomorphism class) for each T. Can we make this choice so that H′ = ΘH?

Lemma 3.24 κ is cartesian. Proof For any t : T_{1} → T_{2}, we obtain the square on the left:

[figure: F ΦΘT_{1}; F ΦΘt; F ΦΘT_{2}; F T_{1}; F κ_{T_{1}}; F t; F T_{2}; F κ_{T_{2}}; S′CT_{1}; S′Ct; S′CT_{2}; SCT_{1}; ϕ_{CT_{1}}; SCt; SCT_{2}; ϕ_{CT_{2}}]

by pullback of the one on the right along F η_{T_{2}} : F T_{2} → SCT_{2}, and F creates pullbacks. □

Proposition 3.25 If S is continuous and Y is pullback-continuous then Θ is continuous. Proof Let T = colim^{↑} T_{i} in T , where T = (X, Y, u), T_{i} = (X_{i}, Y_{i}, u_{i}) and the colimiting cocone is (f_{i}, v_{i}). Then

[figure: Y′_{i}; u′_{i}; S′X′_{i}; S′x_{i}; S′X_{i}; S′f_{i}; S′X; Y_{i}; y_{i}; u_{i}; SX_{i}; ϕ_{X_{i}}; Sf_{i}; SX; ϕ_{X}]

is a pullback. The bottom and top composites are typical vertices of filtered diagrams in Y/SX and Y/S′X respectively, and the functor ϕ_{X}^{∗} (which is, by hypothesis, continuous) takes the first to the second. Now the triangle on the left below belongs to the colimiting cocone for the first diagram,

[figure: Y_{i}; v_{i}; Y; u_{i} ; Sf_{i}; u; SX; Y′_{i}; v′_{i}; Y′; S′X′_{i}; u′_{i}; S′f′_{i}; S′X′; u; S′(x′_{i} ; f_{i}); S′x; S′X]

and hence its image, the diagram on the right, belongs to a colimiting cocone for the second diagram. It follows immediately that Y′ = colim^{↑} Y′_{i}, and (since S′ is continuous by Lemma 3.3.6) we also have T′ = colim^{↑} T′_{i}. □

Everything hinges on the following lemma (cf. 1.6.3), which took six weeks of diagram chasing to identify and prove!

Lemma 3.26 For T′ = (X, Y, u′) ∈ T′ there is a unique map ι_{T′} : T′ → ΘΦT′ such that Φι_{T′} ; κ_{ΦT′} = id.

Proof Put u = u′ ; ϕ_{X}, so ΦT′ = (X, Y, u). Then ΘΦT′ = (X′, Y′, w′) and κ_{ΦT′} = (x, y) in the pullback

[figure: Y′; w′; S′X′; S′x; S′X]

.................................. u′

[figure: Y; j; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; y; u′; S′X; ϕ_{X}; SX; ϕ_{X}]

Now there is a diagonal map u′ : Y → S′X making the lower triangle commute, and hence a unique j : Y → Y′ such that

j ; y  = id_{Y}  (1)
j ; w′ ; S′x = u′  (2)

From the second equation the square

Y  \overline{u′} S′X

.............. S′l

[figure: S′X′; j ; w′; S′x; S′X; id]

commutes, in which u′ is a candidate for S′, and so there is a unique l : X → X′ such that

l; x  = id_{X}  (3)
u′ ; S′l = j ; w′  (4)

Putting ι_{T′} = (l, j) : T′ → ΘΦT′ we obtain

Φι_{T′} ; κ_{ΦT′} = (l; j) ; (x, y) = (id_{X}, id_{Y})

from (1) and (3) as required. The last equation (4) states that ι_{T′} is a morphism. Conversely, any morphism satisfying the required equation has components l and j satisfying (1), (3) and (4), from which (2) also follows. □

Lemma 3.27 ι is a cartesian transformation. Proof Let t′ : T′_{1} → T′_{2}. Consider the mediator from the square to the pullback (κ is cartesian):

ΦT′_{1}

[figure: Φ(t′ ; ι_{T′_{2}}); ..............; id]

ΦΘΦT′_{1} \begin{matrix}κ_{ΦT′_{1}} \\  \end{matrix}ΦT′_{1}

[figure: ΦΘΦT′_{2}; ΦΘΦt′; κ_{ΦT′_{2}}; ΦT′_{2}; Φt′]

By lifting the triangle corresponding to the left hand side, this mediator must be of the form Φf for some unique f : T′_{1} → ΘΦT′_{1} such that

f ; ΘΦt′ = t′ ; ι_{T′_{2}}  and  Φf ; κ_{ΦT′_{1}} = id

But the second equation alone already has a unique solution, namely f = ι_{T′_{1}}, and so this must satisfy the first equation as well, making ι natural. Now the two squares

[figure: ΦT′_{1}; ⊂; Φι_{T′_{1}}; ΦΘΦT′_{1}; κ_{ΦT′_{1}}; ΦT′_{1}]

[figure: ΦT′_{2}; Φt′; ⊂; Φι_{T′_{2}}; ΦΘΦT′_{2}; ΦΘΦt′; κ_{ΦT′_{2}}; ΦT′_{2}; Φt′]

commute, and the rectangle is a pullback because the top and bottom composites are identities. Hence the square on the left is also a pullback, and Φ creates pullbacks. □

Lemma 3.28 ι_{ΘT} ; Θκ_{T} = id Proof Using the same technique again, the mediator for

ΦΘT

[figure: id; ..............; id]

ΦΘΦΘT \overline{\begin{matrix}κ_{ΦΘT} \\  \end{matrix}}ΦΘT

[figure: ΦΘT; ΦΘκ_{T}; κ_{T}; T; κ_{T}]

is Φf for the unique f : ΘT → ΘΦΘT such that

f ; Θκ_{T} = id  and  Φf ; κ_{ΦΘT} = id

So f = ι_{ΘT} and the result follows. □

Theorem 3.29 Any diagonal corresponding to a cartesian transformation between stable functors into a category with pullbacks has a right adjoint for which the unit and counit are also cartesian. If the codomain category is pullback-continuous and the functors are continuous then so is the right adjoint. □

Lemma 3.30 The three triangles of functors commute up to isomorphism, the isomorphisms being related by the fourth triangle:

[figure: T_{0}; C_{0}; F_{0}; X ≅^{α}  ≅^{ω} Y; C; F; T; Φ; T_{0}; H_{0}; X ≅^{β}; H; T; Θ; F_{0}ΦΘH_{0}; ω · β ; ≅; S = F H; F_{0}κH_{0}; ϕ; F_{0}H_{0} = S_{0}]

Although the standard diagonal makes α and ω identities, it may not be possible to choose Θ in such a way that β : ΘH_{0} → H is also an identity. □

Exercise 3.31 Show that each component of ι is split mono, and invertible iff ϕ is mono. □

3.5 Stable Comonads

In this subsection we shall take a closer look at subfunctions of the identity, which we shall write as κ : M → id_{T_{0}} to distinguish this case from the general one. We have already shown that this gives rise to an adjunction Φ ⊣ Θ, and the data (M, κ) form part of what we can see of this adjunction “from one end”. We may also detect ν = Φι_{Θ}, and the triple (M, κ, ν) is called a comonad. Given a (co)monad, we may ask whether we can recover the “other end” of the adjunction. In general this is not possible, there being a “least” (Kleisli) and a “greatest” (Eilenberg-Moore) candidate for it: see [ML] chapter VI or [BW] chapter III. However in the case of rigid adjunctions we find that (M, κ) suffices.

Immediately from Exercise 3.2.2 and Lemma 3.3.6 we have the

Lemma 3.32 M preserves equalisers and, if T_{0} is pullback-continuous, filtered colimits. □

Lemma 3.33 u : Y → MX is a candidate iff u = i ; α for some isomorphism i : Y ≅ X and α : X → MX with α; κ_{X} = id_{X}. Proof By Lemma 3.1.4, u is a candidate for M iff i = u; κ_{X} is for id, and this happens iff i is invertible. □

Definition 3.34 Let M : T_{0} → T_{0} be stable and κ : M → id cartesian. A coalgebra for (M, κ) is an object X ∈ T_{0} together with a morphism (“structure map”) α : X → MX such that α;κ_{X} = id. A coalgebra homomorphism from (X, α) to (Y, β) is a map f : X → Y in T_{0} such that f; β = α; Mf.

[figure: MX; α; κ_{X}; X; id; X; X; α; MX; Y; f; β; MY; Mf]

Write Coalg(M, κ) for the category of coalgebras and homomorphisms.

Proposition 3.35 Coalg(M, κ) is equivalent to the trace, T , of M (more precisely, the forgetful functor is equivalent to the isotomy part). Proof The lemma shows that there is a “forgetful” functor Coalg(M, κ) → trace(M) which is faithful and essentially surjective. To show that it is also full, suppose that the left-hand square

[figure: X; α; MX; κ_{X}; X; Y; f; β; MY; Mg; κ_{Y}; Y; g]

commutes, where α and β are coalgebras. Then the whole diagram commutes and the top and bottom are identities, so f = g. □

Corollary 3.36 The square defining a coalgebra homomorphism is a pullback. Proof Since the above diagram is trivially a pullback and κ is cartesian, the left-hand square, which defines the homomorphism f, is also a pullback. □

Observe that whereas the standard trace includes all possible isomorphisms, the category of coalgebras excludes them. As in Exercise 1.5.9, the equivalence has two canonical pseudo-inverses.

By “looking at the adjunction from one end” is usually meant that as well as the counit κ : ΦΘ → id we also extract what we can from the unit ι, namely the comultiplication ν = Φι_{Θ}. However we find that this is redundant:

Proposition 3.37 There is a unique (cartesian) transformation ν : M → M^{2} such that (M, κ, ν) is a comonad, and every coalgebra for (M, κ) is a coalgebra for the comonad (i.e. if α;κ_{X} = id then α; Mα = α; ν_{X}). Moreover every morphism over id is a comonad homomorphism (i.e. κ′ = ϕ; κ then ν′ ; (ϕ · ϕ) = ϕ; ν where (M′, κ′, ν′) is a comonad.) Proof Abstractly, ν mediates (essentially) the diagrams of lemma 3.4.6; then by considering other pullbacks it may be shown to be natural and coassociative. More concretely, the forgetful functor Φ : Coalg(M, κ) → X is a rigid comparison and so comes with a comultiplication; then every object of Coalg(M, κ) gives rise to (is) a coalgebra for the monad. For the last part, ν′;(ϕ·ϕ) and ϕ; ν both mediate between ϕ; κ = ϕ; κ and the pullback. □

Corollary 3.38 Every rigid adjunction is comonadic. Proof If Φ ⊣ Θ is a rigid adjunction with counit κ : ΦΘ → id then the composition ΦΘ is a trace factorisation and hence unique up to equivalence. We have shown that the category of coalgebras affords such a factorisation and so is equivalent to the given adjunction. □

Question 3.39 Is every adjunction (the coKleisli category in particular) which gives rise to a stable comonad necessarily itself rigid?

Exercise 3.40 Let κ_{1}, κ_{2} : M ⇉ id be cartesian. Then there is a unique τ : M ≅ M such that κ_{1} = τ ; κ_{2}. □

We can now prove what we asserted in section 3.3; we need a choice of pullbacks to provide a pseudoinverse.

Theorem 3.41 Let S : X → Y be stable with trace T . Then there is a weak equivalence

Copt(T ) =^{def} [T → T ]/id ≃ [X → Y]/S

Proof Let S = F H with C ⊣ H be the given trace factorisation. Given κ : M → id, we have Φ : Coalg(M, κ) → T with right adjoint Θ. By Lemma 3.3.2 there is a stable functor S′ = F ΦΘH = F MH and a cartesian transformation ϕ = F κH : S′ → S with diagonal Φ. This extends to a functor Copt(T ) → [X → Y]/S, and every cartesian transformation ϕ : S′ → S arises up to isomorphism in this way. □

Corollary 3.42 For (M, κ) ∈ Copt(T ),

Copt(T )/(M, κ) ≃ Copt(Coalg(M, κ))  □

3.6 Rigid Comparisons

The quadruple (Φ, Θ, ι, κ) is an abstract adjunction in the 2-category SCat: the notion of adjunction is defined in terms of two equations between 2-cells and is therefore meaningful in any 2-category. According to domain-theoretic tradition, it is necessary to consider adjoint pairs in order to make the function-space construction covariant and hence model type polymorphism. We have seen that in the stable case (where the same arguments apply) the use of the corresponding notion of adjunction is not just introduced ad hoc but forced upon us by the structure of the 2-category.

In section 3.2 we said that cartesian transformations give rise to an inclusion between traces, and we have now seen that that inclusion takes the form of the left adjoint of a rigid adjunction. In the cases of qualitative domains and dI-domains, this inclusion preserves atoms or primes and their coherence predicate, for which reason Girard called it a morphism (of qualitative domains).

Although there are strong grounds for regarding them as more fundamental than stable functors, we shall use the more modest term rigid comparison.

Lemma 3.43 Suppose T has and Φ : T → T_{0} preserves pullbacks, and that Φ has a right adjoint for which the unit and counit are cartesian. Then it is an isotomy. Proof Let T ∈ T and w : Y → ΦT in T_{0}, and suppose Φ ⊣ Θ with unit ι and counit κ, so Φι_{T} ; κ_{ΦT} = id. Form the pullback on the left in T :

[figure: T′; j; ΘY; T; t; ι_{T}; ΘΦT; Θw] [figure: ΦT′; Φj; ΦΘY; κ_{Y}; Y]

[figure: ΦT; Φt; Φι_{T}; ΦΘΦT; ΦΘw; κ_{ΦT}; ΦT; w]

Then the top composite on the right is a pullback of an identity and so invertible. Hence t : T′ → T is a lifting of w. Repeating this process with w = Φt′, the first square is (isomorphic and without loss of generality the same as) the one expressing cartesianness of ι, so t = t′. To lift triangles we merely mediate between such pullbacks. □

Theorem 3.44 Let Φ : T → T_{0} be a functor between categories with pullbacks. Then the following are equivalent:

(α) Φ is stable and has a right adjoint for which the unit and counit are cartesian.

(β) Φ is both a (discrete) isotomy and has a right adjoint.

(γ) For some (every) stable functor S_{0} : X → Y with trace T_{0} there is a stable functor S : X → Y with trace T and a cartesian natural transformation ϕ : S → S_{0} with diagonal Φ.

(δ) There is a stable functor M : T_{0} → T_{0} with trace T and a cartesian natural transformation κ : M → id with diagonal Φ.

(ϵ) T is equivalent to the category of coalgebras of a stable copointed endofunctor (M, κ) on T_{0}, and Φ to the forgetful functor.

(ζ) T is equivalent to the category of coalgebras of a stable comonad (M, κ, ν) on T_{0}, and Φ to

the forgetful functor. Proof [α ⇒ β] by Lemma 3.6.1, [β ⇒ γ] by Lemma 3.3.2 and [γ ⇒ α] by Theorem 3.4.7. [γ ⇒ δ ⇒ β] trivially, [δ ⟺ ϵ] by Proposition 3.5.4 and [ϵ ⟺ ζ] by Theorem 3.5.6. □

This theorem completes the justification of our claim in section 2.2.1 that (rigid) comparisons between domains behave like instances of the order relation within a domain: we have shown that a stable functor can be represented as a category (the trace) and a cartesian transformation as a (rigid comparison) functor. As we remarked about the Scott trace in section 1.7, this idea occurs in continuous domain theory (with a view to interpreting polymorphism, a variable type T [x] is interpreted as a functor which takes the order relation x′ ≤ x to a comparison T [x′] → T [x]) but it only works properly in the stable version.

Bibliography

[BW] M. Barr and C. Wells, Toposes, triples and theories, Grundlehren der Mathematischen Wissenschaften 278 (Springer, New York, 1985).

[B78] G. Berry, Stable models of typed λ-calculi, in: C. Böhm, G. Ausiello, eds., Third colloquium on automata, languages and programming (Udine, 1978), Lecture notes in computer science 62 (Springer, Berlin, 1978), 72–89.

[B79] G. Berry, Modèles Complètement Adéquats et Stables des Lambda-Calcul Typés, Thèse de Doctorat d’Etat, Université Paris VII, 1979.

[Br] R. Brown, From Groups to Groupoids: a Brief Survey, Bull. London Math. Soc. 19 (1987) 113–134.

[CGW] Th. Coquand, C.A. Gunter and G. Winskel, DI-domains as a model of polymorphism, University of Cambridge Computer Laboratory technical report 107 (1986).

[D79] Y. Diers, Some spectra relative to functors, J. Pure Appl. Algebra 22 (1979) 57–74.

[D80] Y. Diers, Catégories localement multiprésentables, Arch. Math. 34 (1980) 344–356.

[D81] Y. Diers, Multimonads and multimonadic categories, J. Pure Appl. Algebra 17 (1980) 153–170.

[D84] Y. Diers, Une Construction Universelle des Spectres, Topologies Spectrales et Faisceaux Structuraux, Comm. Alg. 12 (1984) 2141–2183.

[GLT] J.-Y. Girard, Y. Lafont and P. Taylor, Proofs and types, (Cambridge University Press, 1989; reprinted 1990).

[GU] P. Gabriel and F. Ulmer, Lokal Präsentierbare Kategorien, Lecture notes in mathematics 221 (Springer, Berlin, 1971).

[G81] J.-Y. Girard, Π_{2}^{1} logic: part I, dilators, Ann. Math. Logic 21 (1981) 75–219.

[G85] J.-Y. Girard, The system F of variable types, fifteen years later, Theoret. Comput. Sci. 45 (1985) 159–192.

[G88] J.-Y. Girard, Normal functors, power series and λ-calculus, Ann. Pure Appl. Logic 37 (1988) 129–177.

[Jh89] P.T. Johnstone, A topos-theorist looks at dilators, J. Pure Appl. Alg. 58 (1989) 235–249.

[Jy] A. Joyal, Foncteurs analytiques et espèces de structures, in: G. Labelle, P. Leroux, eds., Combinatoire énumérative (Montréal, 1986), Lecture Notes in Mathematics 1234 (Springer, New York, 1987) 126–159.

[L88] F. Lamarche, Modelling polymorphism with categories, Ph.D. thesis, McGill University, 1988.

[L89] F. Lamarche, A simple model for the theory of constructions, in: J.W. Gray, A. Scedrov, eds., Categories in computer science and logic (Boulder, 1987), Contemporary Mathematics 92 (American Mathematical Society, Providence, RI, 1989) 207–216.

[L90] F. Lamarche, Quantitative domains and infinitary algebras, submitted to Theoretical Computer Science.

[ML] S. Mac Lane, Categories for the working mathematician, Graduate texts in mathematics 5 (Springer, New York, 1971).

[S82] D.S. Scott, Domains for denotational semantics, in: M. Nielsen, E.M. Schmidt, eds., Automata, Languages and Progamming (Aarhus, 1982), lecture notes in computer science 140 (Springer, Berlin, 1982) 577–613.

[T87] P. Taylor, Homomorphisms, bilimits and saturated domains, manuscript, 1987, 26pp.

[T88] P. Taylor, The trace factorisation and cartesian closure for stable categories, manuscript, 1988, 70pp, of which the present paper is essentially the first half.

[T89] P. Taylor, Quantitative domains, groupoids and linear logic, in: D. Pitt, ed., Category theory and computer science (Manchester, 1989), Lecture notes in computer science 389 (Springer, Berlin, 1989) 155–181.

[T90] P. Taylor, An Algebraic Approach to Stable Domains, J. Pure Appl. Algebra 64 (1990) 171–203

[T91] P. Taylor, Locally finitely poly-presentable categories, in preparation.