ALGEBRAIC STRUCTURE FOR BICATEGORY

ENRICHED CATEGORIES

R. Gordon and A.J. Power^{∗}

Abstract. We define algebraic structure on a locally finitely presentable W -category for a locally finitely presentable bicategory W with a small set of objects. We further define the W -category of algebras for given algebraic structure. Each algebraic structure gives rise to a finitary W -monad with the same W -category of algebras. Moreover, every finitary W -monad arises in this way from some algebraic structure; but that algebraic structure is not uniquely determined by the monad.

§1. Introduction

The study of data refinement in the development of programming languages gives rise to the study of categories enriched over a monoidal biclosed category, in which the monoidal structure need not possess a symmetry (see [7] and [6]). One requires an analysis of universal algebra enriched over such a monoidal category. The reasoning is as follows. Traditional universal algebra corresponds to the study of finitary monads on the category of small sets. In order to study data refinement, one studies not sets with operations and universally defined equations, but more exotic structures such as locally ordered categories with operations and universally defined equations. So one seeks precise definitions of the concepts of operations and equations, and algebras, in sufficient generality to include the above example, together with a theorem characterizing those definitions in terms of finitary monads. The theorem both validates the definitions and is explicitly used. For this approach to data refinement, the enrichment is central: it allows one to lift data refinement from a set of base types to the set of all types of a programming language (see [7] and [6]).

The natural mathematical level of generality in which to pursue such a study is in terms of W -categories, for a locally finitely presentable bicategory W with a small set of objects. This paper provides such an analysis. It is a further development of the work of [1] and [2], in which we established the basic definitions and results we require here, such as the notion of colimit in a W -category, what it means for a W -category to be locally finitely presentable, and the appropriate generalization of Gabriel-Ulmer duality.

Here, we generalize the work of [5], which amounts to a study of universal algebra with respect to enrichment over a symmetric monoidal closed category V. We define algebraic structure on a locally finitely presentable W -category, and the

Typeset by AMS-TEX

*Supported by ESPRIT Basic Research Action 6453: Types for Proofs and Programs

corresponding algebras. We then prove that any algebraic structure gives rise to a finitary W -monad with the same W -category of algebras. Finally, we show that every finitary W -monad arises in that way from some algebraic structure.

Once the definitions are established, then except for one of the main results of [1], the argument here is essentially the same as that of [5]. We require a little more delicacy here as, in general, functor W -categories do not exist, whereas functor V - categories were used freely in [5]. However, with care one can avoid them, and except for that delicacy, the generalization is largely routine.

We do not develop examples in this paper; but a detailed analysis of the leading class of examples appears in [6], with further explanation of their computational significance in [7]. Briefly, our leading class of examples is based on the category of small locally ordered categories. That category has a monoidal biclosed structure, with closed structure yielding Lax(A, B), the category of locally ordered functors and lax transformations, and coclosed structure giving the dual. That monoidal biclosed category is locally finitely presentable in the sense we define here, and one may study data refinement via universal algebra enriched in it. For further, relatively gentle discussion of enriched universal algebra, we recommend Robinson’s paper [8].

Section 2 recalls those definitions and results we need from [1] and [2]. In Section 3, we define the W -category of algebras for a W -monad and characterize both algebras and maps of algebras in terms of maps of monoids if the monad is finitary. In Section 4, we define algebraic structure on a locally finitely presentable W - category, together with its W -category of algebras, and in Section 5, we prove that algebraic structure gives rise to a finitary W -monad with the same W -category of algebras. Finally, in Section 6, we show that every finitary W -monad arises from some algebraic structure. Our notation agrees with that of [1] and [2], but we review it all here anyway. The one extra condition we need for our main results is that Ob W is small.

We would like to thank Kris Rose and Ross Moore for their XY-pic.

§2. Preliminaries

We assume throughout that W is a bicategory with the horizontal composite of x: u → v and y: v → w denoted by y ⊗ x. We say W is closed if for all x: u → v and y: u → w, there is a universal diagram

[figure: u; y; x; w; v.; x!y]

We call W coclosed if W^{op} is closed, with coclosed structure, given x: v → u and y: w → u, written as in

[figure: v; x; w; x⋔y; y; u; ;]

and we call W biclosed when W is both closed and coclosed.

Definition 2.1. A biclosed bicategory W is locally finitely presentable if for each u, v ∈ Ob W the category W (u, v) is locally finitely presentable, each identity arrow I_{u} is finitely presentable, and y ⊗ x is finitely presentable whenever x and y are finitely presentable.

We denote the locally full subbicategory of W determined by the finitely presentable arrows by W_{f}, and we use the abbreviation lfp for the term locally finitely presentable. It is routine to verify that if W is lfp, then for all finitely presentable x, x ⋔ − and x!− preserve filtered colimits.

This definition of locally finitely presentable bicategory agrees, in the case that W has one object and is symmetric, with Kelly’s definition for symmetric monoidal closed categories in [4], and we use it in [2] for the same purpose as he did, i.e., to prove Gabriel-Ulmer duality.

A W -category A consists of a set Ob A, a function e: Ob A → Ob W, for each A, B ∈ A an arrow A(A, B): eA → eB, and 2-cells j_{A}: I_{u} ⇒ A(A, A) and μ_{ABC}: A(B, C)⊗ A(A, B) ⇒ A(A, C) subject to the evident three coherence axioms. W -functors and W -natural transformations are defined similarly, giving a 2-category W-Cat.

For an object u of W, we denote by A_{u} the category determined by those A such that eA = u, and we say that A lies over u. If W is closed, we denote by W^{u} the W -category for which an object over v is an arrow from u to v, and with W^{u}(x, y) determined by closedness of W. For any W -category A and A ∈ A_{u}, there is an evident W -functor A(A, −): A → W^{u}. A W - functor is representable if it is W -naturally isomorphic to such A(A, −).

Definition 2.2. A W -category A has tensors with an arrow x: u → v in W if for any A ∈ A_{u}, the W -functor W^{u}(x, A(A, −)): A → W^{v} is representable. If W is lfp, we say A has finite tensors if it has tensors with all arrows x: u → v in W_{f}.

Cotensors in A are defined by tensors in the W^{op}-category A^{op}. We denote tensors by x ⊗ A and cotensors by x ⋔ A.

Definition 2.3. Given lfp W, a W -category A is locally finitely presentable if each A_{u} is lfp, A has finite tensors, and each x⊗−: A_{u} → A_{v} has a finitary right adjoint.

If A is lfp, then A has all tensors [1, Corollary 3.9], and the right adjoint to each x ⊗ − is x ⋔ −. A W -functor is called finitary if its restriction to each A_{u} is finitary as an ordinary functor. If we denote by A_{f} the full sub-W -category of A given by all finitely presentable objects of A_{u} for each u, we have [1, Theorem 4.5].

Theorem 2.4. For lfp A and B, the inclusion Z of A_{f} in A induces an equivalence between the category W-Cat_{f} (A, B) of finitary W -functors from A to B and W-Cat (A_{f}, B), the reverse equivalence given by left Kan extension along Z.

The definitions given here are in the form best suited to our purposes in this paper. They agree with the definitions of [1], which were best suited to our proof in [1] of Theorem 2.4 above. Those definitions were further explored in [2], in which we gave two characterizations of locally finitely presentable W -categories. We first gave an intrinsic definition of a cocomplete W -category, defined strong generator and finitely presentable object directly in terms of A rather than A_{u}, then showed that a W -category is locally finitely presentable in the above sense if and only if it is cocomplete and has a strong generator of locally finitely presentable objects. Second, and more substantially, we characterized locally finitely presentable W - categories as W -categories of models of finite limit theories.

§ 3. finitary monads and their algebras

Assume now and for the rest of the paper that W is locally finitely presentable and Ob W is small.

By Theorem 2.4, for lfp A, the ordinary category W-Cat_{f} (A, A) is equivalent to W-Cat (A_{f}, A). For any small W -category D, W-Cat (D, A) is lfp: it has colimits given pointwise; and it follows from the Yoneda lemma for W -categories that the family of W -functors D(D, −) ⊗ A for finitely presentable A ∈ A_{u} and all D ∈ D_{u} for all u, forms a strong generator of finitely presentable objects. So W-Cat_{f} (A, A) is lfp. Colimits in W-Cat_{f} (A, A) are given pointwise, so for any finitary R: A → A,

W-Cat_{f}(R, 1): W-Cat_{f} (A, A) → W-Cat_{f} (A, A)

is cocontinuous, hence has a right adjoint. Thus W-Cat_{f} (A, A) is a monoidal closed category. Its monoids are precisely finitary W -monads on A, i.e. W -monads whose underlying W -functor is finitary; and monoid maps are precisely W -monad maps.

Let the category of monoids and monoid maps be denoted by Mnd_{f}(A).

For any cocomplete monoidal closed category C for which x ⊗ − is finitary for all x, the category of monoids in C is finitarily monadic over C: the proof of monadicity follows from the Beck condition (see [3,Theorem 23.3]), and finitariness is routine. So we may deduce

Proposition 3.1. The forgetful functor from Mnd_{f}(A) to W-Cat_{f} (A, A) is finitarily monadic.

The left adjoint L may be described as follows (see [3,Theorem 23.3]): given finitary R: A → A, let R_{0} = 1: A → A, R_{n+1} = 1 + RR_{n}, and define

ρ_{0}: R_{0} → R_{1}  ρ_{0} = inj_{1}: 1 → 1 + R
ρ_{n}: R_{n} → R_{n+1}  ρ_{n} = 1 + Rρ_{n−1}.

L(R) is the (directed) colimit of the above diagram.

Given a W -natural transformation ϕ: R → T, where (T, η_{T} , μ_{T}) is a finitary W -monad, the corresponding map of monads L(R) → T is given by the cocone

ϕ_{0}: R_{0} → T  ϕ_{0} = η_{T}: 1 → T
ϕ_{n}: R_{n+1} → T  ϕ_{n} = η_{T} + μ_{T} (ϕϕ_{n}): 1 + RR_{n} → T.

Corollary 3.2. For any lfp W -category A, the ordinary category Mnd_{f}(A) is locally finitely presentable.

Since W-Cat_{f}(A, A) is equivalent to W-Cat(A_{f}, A), the latter category inherits the monoidal structure of the former. Moreover, the equivalence lifts to an equivalence between Mnd_{f}(A) and Monoids W-Cat(A_{f}, A), where the latter is the category of monoids in W-Cat(A_{f}, A).

Proposition 3.3. For each u ∈ W and A ∈ A_{u}, the composite

W-Cat(A_{f}, A) ⟶^{Z^{∗}} W-Cat_{f}(A, A) ⟶^{ev_{A}} A_{u}

has a right adjoint, where Z is inclusion of A_{f} in A and Z^{∗} denotes left Kan extension along Z.

Proof. Z^{∗} is an equivalence. Since colimits in W-Cat_{f} (A, A) are calculated pointwise, evaluation, ev_{A}, at A must be cocontinuous. So, since W-Cat (A_{f}, A) is lfp, ev_{A} has a right adjoint (see [4,Theorem7.8]).

□

The right adjoint {A, −} is given by {A, B} = A(−, A) ⋔ B and the family {A, −}_{A∈A_{u}} may be made functorial in A uniquely such that the A -indexed family of isomorphisms A_{u} (Z^{∗}(S)A, B) ≅ W-Cat(A_{f}, A) (S, {A, B}) is natural in A.

Since W-Cat is a finitely complete 2-category, for any W -monad T in it, there is a W -category of algebras.

Definition 3.4. Given a W -monad T on A, T-Alg is the following W -category: an object of T-Alg over u is a T_{u}-algebra; given T -algebras (A, a) and (B, b), we define T-Alg ((A, a), (B, b)) to be the equalizer of

[figure: A(A, B); T; A(a,B); A(T A, B); A(T A, T B); A(T A,b)] (3.1)

Composition is induced by that of A.

It is routine to verify (cf. [3])

Proposition 3.5. For any A ∈ A, the adjunction ev_{A} ∘ Z^{∗} ⊣ {A, −} induces a monoid structure on {A, A}; for any finitary W -monad T on A, the adjunction further yields a bijection natural in T between monoid maps α: T Z → {A, A} and T -actions a: T A → A.

Proposition 3.6. Given an arrow f: A → B in A_{u}, define [f, f] to be the pullback

[figure: [f, f]; π_{1}; π_{0}; {A, A}; {A,f}; {B, B}; {f,B}; {A, B}]

in W-Cat(A_{f}, A).

Then, [f, f] lifts uniquely to a monoid in W-Cat(A_{f}, A) such that π_{0} and π_{1} become monoid maps. Moreover, if (A, a) and (B, b) are T -algebras, then f is a map of algebras if and only if, in Monoids W-Cat(A_{f}, A), the map

( \begin{matrix}α \\ β \end{matrix} ): T Z → \{A, A\} × \{B, B\}

factors (uniquely) through [f, f].

§4. algebraic structure

In this section we define algebraic structure on an lfp W -category. This generalizes the usual definition for universal algebra, which amounts to the case in which W is the one object lfp bicategory determined by Set, and our lfp W -category is also Set. An analysis for one object symmetric W appears in [5]; the definitions here are similar.

For an idea of how to think about our definition of algebraic structure, consider the case of W being Set and the W -category being Set. An instance of algebraic structure is that for groups. A group consists of a set X together with functions from Set(2, X) to Set(1, X), from Set(1, X) to Set(1, X), and from Set(0, X) to Set(1, X), subject to universally defined equations for associativity and left and right unit and inverse laws. So, in the notation of the next definition, we would put S(n) = 1 if n = 0, 1, or 2, and 0 otherwise. The equations hold on derived operations, so we will not express them here. An S-algebra (see Definition 4.2) is precisely a set X together with the three above-mentioned functions, and an (S, E)- algebra (see Definition 4.3) is a group. The category (S,E)-Alg (see Definition 4.4) is the category of groups.

Definition 4.1. Given an lfp W -category A, algebraic structure on A consists of the following:

(1) a W -functor S: | A_{f} | → A, where | A_{f} | is the discrete W -category on Ob (A_{f}). From S, we construct F (S): A_{f} → A as follows: set

S_{0} = Z, the inclusion of A_{f} in A

S_{n+1} = Z + ∑_{d∈| A_{f} |} A (d, S_{n}−) ⊗ Sd

and define σ_{0}: S_{0} → S_{1} and σ_{n}: S_{n} → S_{n+1} by

inj_{1}: Z → Z + ∑_{d∈| A_{f} |} A (d, S_{0}−) ⊗ Sd

and

Z + ∑_{d∈| A_{f} |} A (d, σ_{n−1}−) ⊗ Sd: S_{n} → S_{n+1}

respectively.

F (S) = colim_{n<ω} S_{n}.

(2) a W -functor E: | A_{f} | → A together with W -natural transformations τ_{1}, τ_{2}: E → F (S)J, where J: | A_{f} | → A_{f} is the inclusion.

We denote this algebraic structure by (S, E), generally suppressing τ_{1} and τ_{2}. Informally, for each c in | A_{f} |, Sc may be regarded as the object of basic oper-

ations of arity c, and F (S)c may be regarded as the object of derived operations of arity c. The σ_{n}’s are typically monomorphisms, so F (S) is typically the union of (S_{n})_{n<ω}. The functor E, together with τ_{1} and τ_{2}, represents the equations that must hold between derived operations. A series of detailed examples illustrating this appears in [6].

Definition 4.2. Given S: | A_{f} | → A, an S-algebra is an object A together with a 2-cell ν_{c}: A(c, A) ⇒ A(Sc, A) for each c, or equivalently, a map ν: ∑_{c∈| A_{f} |} A(c, A) ⊗

Sc → A in A.

An S- algebra extends canonically to an F (S)J-algebra (A, ν̄) as follows: define

ν_{0}: ∑_{c∈| A_{f} |} A (c, A) ⊗ S_{0}c → A by evaluation, and ν_{n+1}: ∑_{c∈| A_{f} |} A (c, A) ⊗ S_{n+1}c → A

inductively by evaluation on the first component of S_{n+1}c, and for the d-component, by

A (c, A)⊗A (d, S_{n}c)⊗Sd ⟶^{(ν_{n})_{c}⊗1} A (S_{n}c, A)⊗A (d, S_{n}c)⊗Sd → A (d, A)⊗Sd ⟶^{ν_{d}} A.

Since colimits in W-Cat (A_{f}, A) are given pointwise, we thus obtain an F (S)Jalgebra structure on A.

Definition 4.3. Given algebraic structure (S, E), an (S, E)-algebra is an S-algebra (A, ν) such that both legs of

[figure: A (c, A); ν̄_{c}; A (F (S)c, A); A(τ_{1},A); A(τ_{2},A); A (Ec, A)]

are equal for every c.

Definition 4.4. Given (S, E)-algebras (A, ν) and (B, δ), define (S,E)-Alg by letting

(S,E)-Alg ((A, ν), (B, δ)) be the equalizer of

[figure: A(A, B); {A(Sc,−)}_{c∈| A_{f} |}; {A(c,−)}_{c∈| A_{f} |}; ∏_{c} A(c, A)! A(c, B); ∏_{c} A(c,A)!δ_{c}; ∏_{c} A(Sc, A)! A(Sc, B); ∏_{c}ν_{c}! A(Sc,B); ∏_{c} A(c, A)! A(Sc, B).] (4.1)

(S,E)-Alg is then a W -category, with composition and identities induced by those of A.

An arrow in (S,E)-Alg_{u} is given by an arrow f: A → B in A_{u} such that for all c, fν_{c}(−) = δ_{c}(f−): A(c, A) ⇒ A(Sc, B), i.e. an arrow in A_{u} that commutes with all basic c-ary operations for all c.

§5. from algebraic structure to a finitary monad

In this section we give a construction that assigns a finitary monad T_{(S,E)} to algebraic structure (S, E). This is done by showing that our construction F (S) corresponds to the free finitary monad on S, then defining T_{(S,E)} by the coequalizer in Mnd_{f}(A) determined by τ_{1}, τ_{2}: E → F (S). This induces an isomorphism between the category of T_{(S,E)}-algebras and that of (S, E)-algebras.

Proposition 5.1. The forgetful functor

U: Monoids W-Cat(A_{f}, A) → W-Cat(| A_{f} |, A)

has left adjoint with object part given by F.

Proof. The functor U is a composite of four functors, each having a left adjoint that we can describe easily. By Theorem 2.4, W-Cat (A_{f}, A) is equivalent to W-Cat_{f} (A, A). So Monoids W-Cat (A_{f}, A) is equivalent to Mnd_{f}(A), since the monoidal structure on W-Cat (A_{f}, A) was defined (in Section 3) to force that equivalence. By Proposition 3.1, the forgetful functor from Mnd_{f}(A) to W-Cat_{f} (A, A) has a left adjoint L. Then, again by Theorem 2.4, composition with the inclusion Z: A_{f} → A yields W-Cat_{f} (A, A) equivalent to W-Cat (A_{f}, A). Finally, the functor from W-Cat (A_{f}, A) to W-Cat (| A_{f} |, A) given by composition with the inclusion J: | A_{f} | → A_{f} has a left adjoint given by left Kan extension. So, to describe a left adjoint to U, we need only describe the composite of these four left adjoints.

Putting them together, the left adjoint of U takes S: | A_{f} | → A to L ((ZJ)^{∗}(S)) Z: A_{f} → A. Now (ZJ)^{∗}(S) = ∑_{d∈| A_{f} |} A(d, −) ⊗ Sd, and putting R = (ZJ)^{∗}(S) after Propo-

sition 3.1, we have by induction S_{n} = R_{n}Z for all n. The result follows immediately.

□ Henceforth in this section we suppose that (S, E) is algebraic structure on A.

By Corollary 3.2, Monoids W-Cat(A_{f}, A) is cocomplete. Let T_{(S,E)} be a finitary

W -monad on A such that [figure: F (E); τ̄_{1}; τ̄_{2}; F (S); γ; T_{(S,E)}Z] is a coequalizer in

Monoids W-Cat(A_{f}, A), where τ̄_{1} and τ̄_{2} correspond to τ_{1} and τ_{2} respectively.

Lemma 5.2. Composition with γ induces a bijection between the set of T_{(S,E)}- algebras and that of (S, E)-algebras.

Proof. It follows from our explicit description of {A, −} that to give an S-algebra is to give an object A and a W -natural transformation ν: S → U{A, A}: | A_{f} | → A, or equivalently a monoid morphism ν̄: F (S) → {A, A}.

By induction it follows that the maps ϕ_{n}: R_{n} → T after Proposition 3.1 agree with those after Definition 4.2, in the case that R = (ZJ)^{∗}(S) and T = {A, A}. So, an (S, E)-algebra is precisely a W -natural transformation ν: S− → U{A, A}: | A_{f} | → A such that both legs of

[figure: E; τ_{1}; τ_{2}; F (S)J; ν̄; {A, A}]

are equal, where ν̄ corresponds to ν under the adjunction F ⊣ U. Hence, by definition of T_{(S,E)}, an (S, E)-algebra is precisely a T_{(S,E)}-algebra, the bijection being given by composition with γ.

□

Lemma 5.3. Given (S, E)-algebras (A, ν) and (B, δ), (S,E)-Alg ((A, ν), (B, δ)) is the equalizer of

[figure: A(A, B); A(ν,B); (ZJ)^{∗}(S); A ((ZJ)^{∗}(S)A, (ZJ)^{∗}(S)B); _{A((ZJ)^{∗}(S)A,δ)}; .; A ((ZJ)^{∗}(S)A, B) .] (5.1)

Proof. Compare (4.1) and (5.1). It is immediate that the lower arrows from A(A, B) to A ((ZJ)^{∗}(S)A, B) are the same.

The upper arrow of (5.1) corresponds to

A(A, B) ⊗ (ZJ)^{∗}(S)A ⟶^{ev} (ZJ)^{∗}(S)B ⟶^{δ} B,

which, when preceded by a canonical isomorphism, is

∑_{c∈| A_{f} |} A(A, B) ⊗ A(c, A) ⊗ Sc \underrightarrow{∑(μ⊗1)} ∑_{c∈| A_{f} |} A(c, B) ⊗ Sc ⟶^{δ} B,

which corresponds to the upper arrow of (4.1).

□

Lemma 5.4. Given (S, E)-algebras (A, ν) and (B, δ) corresponding to T_{(S,E)}- algebras (A, a) and (B, b) respectively, both triangles in

[figure: A(A, B); A((ZJ)^{∗}(S)A,δ)∘(ZJ)^{∗}(S); A(ν,B); A(T A,b)∘T; A(a,B); A(T A, B); _{A(ψA,B)}; .; _{A ((ZJ)^{∗}(S)A, B)}] (5.2)

commute, where ψ is the W -natural transformation determined by γ and the unit of the adjunction between Monoids W-Cat(A_{f}, A) and W-Cat(A_{f}, A) applied to J^{∗}(S).

Proof. The bijection between T_{(S,E)}-algebras and (S, E)-algebras given in Lemma 5.2 shows that ν corresponds to

J^{∗}(S) ⟶^{ψ̄} T Z ⟶^{α} {A, A}, (5.3)

where α is the monoid map associated with (A, a) and ψ̄ corresponds to ψ. It is immediate that the lower triangle of (5.2) commutes. The upper triangle is easily checked, using (5.3) with ν replaced by δ and α replaced by β, and by naturality of ψ.

□

Theorem 5.5. Given algebraic structure (S, E), composition with γ induces an isomorphism

(S,E)-Alg ≅ T_{(S,E)}-Alg.

Proof. By Lemma 5.2, γ induces a bijection from the set of T_{(S,E)}-algebras to the set of (S, E)-algebras. By Definition 3.4 and Lemmas 5.3 and 5.4, it follows that composition with γ yields a (unique) W -functor γ^{∗}: T_{(S,E)}-Alg → (S,E)-Alg commuting with the forgetful W -functors to A. It remains to show that γ^{∗} is fully faithful. It suffices to show that for any finitely presentable x and ϕ: x → A(A, B) making the composites with the lower legs of (5.2) equal, it follows that the composites with the horizontal legs of (5.2) are equal.

First observe that x ⋔ B inherits a canonical algebra structure from (B, b) given by

T (x ⋔ B) ⟶^{π_{T,B}} x ⋔ T B ⟶^{x ⋔ b} x ⋔ B, (5.4)

where π is the evident comparison map.

Given ϕ: x → A(A, B), there corresponds a map A → x ⋔ B, which we shall also denote by ϕ, and which makes the diagram

[figure: (ZJ)^{∗}(S)A; ν; (ZJ)^{∗}(S)ϕ; (ZJ)^{∗}(S) (x ⋔ B); π_{(ZJ)^{∗}(S),B}; x ⋔(ZJ)^{∗}(S)B; x ⋔ δ; A; ϕ; x ⋔ B]

commute.

By definition of [ϕ, ϕ], there exists a unique W -natural transformation ω: J^{∗}(S) → [ϕ, ϕ] making

[figure: J^{∗}(S); ξ; ω; λ; [ϕ, ϕ]; π_{1}; π_{0}; {A, A}; {x ⋔ B, x ⋔ B}]

commute, where ξ corresponds to (5.4) composed with ψ, and λ corresponds to ν. By elementary use of adjunctions, the fact that π_{0} and π_{1} are jointly mono, and the definitions of T_{(S,E)} and γ, it follows that ω lifts to a monoid map T_{(S,E)} → [ϕ, ϕ] making the evident two triangles commute; so ϕ: A → x ⋔ B is a map of T -algebras by Proposition 3.6. Hence, the composites of ϕ: x → A(A, B) with the horizontal legs of (5.2) are equal. Hence, as remarked above, it follows that γ∗: T_{(S,E)}-Alg → (S,E)-Alg is an isomorphism.

□

§6. finitary monads as algebraic structure

In this section we show that every finitary W -monad on an lfp W -category A arises from algebraic structure. Of course, that algebraic structure is far from unique even in the case that W is the one object bicategory Set, and A = Set: for instance, there are several presentations of the monad for groups. Nevertheless, this is still a weak completeness result.

Theorem 6.1. Given a finitary W -monad on lfp A, there exists algebraic structure (S, E) on A such that (S,E)-Alg ≅ T-Alg.

Proof. By Theorem 5.5, it suffices to show that for any finitary W -monad T, there is a coequalizer in Monoids W-Cat (A_{f}, A) of the form

[figure: F (E); τ_{1}; τ_{2}; F (S); T Z.]

Observe that for any T ∈ Monoids W-Cat (A_{f}, A), if η, ϵ: F ⊣ U, then

[figure: F UF U(T); F UϵT; ϵF U(T); F U(T); ϵT; T]

is a U-split coequalizer diagram. So if we can show that U reflects the coequalizers of U-split coequalizer pairs, then (U(T), UF U(T)) provides algebraic structure as desired.

Accordingly, suppose that

[figure: P; τ_{1}; τ_{2}; Q; γ; T; (6.1)]

is any U-split coequalizer diagram in Monoids W-Cat (A_{f}, A). Since colimits in W-Cat (A_{f}, A) are given pointwise, (6.1) is a coequalizer in W-Cat (A_{f}, A). So given a monoid map ω: Q → V such that ω · τ_{1} = ω · τ_{2}, there exists a unique W -natural transformation λ: T → V such that λ · γ = ω. We must show that λ is a monoid map.

Since γ and ω preserve the unit of Q, it is immediate that λ preserves the unit of T. In order to show that λ preserves composition, it suffices to show that γ ∘ γ: Q ∘ Q → T ∘ T is epi in W-Cat (A_{f}, A), where ∘ is the monoidal structure on W-Cat (A_{f}, A). The map γ ∘ γ is given explicitly, using the equivalence Z^{∗} ⊣ W-Cat(Z, 1): W-Cat_{f}(A, A) → W-Cat (A_{f}, A) by

[figure: Z^{∗}(Q)Q; Z^{∗}(Q)γ; Z^{∗}(Q)T; (Z^{∗}γ)T; Z^{∗}(T)T.]

Since the coequalizer

[figure: UP; U_{τ_{1}}; U_{τ_{2}}; UQ; Uγ; UT]

is split, γ is a pointwise retraction. So Z^{∗}(Q)γ is a pointwise retraction: given c ∈ A_{fu}, the component of Z^{∗}(Q)γ at c is the arrow Z^{∗}(Q)γ_{c} in A_{u}. Hence Z^{∗}(Q)γ is epi. Since γ is epi in W-Cat (A_{f}, A) and Z^{∗} ⊣ W-Cat (Z, 1) is an equivalence, it follows that Z^{∗}γ is epi in W-Cat_{f} (A, A), hence pointwise epi. So (Z^{∗}γ) T is epi. Hence the composite γ ∘ γ is epi, so (6.1) is a coequalizer as required.

References

[1]. R. Gordon and A.J. Power, Enrichment Through Variation, J. Pure and Applied Algebra (to

appear). [2]. R. Gordon and A.J. Power, Gabriel-Ulmer Duality for Categories Enriched in Bicategories

(submitted). [3]. G.M. Kelly, A Unified Treatment of Transfinite Constructions for Free Algebras, Free Monoids,

Colimits, Associated Sheaves, and so on, Bull. Australian Math. Soc. 22 (1980), 1-83. [4]. G.M. Kelly, Structures Defined by Finite Limits in the Enriched Context, 1, Cahiers de

Topologie et Géométrie Différentielle X XIII (1982), 3-42. [5]. G.M. Kelly and A.J. Power, Adjunctions Whose Counits are Coequalizers, and Presentations

of Finitary Enriched Monads, J. Pure and Applied Algebra 89 (1993), 163-179. [6]. Y. Kinoshita and A.J. Power, Lax Naturality Through Enrichment, J. Pure and Applied

Algebra (to appear). [7]. A.J. Power, An Algebraic Formulation for Data Refinement, Lecture Notes in Computer

Science, vol. 442, Spinger-Verlag, 1990, pp. 390-401. [8]. Edmund Robinson, Variations on Algebra: Monadicity and Generalizations of Equational

Theories, Mathematical Structures in Computer Science (to appear).

Department of Mathematics Temple University Philadelphia, PA 19122, USA

Department of Computer Science University of Edinburgh Edinburgh EH9 3JZ Scotland

E-mail address: gordon@euclid.temple.edu