An enriched view on the extended finitary monad--Lawvere theory correspondence
Richard Garner John Power
math.CT 18C10, 18C35, 18D20

=2em An enriched view on the monad–theory
correspondence]An enriched view on the extended
finitary
  monad–Lawvere theory correspondence


R. Garner]Richard Garner
Department of Mathematics, Macquarie University, NSW 2109,
  Australia
richard.garner@mq.edu.au

J. Power]John Power
Department of Computer Science, University of Bath, Claverton
  Down, Bath BA2 7AY, United Kingdom
A.J.Power@bath.ac.uk

[2010]Primary: 18C10, 18C35, 18D20





The authors gratefully acknowledge the support of Australian
  Research Council grants DP160101519 and FT160100393 and of the Royal
  Society International Exchanges scheme, grant number IE151369. No
  data was generated in the research for this paper.


  We give a new account of the correspondence, first established by
  Nishizawa–Power, between finitary monads and Lawvere theories over
  an arbitrary locally finitely presentable base. Our account explains
  this correspondence in terms of enriched category theory: the
  passage from a finitary monad to the corresponding Lawvere theory is
  exhibited as an instance of free completion of an enriched
  category under a class of absolute colimits. This extends work of
  the first author, who established the result in the special case of
  finitary monads and Lawvere theories over the category of sets; a
  novel aspect of the generalisation is its use of enrichment over a
  bicategory, rather than a monoidal category, in order to
  capture the monad–theory correspondence over all locally finitely
  presentable bases simultaneously.


Dedicated to Jiří Adámek on the occasion of his retirement
[
    [
    December 30, 2023
=====================





§ INTRODUCTION



A key theme of Jiří Adámek's superlative research career has
been the study of the subtle interaction between monads and theories,
especially within computer science. We hope he might see this paper as
a development of the abstract mathematics underlying this aspect of
his body of work. Jiří has been an inspiration to both of us, on
both a scientific and a personal level, as he has been to many in
category theory and beyond, and we are therefore pleased to
dedicate this paper to him.

The starting point of our development is the well-known fact that
categorical universal algebra provides two distinct ways to approach
the notion of (single-sorted, finitary) equational algebraic theory.
On the one hand, any such theory 𝕋 gives rise to a Lawvere
theory whose models coincide (to within coherent isomorphism) with the
𝕋-models. Recall that a Lawvere theory is a small
category Ł equipped with an identity-on-objects, strict
finite-power-preserving functor
𝔽^op→Ł and that a model of a
Lawvere theory is a finite-power-preserving functor
Ł→Set, where here 𝔽 denotes the
category of finite cardinals and mappings.

On the other hand, an algebraic theory 𝕋 gives rise to a
finitary (i.e., filtered-colimit-preserving) monad on the category of
sets, whose Eilenberg–Moore algebras also coincide with the
𝕋-models. We can pass back and forth between the
presentations using finitary monads and Lawvere theories in a manner
compatible with semantics; this is encapsulated by an equivalence of
categories fitting into a triangle

    [@!C@C-3.5em]Mnd_f(Set)^op[dr]_-Alg()[rr]^(0.5)≃   d   Law^op[dl]^-Mod()
       CAT

which commutes up to pseudonatural equivalence. Both these categorical
formulations of equational algebraic structure are invariant
with respect to the models, meaning that whenever two algebraic
theories have isomorphic categories of models, the Lawvere theories
and the monads they induce are also isomorphic. However, the two
approaches emphasise different aspects of an equational theory
𝕋. On the one hand, the Lawvere theory Ł encapsulates
the operations of 𝕋: the hom-set Ł(m,n) comprises
all the operations X^m → X^n which are definable in any
𝕋-model X. On the other hand, the action of the monad T
encapsulates the construction of the free 𝕋-model on
any set; though since there are infinitary equational theories which
also admit free models, the restriction to finitary monads is
necessary to recover the equivalence with Lawvere theories.

While the equivalence in (<ref>) is not hard to construct, there
remains the question of how it should be understood. Clarifying this
point was the main objective of <cit.>: it describes
a setting within which both finitary monads on Set and Lawvere
theories can be considered on an equal footing, and in which the
passage from a finitary monad to the associated Lawvere theory can be
understood as an instance of the same process by which one associates:


  * To a locally small category , its Karoubian envelope;

  * To a ring R, its category of
  finite-dimensional matrices;

  * To a metric space, its Cauchy-completion.


The setting is that of -enriched category
theory <cit.>; while the process is that of free
completion under a class of absolute
  colimits <cit.>—colimits that are preserved by
any -functor. The above examples are instances of such a
completion, since:


  * Each locally small category is a Set-category, and splittings
  of idempotents are Set-absolute colimits;

  * Each ring can be seen as a one-object Ab-category and
  the corresponding
  category of finite-dimensional matrices can be obtained by freely adjoining finite
  biproducts—which are Ab-absolute colimits;

  * Each metric space can be seen as an
  ℝ_+^∞-category—where ℝ_+^∞ is
  the monoidal poset of non-negative reals extended by infinity, as
  defined in <cit.>—and its Cauchy-completion can
  be obtained by adding limits for Cauchy sequences which, again as
  in <cit.>, are ℝ_+^∞-absolute
  colimits.


In order to fit (<ref>) into this same setting, one takes as
enrichment base the category  of finitary endofunctors of
Set, endowed with its composition monoidal structure. On the
one hand, finitary monads on Set are the same as monoids in
, which are the same as one-object -categories. On the other
hand, Lawvere theories may also be identified with certain
-categories; the argument here is slightly more involved, and may
be summarised as follows.

A key result of <cit.>, recalled as
Proposition <ref> below, identifies -categories admitting
all absolute tensors (a kind of enriched colimit) with ordinary
categories admitting all finite powers. In one direction, we obtain a
category with finite powers from an absolute-tensored -category by
taking the underlying ordinary category; in the other, we use a
construction which generalises the endomorphism monad (or in
logical terms the complete theory) of an object in a category
with finite powers.

Using this key result, we may identify Lawvere theories with
identity-on-objects strict absolute-tensor-preserving -functors
𝔽^op→Ł, where, overloading notation,
we use 𝔽^op and Ł to denote not just the
relevant categories with finite powers, but also the corresponding
-categories. In <cit.>, the -categories
equipped with an -functor of the above form were termed
Lawvere -categories.

By way of the above identifications, the equivalence (<ref>)
between finitary monads and Lawvere theories can now be re-expressed
as an equivalence between one-object -categories and Lawvere
-categories: which can be obtained via the standard
enriched-categorical process of free completion under all
absolute tensors. The universal property of this completion also
explains the compatibility with the semantics in (<ref>); we
recall the details of this in Section <ref> below.

We thus have three categorical perspectives on equational algebraic
theories: as Lawvere theories, as finitary monads on Set, and
(encompassing the other two) as -categories. It is natural to ask
if these perspectives extend so as to account for algebraic structure
borne not by sets but by objects of an arbitrary locally
finitely presentable category . This is of practical interest,
since such structure arises throughout mathematics and computer
science, as in, for example, sheaves of rings, or monoidal categories,
or the second-order algebraic structure of <cit.>.

The approach using monads extends easily: we simply replace finitary
monads on Set by finitary monads on . The approach using
Lawvere theories also extends, albeit more delicately, by way of the
Lawvere -theories of <cit.>. If we write _f for a skeleton of the
full subcategory of finitely presentable objects in , then a
Lawvere -theory is a small category Ł together with an
identity-on-objects finite-limit-preserving[Note the absence
  of the qualifier “strict”; for a discussion of this, see
  Remark <ref> below.] functor J →Ł;
while a model of this theory is a functor Ł→Set
whose restriction along J preserves finite limits. These definitions
are precisely what is needed to extend the equivalence (<ref>) to
one of the form:

    [@!C@C-3em]Mnd_f()^op[dr]_-Alg()[rr]^(0.5)≃   d   Law()^op .[dl]^-Mod()
       CAT


What does not yet exist in this situation is an extension of the
third, enriched-categorical perspective; the objective of this paper
is to provide one. Like in <cit.>, this will provide
a common setting in which the approaches using monads and using
Lawvere theories can coexist; and, like before, it will provide an
explanation as to why an equivalence (<ref>) should exist,
by exhibiting it as another example of a completion under a class of
absolute colimits.

There is a subtlety worth remarking on in how we go about this. One
might expect that, for each locally finitely presentable , one
simply replaces the monoidal category  of finitary endofunctors of
Set by the monoidal category _ of finitary endofunctors
of , and then proceeds as before. This turns out not to work in
general: there is a paucity of _-enriched absolute colimits,
such that freely adjoining them to a one-object _-category does
not necessary yield something resembling the notion of Lawvere
-theory.

In overcoming this apparent obstacle, we are led to a global analysis
which is arguably more elegant: it involves a single
enriched-categorical setting in which finitary monads and Lawvere
theories over all locally finitely presentable bases coexist
simultaneously, and in which the monad–theory correspondences for
each  arise as instances of the same free completion
process.

This setting involves enrichment not in the monoidal category of
finitary endofunctors of a particular , but in the
bicategory  of finitary functors between locally
presentable categories[In fact, when it comes down to it, we
  will work not with  itself, but with a biequivalent bicategory
   of lex profunctors; see
  Section <ref>.]. The theory of categories
enriched in a bicategory was developed
in <cit.> and will be recalled
in Section <ref> below; for now, note that a one-object
-enriched category is a monad in , thus, a finitary monad
on a locally finitely presentable category. This explains one side of
the correspondence (<ref>); for the other, we extend the key
technical result of <cit.> by showing that
absolute-tensored -categories can be identified with what we
call partially finitely complete categories. These will be
defined in Section <ref> below; they are
categories , not necessarily finitely complete, that come equipped
with a sieve of finite-limit-preserving functors expressing which
finite limits do in fact exist in .

The relevance of this result is as follows. If
J →Ł is a Lawvere -theory, then we may
view both  and Ł as partially finitely complete, and so as
absolute-tensored -categories, on equipping the former with the
sieve of all finite-limit-preserving functors into it, and the
latter with the sieve of all finite-limit-preserving functors which
factor through J. In this way, we can view a Lawvere -theory as
a particular kind of -functor →Ł, where, as
before, we overload notation by using the same names for the
-enriched categories as for the ordinary categories from which
they are derived.

If we term the -functors arising in this way Lawvere
  -categories, then our reconstruction of the
equivalence (<ref>) will follow, exactly as
in <cit.>, upon showing the equivalence of
one-object -categories, and Lawvere -categories; and,
exactly as before, we will obtain this equivalence via the
enriched-categorical process of free completion under absolute
tensors. Moreover, the universal property of this free completion once
again explains the compatibility of this equivalence with the taking
of semantics; thereby giving an enriched-categorical explanation of
the entire triangle (<ref>).




§ THE ONE-OBJECT CASE



In this section, we summarise and discuss the manner in
which <cit.> reconstructs the equivalence of
finitary monads on Set and Lawvere theories from an
enriched-categorical viewpoint. Most of what we will say is simply
revision, but note that the points clarified by
Proposition <ref> and Example <ref> are new.

We start from the observation that finitary monads on Set are
equally monoids in the monoidal category  of finitary endofunctors
of Set, so equally one-object -enriched categories
in the sense of <cit.>. More precisely:

  
  The category of finitary monads on Set is equivalent to the
  category of one-object -enriched categories.


To understand Lawvere theories from the -enriched perspective is a
little more involved. As a first step, note that if
J 𝔽^op→Ł is a Lawvere theory,
then both 𝔽^op and Ł are categories with finite
powers, and J is a finite-power-preserving functor between them.
Thus the desired understanding flows from one of the key results
of <cit.>, which shows that categories admittings
finite powers are equivalent to -enriched categories admitting all
absolute tensors in the following sense.


  If  is a monoidal category and  is a -category, then a
  tensor of X ∈ by V ∈ comprises an object
  V · X ∈ and morphism
  u  V →(X, V · X) in , such that, for
  any U ∈ and Y ∈, the assignation
  
    U (V · X, Y)   ↦  
        U ⊗ V (V · X, Y) ⊗(X,
        V · X) (X, Y)

  gives a bijection between maps U →(V · X, Y) and
  U ⊗ V →(X,Y) in . Such a tensor is said to
  be preserved by a -functor F → if
  the composite morphism
  F_X,V· X∘ u  V →(X,V· X)
  →(FX, F(V · X)) in  exhibits F(V · X) as
  V · FX. Tensors by V ∈ are said to be absolute if
  they are preserved by any -functor.


There is a delicate point here. The theory of <cit.>
considers enrichment only over a symmetric monoidal closed base; by
contrast, our  is non-symmetric and right-closed—meaning
that there exists a right adjoint [V, ] to the functor
() ⊗ V tensoring on the right by an object V. The
value [V,W] of this right adjoint can be computed by first forming
the right Kan extension Ran_V W ∈ [Set, Set],
and then the finitary coreflection of that. On the other hand,  is
not left-closed—meaning that there is not always a right
adjoint to the functor V ⊗ () tensoring on the left
by V—because V ⊗ () will not be cocontinuous if V
itself is not cocontinuous.

While the non-symmetric, right-closed setting is too weak to allow
constructions such as opposite -categories, functor
-categories, or tensor product of -categories, it is strong
enough to allow for a good theory of -enriched colimits—of which
absolute tensors are an example. In particular, we may give the
following tractable characterisation of the absolute tensors over a
right-closed base. In the statement, recall that a left dual
for V ∈ is a left adjoint for V seen as a 1-cell in the
one-object bicategory corresponding to .


  Let  be a right-closed monoidal category. Tensors by V ∈
  are absolute if and only if V admits a left dual in .


This result originates in <cit.>, though some
adaptations to the proof are required in the non-left-closed setting;
we defer giving these to Section <ref> below,
where we will give a proof which works in the more general
bicategory-enriched context.

For now, applying this result when =, we see that tensors by
an object F ∈—a finitary endofunctor of Set—are
absolute just when F has a (necessarily finitary) left adjoint G.
In this case, by adjointness we must have F ≅ ()^G1;
moreover, in order for F to be a finitary endofunctor, G1 must be
finitely presentable in Set, thus, a finite set. So an
-category is absolute-tensored just when it admits tensors by
()^n ∈ for all n ∈ℕ.
In <cit.>, such -categories were called   
representable.

The following further characterisation of the absolute-tensored
-categories is Proposition 3.8 of ibid.; in the statement,
we write -CAT_abs for the 2-category of
absolute-tensored -categories and all (necessarily
absolute-tensor-preserving) -functors and -transformations,
and write FPOW for the 2-category of categories with finite
powers and finite-power-preserving functors.


  
  The underlying ordinary category of any absolute-tensored
   admits finite powers, while the underlying ordinary
  functor of any  between representable -categories
  preserves finite powers. The induced 2-functor
  -CAT_abs→FPOW is an
  equivalence of 2-categories.


This result is the technical heart of <cit.>; as
there, the task of giving its proof will be eased if we replace the
category of finitary endofunctors of Set by the equivalent
functor category [𝔽, Set]. The equivalence in
question arises via left Kan extension and restriction along the
inclusion 𝔽→Set; and transporting the
composition monoidal structure on finitary endofunctors across it
yields the so-called substitution monoidal structure on
[𝔽, Set], with tensor and unit given by
(A ⊗ B)(n) = ∫^k Ak × (Bn)^k and I(n) = n.
Henceforth, we re-define  to be this monoidal category. Having
done so, we see that a general -category  involves objects
X,Y,…, hom-objects (X,Y) ∈ [𝔽, Set], and
composition and identities notated as follows:

    ∫^k (Y,Z)(k) ×(X,Y)(n)^k    →(X,Z)(n)     I(n)    →(X,X)(n) 
    
        [g, f_1, …, f_k]    ↦ g ∘ (f_1, …, f_k)     i    ↦π_i .

Note moreover that, since the unit I ∈ [𝔽, Set] is
represented by 1, the arrows X → Y in the underlying
ordinary category _0 of  are the elements of (X,Y)(1).


  Suppose  is an absolute-tensored -category. Then for each
  X ∈ and n ∈ℕ, we have y_n · X ∈ and
  a unit map y_n →(X, y_n · X), or equally, an
  element u ∈(X, y_n · X)(n), rendering each (<ref>)
  invertible. When U = y_1, the function (<ref>) is given, to
  within isomorphism, by
  
    (y_n · X,Y)(1)    →(X,Y)(n) 
    
          f    ↦ f ∘ (u) ;

  thus, when Y = X we obtain elements
  p_1, …, p_n ∈(y_n · X, X)(1) with
  p_i ∘ (u) = π_i in (X,X)(n). It follows by the
  -category axioms that
  (u ∘ (p_1, …, p_n)) ∘ (u) = u, and so, by (<ref>)
  with Y = y_n · X, that
  u ∘ (p_1, …, p_n) = 𝕀_y_n · X in
  (y_n · X, y_n · X)(1).

  We claim that the maps p_i  y_n · X → X in _0
  exhibit y_n · X as the n-fold power X^n. Indeed, given
  g_1, …, g_n  Z → X in _0, we define
  g  Z → y_n · X by
  g = u ∘ (g_1, …, g_n), and now p_i ∘ (u) = π_i
  implies p_i ∘ (g) = g_i. Moreover, if
  h  Z → y_n · X satisfies p_i ∘ (h) = g_i
  then
  g = u ∘ (p_1 ∘ (h), …, p_n ∘ (h)) = (u ∘ (p_1,
  …, p_n)) ∘ h = h.

  This proves the first claim. The second follows easily from the fact
  that any -functor preserves absolute tensors, and so we have a
  2-functor -CAT_abs→FPOW.
  Finally, to show this is a 2-equivalence we construct an explicit
  pseudoinverse. To each category  with finite powers, we associate
  the -category  with objects those of ,
  with hom-objects (X, Y) = (X^(), Y), with
  composition operations (<ref>) obtained using the universal
  property of power, and with identity elements π_i given by power projections.
  This  is absolute-tensored on taking the tensor of
  X ∈ by y_n to be X^n, with unit element
  1_X^n∈(X, X^n)(n) = (X^n, X^n). It is now
  straightforward to extend the assignation ↦
  to a 2-functor
  FPOW→-CAT_abs, and to show
  that this is pseudoinverse to the underlying ordinary category
  2-functor.


In particular, if J 𝔽^op→Ł is
a Lawvere theory, then we can view both 𝔽^op and
Ł as -categories, and J as an -functor between them.
Defining a Lawvere -category to be a representable
-category Ł equipped with an identity-on-objects, strict
absolute-tensor-preserving -functor
𝔽^op→Ł, it follows easily that:


  
  The category of Lawvere -categories is equivalent to the
  category of Lawvere theories (where maps in each case are commuting
  triangles under 𝔽^op).


Using Propositions <ref> and <ref>, we may now
re-express the the monad–theory correspondence (<ref>) in
-categorical terms as an equivalence between one-object
-categories and Lawvere -categories. We obtain this using the
process of free completion under absolute tensors—a
description of which can be derived
from <cit.>.


  
  Let  be a monoidal category and let _d ⊂ be a
  subcategory equivalent to the full subcategory of objects with left
  duals in . The free completion under absolute tensors of a
  -category  is given by the -category  with:
  
  
  * Objects V · X, where X ∈ and V ∈_d;
  
  * Hom-objects
    (V · X, W · Y) = W ⊗(X,Y) ⊗ V^∗
    (for V^∗ a left dual for V);
  
  * Composition built from composition in  and the counit maps
    ε W^∗⊗ W → I;
  
  * Identities built from the unit maps
    η I → V ⊗ V^∗ and identities in
    .
  


Taking = and _d to be the full subcategory on the y_n's,
we thus arrive at:


  
  The category of one-object -categories is equivalent to the
  category of Lawvere -categories.



  The free completion under absolute tensors of the unit -category
   is 𝔽^op; whence each one-object
  -category  yields a Lawvere -category on applying
  completion under absolute tensors to the unique -functor
  →. In the other direction, we send a Lawvere
  -category J 𝔽^op→Ł to
  the one-object sub--category of Ł on J1.


The conjunction of Propositions <ref>, <ref>
and <ref> now yields the equivalence on the top row
of (<ref>). More pedantically, it yields an equivalence,
which we should check is in fact the usual one:


  
  Let T be a finitary monad on Set, and let  be the
  corresponding one-object -category; thus,  has a single
  object X with (X, X)(n) = Tn, and composition and identities
  coming from the monad structure of T. The free completion
   of  under absolute tensors has objects y_n · X
  for n ∈ℕ—or equally, just natural numbers—and
  hom-objects given by
  
    (n, m) = y_m ⊗(X,X) ⊗
        (y_n)^∗≅ (T(n ×))^m  .

  The underlying ordinary category of  is thus the category
  Ł with natural numbers as objects, and Ł(n,m) = (Tn)^m.
  Similarly, the underlying strict finite-power-preserving functor of
  𝔽^op→ is given by
  postcomposition with the unit of T, and so is precisely the Lawvere
  theory corresponding to the finitary monad T.


To reconstruct the whole pseudocommutative triangle in (<ref>),
we need the following result, which combines Propositions 2.5 and
4.4 of <cit.>; we omit the proof for now,  though
note that the corresponding generalisations over a general locally
finitely presentable base will be proven as Propositions <ref>
and <ref> below.


  
  Let  denote the -category corresponding to the
  category-with-finite-powers Set. The embeddings of finitary
  monads and Lawvere theories into -categories fit into
  pseudocommutative triangles:
  
    [@!C@C-4em]Mnd_f(Set)^op[dr]_-Alg()[rr]^(0.5)   d   -CAT^op[dl]^--CAT(, )
       CAT       and    [@!C@C-3em]Law^op[dr]_-Mod()[rr]^(0.5)   d   -CAT^op[dl]^--CAT(, ) .
       CAT



Given this, to obtain the compability with semantics in (<ref>),
it suffices to show that, for any one-object -category  with
completion under absolute tensors , there is an equivalence
between the category of -functors → and the
category of -functors →. But since by
construction  is absolute-tensored, this follows directly from the
universal property of free completion under absolute tensors.




§ INGREDIENTS FOR GENERALISATION



In the rest of the paper, we extend the analysis of the previous
section to deal with the finitary monad–Lawvere correspondence over
an arbitrary locally finitely presentable (lfp) base. In this section,
we set up the necessary background for this: first recalling
from <cit.> the details of the generalised
finitary monad–Lawvere theory correspondence, and then recalling
from <cit.> some necessary
aspects of bicategory-enriched category theory. We will assume
familiarity with the basic theory of lfp categories as found, for
example, in <cit.>.




 §.§ The monad–theory correspondence over a general lfp base



In extending the monad–theory correspondence (<ref>) from
Set to a given lfp category , one side of the
generalisation is apparent: we simply replace finitary monads on
Set by finitary monads on . On the other side, the
appropriate generalisation of Lawvere theories is given by the
Lawvere -theories of <cit.>:


  
  A Lawvere -theory is a small category Ł together with
  an identity-on-objects, finite-limit-preserving functor
  J →Ł. A morphism of Lawvere
  -theories is a functor Ł→Ł' commuting with the
  maps from . A model for a Lawvere -theory is a
  functor F Ł→Set for which FJ preserves
  finite limits.


Here, and in what follows, we write _f for a small subcategory
equivalent to the full subcategory of finitely presentable objects in
. Note that, while  has all finite limits, we do not assume
the same of Ł; though, of course, it will admit all finite limits
of diagrams in the image of J, and so in particular all finite
products.


  
  Our definition of Lawvere -theory alters that
  of <cit.> by dropping the
  requirement of strict finite limit preservation. However,
  this apparent relaxation does not in fact change the notion of
  theory. To see why, we must consider carefully what this strictness
  amounts to, which is delicate, since Ł need not be finitely
  complete. The correct interpretion is as follows: we fix some choice
  of finite limits in , and also assume that, for each finite
  diagram D →, the category Ł is endowed
  with a choice of limit for JD (in particular, because J is the
  identity on objects, this equips Ł with a choice of finite
  products). We now require that J →Ł send
  the chosen limits in  to the chosen limits in Ł. However, in
  this situation, the choice of limits in Ł is uniquely determined
  by that in  so long as J preserves finite limits in
  the non-algebraic sense of sending limit cones to limit cones. Thus,
  if we interpret the preservation of finite limits in
  Definition <ref> in this non-algebraic sense, then our notion
  of Lawvere -theory agrees
  with <cit.>.

  Note also that our definition of model for a Lawvere -theory is
  that of <cit.>, rather than that
  of <cit.>: the latter paper defines a model to
  comprise A ∈ together with a functor
  F Ł→Set such that
  FJ = (, A) →Set. The equivalence
  of these definitions follows since  is equivalent to the
  category FL(_f^op, Set) of finite-limit-preserving functors
  →Set via the assignation
  A ↦(, A).


Even bearing the above remark in mind, it is not immediate that
Lawvere Set-theories and their models coincide with Lawvere
theories and their models in the previous sense; however, this was
shown to be so in <cit.>. The
correctness of these notions over a general base is confirmed by the
main result of <cit.>, which we restate here as:


  <cit.>
  The category of finitary monads on  is equivalent to the
  category of Lawvere -theories; moreover this equivalence is
  compatible with the semantics in the sense displayed in (<ref>).



  For a finitary monad T on , let Ł_T be the category with
  objects those of _f, hom-sets Ł_T(A,B) = (B,TA), and the
  usual Kleisli composition; now the identity-on-objects
  J_T _f^op→Ł_T sending
  f ∈_f(B,A) to η_A ∘ f ∈Ł_T(A,B) is a Lawvere
  -theory. Conversely, if
  J _f^op→Ł is a Lawvere
  -theory, then the composite of the evident forgetful functor
  Mod(Ł) →FL(_f^op, Set)
  with the equivalence
  FL(_f^op, Set) → is
  finitarily monadic, and so gives a finitary monad T_Ł on .
  With some care one may now show that these processes are
  pseudoinverse in a manner which is compatible with the semantics.





 §.§ Bicategory-enriched category theory



We now recall some basic definitions from the theory of categories
enriched over a bicategory as developed in <cit.>.


  
  Let  be a bicategory whose 1-cell composition and identities
  we write as  and _x respectively. A
  -category  comprises:
  
  
  * A set  of objects;
  
  * For each X ∈, an extent
    ϵ X ∈;
  
  * For each X, Y ∈, a hom-object[There are
      two conventions in the literature: we either take (X,Y) ∈(ϵ X, ϵ Y), as in <cit.>
      for example, or we take (X,Y) ∈(ϵ Y, ϵ X) as in <cit.>. We
      have chosen the former convention here, and have 
      adjusted results from the literature where necessary to conform
      with this.]
    (X,Y) ∈(ϵ X, ϵ Y);
  
  * For each X, Y, Z ∈, composition maps in
    (ϵ X, ϵ Z) of the form
    
    μ_xyz(Y,Z) (X,Y) →(X,Z)  ;

  
  * For each X ∈ an identities map in
    (ϵ X, ϵ X) of the form
    
    ι_X _ϵ X→(X,X)  ;

  
  subject to associativity and unitality axioms. A -functor
  F → between -categories comprises an
  extent-preserving assignation on objects, together with maps
  F_XY(X,Y) →(FX,FY) in
  (ϵ X, ϵ Y) for each X,Y ∈, subject to the
  two usual functoriality axioms. Finally, a -transformation
  α F ⇒ G → between
  -functors comprises maps
  α_x _ϵ X→(FX,GX) in
  (ϵ X, ϵ X) for each X ∈ obeying a
  naturality axiom. We write -CAT for the 2-category of
  -categories, -functors and -transformations.


Note that, if  is the one-object bicategory corresponding to a
monoidal category , then we re-find the usual definitions of
-category, -functor and -transformation. A key difference
in the general bicategorical situation is that a -category does
not have a single “underlying ordinary category”, but a whole family
of them:


  
  For any x ∈, we write _x for the -category with a
  single object ∗ of extent x and with
  _A(∗, ∗) = _x, and write ()_x for the
  representable 2-functor
  -CAT(_x, ) -CAT→CAT. On objects, this 2-functor sends a -category 
  to the ordinary category _x whose objects are the objects of  with
  extent x, and whose morphisms X → Y are morphisms
  _x →(X,Y) in (x,x).





 §.§ Enrichment through variation



It was shown in <cit.> that there is a close link
between -categories and -representations. A
-representation is simply a homomorphism of bicategories
F →CAT, but thought of as a “left
action”; thus, we notate the functors
F_xy(x,y) →CAT(Fx,Fy) as
W ↦ W ∗_F (), and write the components of the coherence
isomorphisms for F as maps
λ I_x ∗_F X → X and
α (V ⊗ W) ∗_F X → V ∗_F (W ∗_F
X).

Theorem 3.7 of <cit.> establishes an equivalence
between closed -representations and tensored
-categories. Here, a -representation is called closed
if each functor () ∗_F W (x,y) → Fy has a
right adjoint W, _F  Fy →(x,y); while a
-category is tensored if it admits all tensors in the
following sense:


  If  is a bicategory and  is a -category, then a
  tensor of X ∈_x by W ∈(x,y) is an object
  W · X ∈_y together with a map
  u  W →(X, W · X) in (x,y) such that,
  for any U ∈(y,z) and Z ∈_z, the assignation
  
    U (W · X, Z)   ↦  
        U ⊗ W (V · X, Z) ⊗(X,
        W · X) (X, Z)

  establishes a bijection between morphisms U →(W · X, Z)
  in (y,z) and morphisms U ⊗ W →(X,Z) in
  (x,z).


We note here for future use that a tensor W · X is said to be
preserved by a -functor F → if the
composite
W →(X, W · X) →(FX, F(W · X))
exhibits F(W · X) as W · FX; and that tensors by a
1-cell W are called absolute if they are preserved by any
-functor.
 
   <cit.>
   There is an equivalence between the 2-category
   -CAT_tens of tensored -categories, 
   tensor-preserving -functors and -natural transformations, and the
   2-category Hom(, CAT)_cl of closed
   -representations, pseudonatural transformations and modifications.
 

 
   In one direction, the closed -representation C associated to a
   tensored -category  is defined on objects by C(x) = _x,
   and with action by 1-cells given by tensors:
   W ∗_C X = W · X. We do not need the further details here,
   and so omit them. In the other direction, the tensored -category
    associated to a closed representation
   F →CAT has objects of extent a being
   objects of Fa; hom-objects given by (X,Y) = X,Y_F; and
   composition and identities given by transposing the maps
   
    (Y,Z_F ⊗X,Y_F) ∗_F X Y,Z_F ∗_F (X,Y_F ∗_F X) Y,Z_F ∗_F Y
          Z

   and λ I_a ∗_F X → X under the closure
   adjunctions. The -category  so obtained admits all tensors on
   taking W · X = W ∗_F X with unit
   W →X, W ∗_F X_F obtained from the closure
   adjunctions.
 

We will make use of this equivalence in
Section <ref> below, and will require the
following easy consequence of the definitions:


  
  Let F →CAT be a closed representation,
  corresponding to the tensored -category , and let
  T  a → a be a monad in , corresponding to the
  one-object -category . There is an isomorphism of categories
  -CAT(, ) ≅ F(T)-Alg, natural in
  maps of monads on a in .



  The action on objects of a -functor → picks out an
  object of extent a in , thus, an object X ∈ Fa. The action
  on homs is given by a map x  T →X,X_F in (a,a),
  while functoriality requires the commutativity of:
  
    [@!C@C-1.5em@-0.5em]    I_a [dl]_η[dr]^ι
    
          T [rr]^x       X,X_F    and    [@C+0.5em@-0.5em] T ⊗ T [r]^-x ⊗ x[d]_μ   X,X_F ⊗X,X_F [d]^μ
    
          T [r]^-x    X,X_F .

  Transposing under adjunction, this is equally to give X ∈ Fa and a map
  T ∗_F X → X satisfying the two axioms to be an algebra for
  F(T) = T ∗_F (). Further, to give a -transformation
  F ⇒ G → is equally to give
  ϕ I_x →X,Y_F such that
  
    [@C+1em]
          T [r]^y[d]_x   Y, Y_F [r]^-φ⊗ 1   X,Y_F ⊗Y,Y_F [d]^μ
    X, X_F [r]^-1 ⊗φ   X,X_F⊗X,Y_F [r]^-μ   X, Y_F

  commutes; which, transposing under adjunction and using the coherence
  constraint I_a ∗ X ≅ X, is equally to give a map X → Y
  commuting with the F(T)-actions. The naturality of the
  correspondence just described in T is easily checked.





§ FINITARY MONADS AND THEIR ALGEBRAS



We now begin our enriched-categorical analysis of the monad–theory
correspondence over an lfp base. We first describe a bicategory 
of lex profunctors which is biequivalent to the bicategory
 of finitary functors between lfp categories, but more
convenient to work with; we then exhibit each finitary monad on an lfp
category as a -category, and the associated category of algebras
as a category of -enriched functors.




 §.§ Finitary monads as enriched categories



The basic theory of lfp categories tells us that for any small
finitely-complete 𝔸, the category
(𝔸, Set) of finite-limit-preserving functors
𝔸→Set is lfp, and moreover that every lfp
category is equivalent to one of this form. So  is biequivalent
to the bicategory whose objects are small finitely-complete
categories, whose hom-category from 𝔸 to 𝔹 is
((𝔸, Set), (𝔹, Set)), and
whose composition is inherited from .

Now, since for any small finitely-complete 𝔸, the inclusion
𝔸^op→(𝔸, Set)
exhibits its codomain as the free filtered-cocomplete category on its
domain, there are equivalences
((𝔸, Set), (𝔹, Set)) ≃
[𝔸^op, (𝔹, Set)]; thus
transporting the compositional structure of  across these
equivalences, we obtain:


  
  The right-closed bicategory  of lex profunctors has:
  

  
  * As objects, small categories with finite limits.

  
  * (𝔸, 𝔹) = [𝔸^op,
    (𝔹, Set)]; we typically identify objects therein
    with functors
    𝔸^op×𝔹→Set
    that preserve finite limits in their second variable.

  
  * The identity 1-cell
    I_𝔸∈(𝔸, 𝔸) is given by
    I_𝔸(a',a) = 𝔸(a',a), while the composition of
    M ∈(𝔸, 𝔹) and
    N ∈(𝔹, ℂ) is given by:
    
    (N ⊗ M)(a, c) = ∫^b ∈𝔹 N(b,c) × M(a,b) .


  
  * For M ∈(𝔸, 𝔹) and
    P ∈(𝔸, ℂ), the right closure
    [M,P] ∈(𝔹, ℂ) is defined by
    
    [M,P](b,c) = ∫_a  [M(a,b), P(a,c)] .

  


By the above discussion,  is biequivalent to , and this
induces an equivalence between the category of monads on  in
—thus, the category of finitary monads on —and the
category of monads on  in . Such monads correspond with
one-object -categories of extent  and so:


  
  For any locally finitely presentable category , the category
  Mnd_f() of finitary monads on  is equivalent to the
  category of -categories with a single object of extent .





 §.§ Algebras for finitary monads as enriched functors



We now explain algebras for finitary monads in the -enriched
context. Composing the biequivalence → with the
inclusion 2-functor →CAT yields a
homomorphism S →CAT which on objects
sends 𝔸 to (𝔸, Set), and for which the
action of a 1-cell M ∈(𝔸, 𝔹) on an object
X ∈(𝔸, Set) is given as on the left in

    (M ∗_S X)(b) = ∫^a ∈𝔸 M(a,b) × Xa         X,Y_S(a,b) = Set(Xa,Yb) .

This S is a closed representation, where for
X ∈(𝔸, Set) and
Y ∈(𝔹, Set) we define X,Y_S as to the
right above; and so applying Proposition <ref> gives a
tensored -category  with objects of extent 𝔸 being
finite-limit-preserving functors 𝔸→Set,
and with hom-objects (X,Y)(a,b) = Set(Xa, Yb).


  
  For any locally finitely presentable category , the embedding of finitary
  monads on  as one-object -categories obtained in
  Proposition <ref> fits into a triangle, commuting up to
  pseudonatural equivalence:
  
    [@!C@C-4em]Mnd_f()^op[dr]_-()-Alg[rr]^(0.5)   d    (-CAT)^op .[dl]^-   -CAT(, )
       CAT




  Given T ∈Mnd_f(), which is equally a monad on  in
  , we can successively apply the biequivalences
  → and → to
  obtain in turn a monad T' on _f^op∈ and a
  monad T” on FL(_f^op, Set). It follows
  easily from the fact of a biequivalence that
  T-Alg≃ T”-Alg.

  Now, starting from T ∈Mnd_f(), the functor across the
  top of (<ref>) sends it to the one-object -category
  ' corresponding to T'; whereupon by Proposition <ref>,
  we have pseudonatural equivalences
  
    -CAT(', ) ≅ S(T')-Alg =
        T”-Alg≃ T-Alg .*

  







 §.§ General -categories



Before turning to the relationship of -categories and Lawvere
-theories, we take a moment to unpack the data for a general
-category . We have objects X, Y, … with associated
extents 𝔸, 𝔹, … in ; while for objects
X ∈_𝔸 and Y ∈_𝔹, we have the
hom-object
(X,Y) 𝔸^op×𝔹→Set, which is a functor preserving finite limits in its second
variable. By the coend formula (<ref>) for 1-cell composition
in , composition in  is equally given by functions

    (Y,Z)(j,k) ×(X,Y)(i,j)    →(X,Z)(i, k) 
    
        (g,f)    ↦ g ∘ f

which are natural in i ∈𝔸 and k ∈ℂ and
dinatural in j ∈𝔹. On the other hand, identities in 
are given by functions
ι_X 𝔸(i,j) →(X,X)(i,j), natural in
i,j ∈𝔸; if we define 1_X,iι_X(1_i), then
the -category axioms for  say that
f ∘ 1_X,i = f = 1_Y,j∘ f for all f ∈(X,Y)(i,j)
and that the operation (<ref>) is associative. Note that the
naturality of each ι_X together with the unit axioms imply that
the action on morphisms of the hom-object (X,Y) is given by

    (X,Y)(φ, ψ) (X,Y)(i,j)    →(X,Y)(i',j')
    
        f    ↦ι_Y(ψ) ∘ f ∘ι_X(φ) .

Applying naturality of ι_X again to this formula yields the
following functoriality equation for any pair of composable maps in
𝔸:

    ι_X(φ' ∘φ) = ι_X(φ') ∘ι_X(φ) .





§ PARTIAL FINITE COMPLETENESS



In the following two sections, we will identify the absolute-tensored
-categories with what we call partially finitely complete
ordinary categories; this identification will take the form of a
biequivalence between suitably-defined 2-categories. We will exploit
this biequivalence in Section <ref> in order to
identify Lawvere -theories with certain functors between absolute-tensored
-categories.



 §.§ Partially finitely complete categories


We begin by introducing the 2-category of partially finitely
complete categories and partially finite-limit-preserving functors.

  
  By a left-exact sieve on a category , we mean a
  collection  of finite-limit-preserving functors
  𝔸→, each with small, finitely-complete
  domain, and satisfying the following conditions, wherein we write
  [𝔸] for those elements of  with domain
  𝔸:
  
  
  * If X ∈[𝔹] and
    G ∈FL(𝔸, 𝔹), then
    XG ∈[𝔸];
  
  * If X ∈[𝔸] and
    X ≅ Y 𝔸→, then
    Y ∈[𝔸];
  
  * Each object of  is in the image of some functor in .
  
  A partially finitely complete category (, _) is a
  category  together with a left-exact sieve _ on it. Where
  confusion is unlikely, we may write (, _) simply as . A
  partially finite-limit-preserving functor
  (, _) → (, _) is a functor
  F → such that FX ∈_ for all
  X ∈_; we call such an F sieve-reflecting if, for
  all Y ∈_, there exists X ∈_ such that
  FX ≅ Y. We write PARFL for the 2-category of
  partially finitely complete categories, partially finite-limit-preserving functors,
  and arbitrary natural transformations.


The following examples should serve to clarify the relevance of these
notions to Lawvere theories over a general lfp base.


  
  Any finitely complete  can be seen as partially finitely
  complete when endowed with the sieve _ of all
  finite-limit-preserving functors into  with small domain. If
   is also finitely complete, then any finite-limit-preserving
  F → is clearly also partially finite-limit-preserving;
  conversely, if F → is partially finite-limit-preserving,
  then for any finite diagram D 𝕀→,
  closing its image in  under finite limits yields a small
  subcategory 𝔸 for which the full inclusion
  J 𝔸→ preserves finite limits. As F
  is partially finite-limit-preserving, the composite
  FJ 𝔸→ also preserves finite limits;
  in particular, the chosen limit cone over D in —which lies
  in the subcategory 𝔸—is sent to a limit cone in .
  It follows there is a full and locally full inclusion of
  2-categories →.



  
  If J _f^op→Ł is a Lawvere
  -theory, then Ł becomes a partially finitely complete
  category when endowed with the sieve generated by J:
  
    _Ł = { F 𝔸→Ł : F ≅ JG  for some
          finite-limit-preserving 
        G 𝔸→_f^op} .

  Clearly _Ł satisfies conditions (i) and (ii) above, and
  satisfies (iii) by virtue of J being bijective on objects.
  Moreover, a partially finite-limit-preserving Ł→ is precisely a
  functor F Ł→ such that FJ ∈_; so in
  particular, a partially finite-limit-preserving Ł→Set is
  precisely a model for the Lawvere -theory Ł.





 §.§ Partial finite completeness and -enrichment


Towards our identification of absolute-tensored -categories with
partially finitely complete categories, we now construct a
2-adjunction

    @<-4.5pt>[r]_-Γ@[r]|-   -CAT@<-4.5pt>[l]_-∫ .



  
  Let  be a partially finitely complete category. The
  -category Γ() has objects of extent 𝔸 given
  by elements X ∈_[𝔸], and remaining data defined as
  follows:
  
  
  * For X ∈_[𝔸] and Y ∈_[𝔹],
    the hom-object Γ()(X,Y) ∈(𝔸, 𝔹)
    is given by Γ()(X,Y)(i,j) = (Xi,Yj). Note that this
    preserves finite limits in its second variable since Y and each
    (Xi, ) do so.
  
  * Composition in Γ() may be specified, as
    in (<ref>), by natural families of functions
    Γ()(Y,Z)(j,k) ×Γ()(X,Y)(i,j) →Γ()(X,Z)(i,k), which we obtain from composition in .
  
  * Identities
    ι_X 𝔸(i,j) →Γ()(X,X)(i,j) =
    (Xi,Xj) are given by the action of X on morphisms.
  
  The -category axioms for Γ() follow from the category
  axioms of  and functoriality of each X.

  If F → is a partially finite-limit-preserving functor,
  then we define the -functor
  Γ(F) Γ() →Γ() to have action
  on objects X ↦ FX (using the fact that FX ∈_
  whenever X ∈_). The components of the action of Γ(F) on hom-objects
  Γ()(X,Y) →Γ()(FX,FY) are functions
  (Xi,Yj) →(FXi,FYj), which are given simply by the
  action of F on morphisms. The -functor axioms are immediate
  from functoriality of F.

  Finally, for a 2-cell
  α F ⇒ G → in
  , we define a -transformation
  Γ(α) Γ(F) ⇒Γ(G) whose
  component I_𝔸→Γ()(FX,GX) is given by
  the dinatural family of elements α_Xi∈(FXi,GXi). The
  -naturality of Γ(α) amounts to the condition that
  Gf ∘α_Xi = α_Yj∘ Ff  FXi →
  GYj for all f  Xi → Yj in ; which is so by
  naturality of α.



  
  The data of Definition <ref> comprise the action on 0-, 1-, and 2-cells 
  of a 2-functor Γ→-CAT, Moreover the 2-functor Γ admits a left 2-adjoint
  ∫-CAT→.



  The 2-functoriality of Γ is easy to check, and so it
  remains to construct its left 2-adjoint ∫. Given a
  -category , we write  for the category with:
  
  
  * Objects of the form (X,i) where
    X ∈_𝔸 and i ∈𝔸;
  
  * Morphisms f  (X,i) → (Y,j) being
    elements f ∈(X,Y)(i,j);
  
  * Identities given by the elements
    1_X,i∈(X,X)(i,i);
  
  * Composition mediated by the functions (<ref>).
  
  Given X ∈_𝔸, we write
  ι_X 𝔸→ for the functor given by
  i ↦ (X,i) on objects and by the identities map
  ι_X 𝔸(i,i') →(X,X)(i,i') of 
  on morphisms; note this is functorial by (<ref>). By the
  definition of  and (<ref>), we have that
  
    (X,Y) = ()(ι_X(), ι_Y()) 𝔸^op×𝔹→Set ;

  in particular, as each (X,Y) preserves finite limits in its
  second variable, each
  functor ( (X,i), ι_Y()) 𝔹→Set
  preserve finite limits, whence each
  ι_Y 𝔹→ preserves finite limits.
  It follows that  is partially finitely complete when endowed
  with the left-exact sieve
  
    _∫ = { G 𝔸→Γ() : G ≅ι_Y F
         for some Y ∈_𝔹 and F ∈FL(𝔸, 𝔹) } .


  We now show that  provides the value at  of a left
  2-adjoint to Γ; thus, we must exhibit isomorphisms of
  categories, 2-natural in ∈, of the form:
  
    (, ) ≅-CAT(, Γ()) .

  Now, to give a partially finite-limit-preserving functor
  F → is to give:
  
  
  * For all X ∈_𝔸 and i ∈𝔸 an object
    F(X,i) ∈; and
  
  * For all f ∈(X,Y)(i,j), a map
    Ff  F(X,i) → F(Y,j) in ,
  
  functorially with respect to the composition (<ref>) and
  composition in , and subject to the requirement that
  Fι_X ∈_[𝔸] for all X ∈_𝔸. On
  the other hand, to give a -functor
  G →Γ() is to give:
  
  
  * For all X ∈_𝔸, a functor
    GX ∈_[𝔸]; and
  
  * For all f ∈(X,Y)(i,j), an element of
    Γ()(GX, GY) = ((GX)i, (GY)j), i.e., a map
    Gf  (GX)i → (GY)j in ,
  
  subject to the same functoriality condition. Thus, given
  F →, we may define
  F̅→Γ() by taking
  F̅X = Fι_X (which is in _[𝔸] by assumption)
  and F̅f = Ff; the functoriality is clear. On the other
  hand, given G →Γ(), we may define
  G̅→ by taking
  G̅(X,i) = (GX)i and G̅f = Gf. Functoriality is again
  clear, but we need to check that
  G̅ι_X ∈_[𝔸] for all X ∈_𝔸.
  In fact we show that G̅ι_X = GX, which is in
  _[𝔸] by assumption. On objects,
  G̅ι_X(i) = G̅(X,i) = (GX)i as required. On morphisms,
  the compatibility of G with identities in  and Γ()
  gives a commuting triangle of sets and functions:
  
    [@!C@C-6em]
           𝔸(i,j)[dl]_-ι_X[dr]^-ι_GX
    (X,X)(i,j)[rr]^-G      Γ()(GX, GX)(i,j) = (GXi, GXj) .

  The left-hand path maps φ∈𝔸(i,j) to
  Gι_X(φ) = G̅ι_X(φ); while by definition of
  Γ() the right-hand path maps φ to GX(φ);
  whence G̅ι_X = GX as required. It is clear from the above
  calculations that the assignations F ↦F̅ and
  G ↦G̅ are mutually inverse, which establishes the
  bijection (<ref>) on objects.

  To establish (<ref>) on maps, let
  F_1, F_2 ⇉. The components of a
  -transformation
  α̅F̅_1 ⇒F̅_2 →Γ() comprise natural families of functions
  α̅_Xij𝔸(i,j) →Γ()(F̅_1X,
  F̅_2X)(i,j) = (F_1ι_X(i), F_2ι_X(j))
  satisfying -naturality. By Yoneda, each α̅_Xij is
  uniquely determined by elements
  α̅_X,i = α̅_Xii(𝕀_i) ∈(F_1(X,i),
  F_2(X,i)) satisfying
  F_2ι_X(φ) ∘α̅_X,i = α̅_X,j∘ F_1ι_X(φ) for all φ∈𝔸(i,j);
  their -naturality is now the requirement that the square
  
    [@C+2em](X,Y)(i,j)[r]^-F_1[d]_F_2   (F_1(X,i),F_1(Y,j))[d]^α̅_Y,j∘ ()
    (F_2(X,i),F_2(Y,j))[r]^-() ∘α̅_X,i   (F_1(X,i),F_2(Y,j))

  commute for each X,Y,i,j. Note that this implies the
  earlier condition that
  F_2ι_X(φ) ∘α̅_X,i = α̅_X,j∘ F_1ι_X(φ) on taking X=Y and evaluating at
  ι_X(φ); now evaluating at a general element, we get the
  condition that
  F_2f ∘α̅_X,i = α̅_Y,j∘ F_1f for
  all f  (X,i) → (Y,j) in —which says
  precisely that we have a natural transformation
  α̅ F_1 ⇒ F_2 →.
  This establishes the bijection (<ref>) on morphisms; the
  2-naturality in  is left as an easy exercise for the reader.





§ ABSOLUTE-TENSORED -CATEGORIES



In this section, we prove the key technical result of this paper,
Theorem <ref>, which shows that the
2-adjunction (<ref>) exhibits  as biequivalent
to the full sub-2-category of -CAT on the
absolute-tensored -categories.




 §.§ Absolute tensors in -categories



We begin by characterising absolute tensors in -categories for an
arbitrary right-closed bicategory . Here, right-closedness
is the condition that, for every 1-cell W ∈(x,y) and every
z ∈, the functor
() ⊗ W (y,z) →(x,z) admits a right
adjoint [W, ] (x,z) →(y,z). In this
setting, we will show that tensors by a 1-cell W are absolute if
and only if W is a right adjoint in . If  were both left-
and right- closed, this would follow from the characterisation of
enriched absolute colimits given in <cit.>, but in
the absence of left-closedness, we need a different proof. The first
step is the following, which is a special case
of <cit.>:


  
  Let  be a bicategory, let  be a -category,
  let X ∈_x and let W ∈(x,y). If W admits the left
  adjoint W^∗∈(y,x), then there is a bijective
  correspondence between data of the following forms:
  
  
  * A map u  W →(X, Y) in (x,y) exhibiting Y as
    W · X;
  
  * Maps u  W →(X, Y) in (x,y) and
    u^∗ W^∗→(Y, X) in (y,x) rendering
    commutative the squares:
    
    I_y [r]^η[d]_ι    W ⊗ W^∗[d]^u
              ⊗ u^∗   
            W^∗⊗ W [r]^ε[d]_u^∗⊗ u    I_x [d]^ι
    (Y,Y) @<-[r]^- μ   (X,Y) ⊗(Y,X)    (Y,X) ⊗(X,Y) [r]^-μ   (X,X) .

  



  Given (a), applying surjectivity in (<ref>) to
  ι_X ∘ε W^∗⊗ W → I_x
  →(X,X) yields a unique map
  u^∗ W^∗→(Y,X) making the square right
  above commute. To see that the left square also commutes, it
  suffices by injectivity in (<ref>) to check that the sides become
  equal after tensoring on the right with u and postcomposing with
  μ(Y,Y) ⊗(X,Y) →(X,Y). This
  follows by a short calculation using commutativity in the right
  square and the triangle identities.

  To complete the proof, it remains to show that if u and u^∗
  are given as in (b), then u exhibits Y as W · X. Thus,
  given g  U ⊗ W →(X,Z), we must show that
  g = μ∘ (f ⊗ u) as in (<ref>) for a unique
  f  U →(Y,Z). We may take f to be
  
    U  U ⊗ W ⊗
        W^∗(X,Z)
        ⊗(Y,X) (Y,Z) ;

  now that g = μ∘ (f ⊗ u) follows on rewriting with
  the right-hand square of (<ref>), the triangle identities and the
  -category axioms for . Moreover, if f'  U →(Y,Z)
  also satisfies g = μ∘ (f' ⊗ u), then substituting
  into (<ref>) gives
  
    f = U  U ⊗ W ⊗
        W^∗(Y,Z) ⊗(X,Y)
        ⊗(Y,X) (Y,Z)

  which is equal to f' via the category axioms for  and the left
  square of (<ref>).


Using this result, we may now prove:


  
  Let  be a right-closed bicategory. Tensors by W ∈(x,y)
  are absolute if and only if the 1-cell W admits a left adjoint
  in .



  If W admits a left adjoint, then the data for a tensor by W can
  be expressed as in Proposition <ref>(b); since these data
  are clearly preserved by any -functor, tensors by W are
  absolute. Conversely, suppose that tensors by W are absolute; we
  will show that W admits the left dual [W,I_x] ∈(y,x). The
  counit ε is the evaluation map
  ev [W, I_x] ⊗ W → I_x, and it
  remains only to define the unit.

  For each a ∈, we have the -representation
  (a, ) →CAT which is closed since
   is right-closed. Thus, by the construction of
  Proposition <ref>, there is a tensored -category
  (a, ) = a/ whose objects of extent b are
  1-cells a → b, whose hom-objects are
  (a/)(X,Y) = [X,Y], and whose tensors are given by
  Y · X = Y ⊗ X.

  Now, for any 1-cell Z ∈(a,b), there is a -functor
  [Z, ]  a/→ b/ given on objects by
  X ↦ [Z,X] and with action
  [X,Y] → [ [Z,X], [Z,Y] ] on hom-objects obtained by
  transposing the composition map in a /. Since tensors by W
  are absolute, they are preserved by
  [Z, ]  a/→ b/; it follows that the map
  
    θ_ZX W ⊗ [Z,X] → [Z, W ⊗ X]

  in (b,z) given by transposing
  W ⊗ev W ⊗ [Z,X] ⊗ Z → W
  ⊗ X is invertible for all Z ∈(a,b) and
  X ∈(a, x). In particular, we have
  θ_W,I_x W ⊗ [W,I_x] ≅ [W,W ⊗ I_x] and
  so a unique η I_y → W ⊗ [W,I_x] such that
  θ_VI∘η is the transpose of the morphism
  ρ_Wλ_W  I_y ⊗ W → W → W
  ⊗ I_x. This condition immediately implies the triangle
  identity (W ⊗ε) ∘ (η⊗ W) = 1, and
  implies the other triangle identity
  (ε⊗ [W,I_x]) ∘ ([W,I_x] ⊗η) = 1
  after transposing under adjunction and using bifunctoriality of
  ⊗.





 §.§ Absolute -tensors



Using the above result, we may now characterise the absolute-tensored
-categories via the construction ∫ of
Proposition <ref>.


  
  A -category  is absolute-tensored if and only if, for all
  X ∈_𝔹 and all
  F 𝔸→𝔹 in , there
  exists Y ∈_𝔸 and a natural isomorphism
  
    [@-0.5em@!C]𝔸[rr]^-F[dr]_-ι_Y   dυ   𝔹[dl]^-ι_X




  We write ()_∗^op→
  for the identity-on-objects homomorphism sending
  F 𝔸→𝔹 to the lex profunctor
  F_∗𝔹𝔸 with
  F_∗(b,a) = 𝔹(b,Fa). Each F_∗ has a left adjoint
  F^∗ in  with F^∗(a,b) = 𝔹(Fa,b), and—as
  all idempotents split in a finitely complete category—the usual
  analysis of adjunctions of profunctors adapts to show that, within
  isomorphism, every right adjoint 1-cell in  arises
  thus. So by Proposition <ref>, a -category  is
  absolute-tensored just when it admits all tensors by 1-cells
  F_∗.

  By Proposition <ref>, this is equally to say that, for all
  X ∈_𝔹 and F ∈(𝔸, 𝔹), we
  can find Y ∈_𝔸 and maps
  u  F_∗→(X, Y) and
  u^∗ F^∗→(Y,X) rendering commutative
  both squares in (<ref>). To complete the proof, it suffices to
  show that the data of u and u^∗ are equivalent to those of an
  invertible transformation υ as in (<ref>). Now, u 
  comprises a natural family of maps
  𝔹(j,Fi) →(X,Y)(j, i); equally, by Yoneda,
  elements
  υ_i ∈(X, Y)(Fi, i) = (ι_X(Fi), ι_Y(i))
  dinatural in i ∈𝔸; or equally, the components of a
  natural transformation υ as in (<ref>). Similar
  arguments show that giving
  u^∗ F^∗→(Y,X) is equivalent to giving a
  natural transformation
  υ^∗ι_Y ⇒ι_X F, and that
  commutativity in the two squares of (<ref>) is equivalent to
  the condition that υ and υ^∗ are mutually
  inverse.


We now have all the necessary ingredients to prove:


  
  The 2-functor
  Γ→-CAT
  of (<ref>) is an equivalence on hom-categories, and its
  biessential image comprises the absolute-tensored -categories.
  Thus Γ exhibits  as biequivalent to
  the full and locally full sub-2-category of -CAT
  on the absolute-tensored -categories.



  By a standard argument, to say that Γ is an equivalence on
  homs is equally to say that each counit component
  ε_∫Γ→
  of (<ref>) is an equivalence in . Now, from the
  definitions, the category ∫Γ has:
  
  
  * Objects being pairs
    (X ∈[𝔸], i ∈𝔸);
  
  * Morphisms (X,i) → (Y,j) being maps
    Xi → Yj in ;
  
  * Composition and identities inherited from ,
  
  while ε_∫Γ→ sends
  (X,i) to Xi and is the identity on homsets. So clearly
  ε_ is fully faithful; while condition (iii) for a
  left-exact sieve ensures that it is essentially surjective, and so
  an equivalence of categories. However, for ε_ to be an
  equivalence in , its pseudoinverse must also be
  partially finite-limit-preserving. This is easily seen to be equivalent to
  ε_ being sieve-reflecting; but for each
  X ∈[𝔸], the functor
  ι_X 𝔸→ sending i to (X,i)
  and φ to Xφ is by definition in the sieve _∫Γ, and
  clearly ε_∘ι_X = X.

  This shows that Γ is locally an equivalence; as for its
  biessential image, this comprises just those
  ∈-CAT at which the unit
  η_→Γ() is an equivalence of
  -categories. Now, from the definitions, Γ() has:
  
  
  * Objects of extent 𝔸 being functors
    𝔸→ in the left-exact sieve
    _∫;
  
  * Hom-objects given by
    Γ()(X,Y) = (X, Y);
  
  * Composition and identities inherited from ,
  
  while the -functor η_→Γ()
  is given on objects by X ↦ι_X, and on homs by the
  equality (X,Y) = ()(ι_X, ι_Y)
  of (<ref>); in particular, it is always fully faithful. To
  characterise when it is essentially surjective, note first that
  isomorphisms in Γ()_𝔸 are equally natural
  isomorphisms in [𝔸, ]. Now as objects of
  Γ()_𝔸 are elements of
  _∫[𝔸], and since by (<ref>) every such
  is isomorphic to ι_X F for some X ∈_𝔹 and
  F ∈(𝔸, 𝔹), we see that η_ is
  essentially surjective precisely when for all X ∈_𝔹
  and F ∈(𝔸, 𝔹) there exists
  Y ∈_𝔸 and a natural isomorphism
  υι_X F ≅ι_Y: which by
  Proposition <ref>, happens precisely when  admits all
  absolute tensors.


We will use this result in the sequel to freely identify
absolute-tensored -categories with partially finitely complete
categories; note that, on doing so, the left 2-adjoint
∫-CAT→
of (<ref>) provides us with a description of the free
  completion of an -category under absolute tensors.




§ LAWVERE -THEORIES AND THEIR MODELS



We are now ready to give our -categorical account of Lawvere
-theories and their models. We will identify each Lawvere -theory
with what we term a Lawvere -category on , and will
identify the category of models with a suitable category of
-enriched functors.




 §.§ Lawvere -theories as enriched categories



Lawvere -categories will involve certain absolute-tensored
-categories, which in light of Theorem <ref>, we may work
with in the equivalent guise of partially finitely complete
categories. In giving the following definition, and throughout the
rest of this section, we view the finitely complete  as being
partially finitely complete as in Example <ref>.


  
  Let  be an lfp category. A Lawvere -category over
     comprises a partially finitely complete category Ł
  together with a map J →Ł in 
  which is identity-on-objects and sieve-reflecting. A morphism of
  Lawvere -categories is a commuting triangle in .



  
  For any locally finitely presentable , the category of
  Lawvere -theories is isomorphic to the category of Lawvere
  -categories over .



  Any Lawvere -theory J →Ł can be viewed
  as a Lawvere -category over  as in Example <ref>; it
  is moreover clear that under this assignation, maps of Lawvere
  -theories correspond bijectively with maps of Lawvere
  -categories. It remains to show that each Lawvere
  -category J →Ł over  arises from a
  Lawvere -theory. Because in this context,  is equipped with
  the maximal left-exact sieve, the fact that J is a morphism in
   is equivalent to the condition that J ∈_Ł—so that,
  in particular, J is finite-limit-preserving. Moreover, the fact of
  J being sieve-reflecting implies that _Ł must be exactly the
  left-exact sieve (<ref>) generated by J.





 §.§ Models for Lawvere -theories as enriched functors


We now describe how models for a Lawvere -theory can be understood
in -categorical terms. Recall from
Section <ref> that we defined  to be the
-category whose objects of extent 𝔸 are
finite-limit-preserving functors 𝔸→Set,
and whose hom-objects are given by (X,Y)(i,j) = Set(Xi,Yj).
By inspection of Definition <ref>, this is equally the
-category Γ(Set) when Set is seen as
partially finitely complete as in Example <ref>.


  
  For any locally finitely presentable category , the
  identification of Lawvere -theories with Lawvere
  -categories on  fits into a triangle, commuting up to
  pseudonatural equivalence:
  
    [@!C@C-5em]Law()^op[dr]_-()-Mod[rr]^(0.5)   d   r1.2em(-CAT)^op[dl]^-   -CAT(, )
       CAT

  wherein the horizontal functor is that sending a Lawvere -theory
  J →Ł to the -category Γ(Ł).



  We observed in Example <ref> above that, if J →Ł is a Lawvere -theory, then the category
Ł-Mod of Ł-models is isomorphic to the hom-category
(Ł, Set).
  
  
  
  
  
 Since
  Γ→-CAT is an
  equivalence on homs, and since Γ(Set) =, we thus
  obtain the components of the required pseudonatural equivalence as
  the composites
  
    Ł-Mod(Ł, Set) -CAT(Γ(Ł), ) .*

  








§ RECONSTRUCTING THE MONAD–THEORY CORRESPONDENCE



We have now done all the hard work necessary to prove our main result.


  The process of freely completing a one-object -category under
  absolute tensors induces, by way of the identifications of
  Propositions <ref> and <ref>, an equivalence betwen
  the categories of finitary monads on  and of Lawvere
  -theories. This equivalence fits into a pseudocommuting
  triangle:
  
    [@!C@C-2em]Mnd_f()^op[dr]_(0.4)()-Alg[rr]    @[d]|≃   Law()^op .[dl]^(0.4) ()-Mod
       CAT




  To obtain the desired equivalence, it suffices by
  Propositions <ref> and <ref> to construct an
  equivalence between the category of -categories with a single
  object of extent _f^op, and the category of Lawvere
  -categories on .

  On the one hand, given the one-object -category , applying
  the free completion under absolute tensors
  ∫-CAT→ to the
  unique -functor ! _→ yields a
  Lawvere -category:
  
    J_ = ∫ ! →∫ ,

  where direct inspection of the definition of ∫ tells us that
  ∫_ = and that ∫ ! is identity-on-objects and sieve-reflecting.

  On the other hand, if J →Ł is a Lawvere
  -category on , then we may form the composite around the
  top and right of the following square, wherein η is a unit
  component of the 2-adjunction (<ref>):
  
    _[r]^-η[d]_F   Γ()[d]^Γ(J)
    _J[r]^-G   Γ(Ł) .

  We now factorise this composite as (identity-on-objects, fully
  faithful), as around the left and bottom, to obtain the required
  one-object -category _J.

  The functoriality of the above assignations is direct; it
  remains to check that they are inverse to within
  isomorphism. First, if  is a one-object -category with
  associated Lawvere -category (<ref>), then in the
  naturality square
  
    __f^op[r]^-η[d]_!   Γ()[d]^Γ(∫ !)
    [r]^-η   Γ(∫)

  for η, the left-hand arrow is identity-on-objects, and the
  bottom fully faithful (by Theorem <ref>). Comparing
  with (<ref>), we conclude by the essential uniqueness of
  (identity-on-objects, fully faithful) factorisations that ≅_J_ as
  required.

  Conversely, if J →Ł is a Lawvere
  -category on  with associated one-object -category
  _J as in (<ref>), then we may form the following diagram:
  
    [dl]_-J__J = ∫F[dr]^-J
    ∫_J[r]_-∫G   ∫Γ(Ł)
          [r]_-ε   Ł

  where ε is a counit component of (<ref>). The
  composite around the left and bottom is the adjoint transpose of
  GF under (<ref>); but by (<ref>),
  GF = Γ(J) ∘η which is in turn the adjoint transpose
  of J. It thus follows that the above triangle commutes. Since both
  ∫F and J are identity-on-objects, so is the horizontal
  composite; moreover, ε is an equivalence by
  Theorem <ref> while ∫G is fully faithful since G is,
  by inspection of the definition of ∫. So the lower composite is
  fully faithful and identity-on-objects, whence invertible, so that
  J ≅ J__J as required.

  We thus have an equivalence as across the top of (<ref>), and
  it remains to show that this renders the triangle below  commutative
  to within pseudonatural equivalence. To this end, consider the
  diagram
  
    [@!C@C-4em]Mnd_f()^op[d] [rr] drr      Law()^op[d]  .
    -CAT^op[rr]^Γ∫[dr]_(0.4)-CAT(,  )     @[d]|≃   -CAT^op[dl]^(0.4)  -CAT(,  )
       CAT^

  The top square commutes to within isomorphism by our construction of
  the equivalence Mnd_f(Set) ≃Law; whilst
  the lower triangle commutes to within pseudonatural equivalence
  because Γ∫ is a bireflector of -categories into
  absolute-tensored -categories, and  is by definition
  absolute-tensored. Finally, by Propositions <ref>
  and <ref>, the composites down the left and the right are
  pseudonaturally equivalent to ()-Alg and
  ()-Mod respectively.


The only thing that remains to check is:

  
    The equivalence constructed in Theorem <ref> agrees with the
    equivalence constructed by Nishizawa–Power in <cit.>.


  We prove this by tracing through the steps by which we constructed
  the equivalence of Theorem <ref>, starting from a finitary
  monad S → in LFP.

  
  
  * We first transport S across the biequivalence
    LFP≃ to get a monad of the form T in
    . From the description of this biequivalence in
    Section <ref>, the underlying lex profunctor
    T _f ×→Set is given by
    T(i,j) = (j,Si), while the unit and multiplication of T are
    induced by postcomposition with those of S.
  
  * We next form the one-object -category  which
    corresponds to T.

  * We next construct the Lawvere -category
  J →∫ corresponding to  by
  applying ∫ to the unique -functor
  _→. From the explicit description of ∫
  in Proposition <ref>, we see that ∫ has the same
  objects as , hom-sets ∫(i,j) = (j,Si), and
  composition as in the Kleisli category of S. Moreover, the functor
  J is the identity on objects, and given on hom-sets by
  postcomposition with the unit of S.

  * Finally, the Lawvere -theory associated to this Lawvere
  -category is obtained by applying the forgetful functor
  →CAT; which, comparing the preceding
  description with the proof of Theorem <ref>, is exactly the
  Lawvere -theory associated to the finitary monad
  S →. 


Gar14b

[AR94]Adamek1994Locally
Jiří Adámek and Jiří Rosický.
Locally presentable and accessible categories, volume 189 of
  London Mathematical Society Lecture Note Series.
Cambridge University Press, 1994.

[BC82]Betti1982Cauchy-completion
R. Betti and A. Carboni.
Cauchy-completion and the associated sheaf.
Cahiers de Topologie et Géométrie Différentielle,
  23(3):243–256, 1982.

[FPT99]Fiore1999Abstract
Marcelo Fiore, Gordon Plotkin, and Daniele Turi.
Abstract syntax and variable binding.
In Logic in Computer Science 14 (Trento, 1999), pages 193–202.
  IEEE Computer Society Press, 1999.

[Gar14a]Garner2014Diagrammatic
Richard Garner.
Diagrammatic characterisation of enriched absolute colimits.
Theory and Applications of Categories, 29:No. 26, 775–780,
  2014.

[Gar14b]Garner2014Lawvere
Richard Garner.
Lawvere theories, finitary monads and Cauchy-completion.
Journal of Pure and Applied Algebra, 218(11):1973–1988, 2014.

[GP97]Gordon1997Enrichment
R. Gordon and A. J. Power.
Enrichment through variation.
Journal of Pure and Applied Algebra, 120(2):167–185, 1997.

[GU71]Gabriel1971Lokal
Peter Gabriel and Friedrich Ulmer.
Lokal präsentierbare Kategorien, volume 221 of Lecture Notes in Mathematics.
Springer-Verlag, 1971.

[Kel82]Kelly1982Basic
G. Maxwell Kelly.
Basic concepts of enriched category theory, volume 64 of London Mathematical Society Lecture Note Series.
Cambridge University Press, 1982.
Republished as: Reprints in Theory and Applications of
  Categories 10 (2005).

[Law73]Lawvere1973Metric
F. William Lawvere.
Metric spaces, generalized logic, and closed categories.
Rendiconti del Seminario Matematico e Fisico di Milano,
  (43):135–166, 1973.
Republished as: Reprints in Theory and Applications of
  Categories 1 (2002).

[LP09]Lack2009Gabriel-Ulmer
Stephen Lack and John Power.
Gabriel-Ulmer duality and Lawvere theories enriched over a
  general base.
Journal of Functional Programming, 19(3-4):265–286, 2009.

[NP09]Nishizawa2009Lawvere
Koki Nishizawa and John Power.
Lawvere theories enriched over a general base.
Journal of Pure and Applied Algebra, 213(3):377–386, 2009.

[Str83a]Street1983Absolute
Ross Street.
Absolute colimits in enriched categories.
Cahiers de Topologie et Geométrie Différentielle
  Catégoriques, 24(4):377–379, 1983.

[Str83b]Street1983Enriched
Ross Street.
Enriched categories and cohomology.
Quaestiones Mathematicae, 6:265–283, 1983.
Republished as: Reprints in Theory and Applications of
  Categories 14 (2005).

[Wal81]Walters1981Sheaves
R. F. C. Walters.
Sheaves and Cauchy-complete categories.
Cahiers de Topologie et Geométrie Différentielle
  Catégoriques, 22(3):283–286, 1981.



