Todd Trimble multisorted Lawvere theories

Contents

This material is in reply to a query of John Baez at the n-Category Café.

Background

This section is just to provide some background for notions of multisorted Lawvere theories, to state a form of John’s desired theorem, and to fix some general notation.

Let i:FinSeti: Fin \to Set be the inclusion of the category of finite sets {1,,n}\{1, \ldots, n\} into the category of all sets. Let Λ\Lambda be a set, and let iΛi \downarrow \Lambda, or just Fin/ΛFin/\Lambda, be the comma category whose objects are pairs (S,x:SΛ)(S, x: S \to \Lambda) where SS is a finite set.

We can think of such a pair (S,x)(S, x) as a finite set fibered over Λ\Lambda, so that all but finitely many fibers are empty. The category Fin/ΛFin/\Lambda has finite coproducts (they are just coproducts in each separate fiber).

A key fact we need is that Fin/ΛFin/\Lambda is the free category with finite coproducts generated by Λ\Lambda. More formally: treat the set Λ\Lambda as a discrete category; there is an evident functor ι:ΛFin/Λ\iota: \Lambda \to Fin/\Lambda which takes λΛ\lambda \in \Lambda to the evident fibered set λ:1Λ\lambda: 1 \to \Lambda.

Lemma

Let CC be a category with finite coproducts, and let f:ΛCf: \Lambda \to C be a functor. There is (up to unique isomorphism) a unique coproduct-preserving functor f˜:Fin/ΛC\tilde{f}: Fin/\Lambda \to C that extends ff along ι:ΛFin/Λ\iota: \Lambda \to Fin/\Lambda. If CC has chosen coproducts, we can demand preservation on the nose.

The idea of proof is that f˜\tilde{f} takes a fibered set x:SΛx: S \to \Lambda to the coproduct iSf(x(i))\sum_{i \in S} f(x(i)) in CC.

Dually, the free category with finite products generated by Λ\Lambda is (Fin/Λ) op(Fin/\Lambda)^{op}. For CC a category with finite products, the product-preserving extension of f:ΛCf: \Lambda \to C to (Fin/Λ) opC(Fin/\Lambda)^{op} \to C will be denoted f f^-.

Definition

A Λ\Lambda-sorted Lawvere theory is a category with finite products Θ\Theta equipped with a finite-product preserving functor k:(Fin/Λ) opΘk: (Fin/\Lambda)^{op} \to \Theta that is the identity on objects. (Thus we can think of Θ\Theta as having chosen products.)

Yes, this is “evil”, but it can be a convenient (and harmless) evil. Even in the usual one-sorted case, if we purge this evil, we can have a Lawvere theory in which the generic object xx is isomorphic to its square x 2x^2. Whereas it is convenient to think of them as distinct so that nn-ary operations in the theory are identified with morphisms x nxx^n \to x, and the arity is well-defined. But anyone who is offended by this evil can rewrite matters, at the cost of some extra words (replacing “identity/bijective on objects” with “essentially surjective”).

As usual, a model of a Lawvere theory Θ\Theta in a category with finite products CC is a product-preserving functor F:ΘCF: \Theta \to C. A homomorphism of models is a natural transformation between such functors. Thus we define the category of models,

Mod C(Θ)Prod(Θ,C),Mod_C(\Theta) \coloneqq \mathbf{Prod}(\Theta, C),

and there is a forgetful functor Mod C(Θ)C ΛMod_C(\Theta) \to C^\Lambda obtained by an obvious composition:

Prod(Θ,C)Prod(k,C)Prod((Fin/Λ) op,C)C Λ.\mathbf{Prod}(\Theta, C) \stackrel{\mathbf{Prod}(k, C)}{\to} \mathbf{Prod}((Fin/\Lambda)^{op}, C) \simeq C^\Lambda.

We will prove

Theorem

Let CC be a category that admits general colimits and finite products that distribute over colimits. Then the forgetful functor Mod C(Θ)C ΛMod_C(\Theta) \to C^\Lambda is monadic.

There are a number of ways of proving this theorem. One idea is to invoke a monadicity theorem, say a crude monadicity theorem, and in fact we will pursue this first. If all we are after is monadicity, then this approach is arguably overkill: the monadicity can be proved in a much “softer” and more direct fashion (by adapting some of Kelly’s ideas on operad theory). This approach is touched upon here; perhaps at some point we’ll go through it in more detail. However, an extra bonus of the approach via crude monadicity is that it makes cocompleteness of Mod C(Θ)Mod_C(\Theta) immediate, by an old result of Linton.

Crude monadicity

Recall the crude monadicity theorem: a functor U:ABU: A \to B is monadic if

  1. UU has a left adjoint F:BAF: B \to A,

  2. The category AA has reflexive coequalizers,

  3. The functor U:ABU: A \to B preserves reflexive coequalizers and reflects isomorphisms.

In the case of the forgetful functor U:Prod(Θ,C)C ΛU: \mathbf{Prod}(\Theta, C) \to C^\Lambda, these conditions are not difficult to check, although for our purposes the existence of the left adjoint will require some preface, so we save this for later.

Lemma

U:Prod(Θ,C)C ΛU: \mathbf{Prod}(\Theta, C) \to C^\Lambda reflects isomorphisms.

Proof

On account of Prod((Fin/Λ) op,C)C Λ\mathbf{Prod}((Fin/\Lambda)^{op}, C) \simeq C^\Lambda, this is equivalent to saying the functor G:Prod(Θ,C)Prod((Fin/Λ) op,C)G: \mathbf{Prod}(\Theta, C) \to \mathbf{Prod}((Fin/\Lambda)^{op}, C), induced from the product-preserving functor k:(Fin/Λ) opΘk: (Fin/\Lambda)^{op} \to \Theta, reflects isomorphisms.

Suppose M,N:ΘCM, N: \Theta \to C are product-preserving functors and ψ:MN\psi: M \to N is a natural transformation, such that the whiskering ψk:MkNk\psi k: M k \to N k is invertible. But such a natural transformation is invertible iff all its components ψk(x)\psi k (x) are invertible. Since kk is the identity on objects, this means each component ψ(x)\psi (x) is invertible, so ψ\psi itself is invertible, as was to be shown.

Lemma

Suppose CC has finite products and reflexive coequalizers, and that products distribute over reflexive coequalizers. Then the product functor C×CCC \times C \to C preserves reflexive coequalizers.

The following proof is based on a neat argument given by Steve Lack. Another proof may be based on lemma 0.17 from Johnstone’s Topos Theory, page 4 (you can see it by looking inside the book at Amazon).

Proof

The walking reflexive fork abaa \to b \stackrel{\to}{\to} a is a sifted category DD, meaning precisely that the diagonal functor Δ:DD×D\Delta: D \to D \times D is a final functor. (See Adámek, Rosický, Vitale for basic information on sifted categories and sifted colimits; see particularly their example 1.2.)

Now suppose we have a reflexive fork diagram DC×CD \to C \times C given by two reflexive fork diagrams F,G:DCF, G: D \to C in our category CC. We have

(colim dDF(d))×(colim dDG(d)) colim dD[F(d)×colim dDG(d)] colim dDcolim dD[F(d)×G(d)] colim (d,d)D×DF(d)×G(d) colim dDF(d)×G(d)\array{ (colim_{d \in D} F(d)) \times (colim_{d' \in D} G(d')) & \cong & colim_{d \in D} [F(d) \times colim_{d' \in D} G(d')] \\ & \cong & colim_{d \in D} colim_{d' \in D} [F(d) \times G(d')] \\ & \cong & colim_{(d, d') \in D \times D} F(d) \times G(d') \\ & \cong & colim_{d \in D} F(d) \times G(d) }

where the first two isomorphisms are come from products distributing over reflexive coequalizers, the third comes from a “Fubini theorem”, and the last from the finality of Δ:DD×D\Delta: D \to D \times D. This shows the product applied to a reflexive coequalizer of F,G:DC×C\langle F, G\rangle: D \to C \times C is canonically isomorphic to the reflexive coequalizer of the product F×G:DCF \times G: D \to C, as was to be shown.

Proposition

If products distribute over reflexive coequalizers in CC, then Prod(Θ,C)\mathbf{Prod}(\Theta, C) admits reflexive coequalizers and U:Prod(Θ,C)C ΛU: \mathbf{Prod}(\Theta, C) \to C^\Lambda preserves them.

Proof

Let [Θ,C][\Theta, C] denote the category of all functors ΘC\Theta \to C; this certainly has reflexive coequalizers if CC has them. For any category AA, let A DA^D be the category of reflexive fork diagrams in AA. Let

j:Prod(Θ,C)[Θ,C]j: \mathbf{Prod}(\Theta, C) \hookrightarrow [\Theta, C]

be the full inclusion. We show Prod(Θ,C)\mathbf{Prod}(\Theta, C) is closed under reflexive coequalizers as computed in [Θ,C][\Theta, C], i.e., that the composite (where “colimcolim” means coequalizer)

Prod(Θ,C) Dj D[Θ,C] Dcolim[Θ,C]\mathbf{Prod}(\Theta, C)^D \underset{j^D}{\hookrightarrow} [\Theta, C]^D \underset{colim}{\to} [\Theta, C]

factors through the full inclusion j:Prod(Θ,C)[Θ,C]j: \mathbf{Prod}(\Theta, C) \hookrightarrow [\Theta, C]. This will mean both that Prod(Θ,C)\mathbf{Prod}(\Theta, C) has reflexive coequalizers and that jj preserves them, whence UU which is the composite

Prod(Θ,C)j[Θ,C][kι,1 C][Λ,C]=C Λ\mathbf{Prod}(\Theta, C) \underset{j}{\hookrightarrow} [\Theta, C] \underset{[k\iota, 1_C]}{\to} [\Lambda, C] = C^\Lambda

also preserves them.

But if θ 1,θ 2\theta_1, \theta_2 are two objects of Θ\Theta, and if F:DProd(Θ,C)F: D \to \mathbf{Prod}(\Theta, C) is a reflexive fork, then colimjFcolim\; j F preserves the product θ 1×θ 2\theta_1 \times \theta_2 since

[colim dDF(d)](θ 1)×[colim dDF(d)](θ 2) colim d[F(d)(θ 1)]×colim d[F(d)(θ 2)] colim d[F(d)(θ 1)×F(d)(θ 2)] colim dF(d)(θ 1×θ 2) [colim dF(d)](θ 1×θ 2)\array{ [colim_{d \in D} F(d)](\theta_1) \times [colim_{d' \in D} F(d')](\theta_2) & \cong & colim_d [F(d)(\theta_1)] \times colim_{d'} [F(d')(\theta_2)] \\ & \cong & colim_d [F(d)(\theta_1) \times F(d)(\theta_2)] \\ & \cong & colim_d F(d)(\theta_1 \times \theta_2) \\ & \cong & [colim_d F(d)](\theta_1 \times \theta_2) }

where the first and last isomorphisms hold since colimits in [Θ,C][\Theta, C] are computed pointwise, the second isomorphism holds by the lemma, and the third holds since each F(d):ΘCF(d): \Theta \to C is product-preserving.

Existence of the left adjoint

Now we show that U:Prod(Θ,C)C ΛU: \mathbf{Prod}(\Theta, C) \to C^\Lambda has a left adjoint Free:C ΛProd(Θ,C)Free: C^\Lambda \to \mathbf{Prod}(\Theta, C), under the following assumptions

We will call such a category cartesian monoidally cocomplete, or CMC. (Another name for it could be ‘cartesian 2-rig’, and indeed some of the material below is a cartesian analogue of the formalism of typed operads in the context of 2-rigs; see Baez-Dolan, section 2.3.)

It’s possible to dive right in and write down a coend formula for the asserted left adjoint FreeFree, but it is clarifying to introduce it by telling a little abstract story. The basic theme is the idea of the free cartesian monoidally cocomplete category on a set Λ\Lambda and suitable monads thereon as being “Λ\Lambda-typed cartesian operads”; this kind of idea has been used by various authors (Kelly, Baez-Dolan) in the symmetric monoidal case instead of the cartesian monoidal case undertaken here, but the development is conceptually almost identical. We will see that typed or multisorted Lawvere theories canonically give rise to such typed cartesian operads.

Proposition

Let DD be a category with finite products. For CMC categories A,BA, B, let CMC(A,B)\mathbf{CMC}(A, B) denote the category of finite-product preserving, cocontinuous functors between them. Then, if DD is a category with finite products, then the Day convolution product on Set D opSet^{D^{op}} induced by the cartesian monoidal structure on DD is also cartesian, and Set D opSet^{D^{op}} is CMC. Furthermore, Set D opSet^{D^{op}} is the free CMC category generated by DD as a cartesian monoidal category, in the sense that for any CMC category there is an equivalence

Prod(D,C)CMC(Set D op,C)\mathbf{Prod}(D, C) \simeq \mathbf{CMC}(Set^{D^{op}}, C)

which takes a finite-product preserving functor H:DCH: D \to C to the left Kan extension H^\widehat{H}, of HH along the Yoneda embedding DSet D opD \to Set^{D^{op}}.

I won’t go through the proof here (which is outlined for example here), but it will be handy to recall the coend formula for the left Kan extension: it is

H^(W)= dDH(d)W(d)\widehat{H}(W) = \int^{d \in D} H(d) \cdot W(d)

where W:D opSetW: D^{op} \to Set is a weight over DD.

Proposition

Set Fin/ΛSet^{Fin/\Lambda} is the free cartesian monoidally cocomplete category generated by the discrete category Λ\Lambda.

The point is that for a cartesian monoidally cocomplete CC, there are equivalences of categories

[Λ,C]Prod((Fin/Λ) op,C)CMC(Set Fin/Λ,C)[\Lambda, C] \simeq \mathbf{Prod}((Fin/\Lambda)^{op}, C) \simeq \mathbf{CMC}(Set^{Fin/\Lambda}, C)

both of which have been described above. Putting them together: there is in the first place, for each typing f:ΛCf: \Lambda \to C an induced finite-product preserving map f :(Fin/Λ) opCf^-: (Fin/\Lambda)^{op} \to C; here we think of f xf^x as being a fiberwise finite power of ff if x:SΛx: S \to \Lambda is a finite set over Λ\Lambda, i.e.,

f x= λΛf(λ) x λ.f^x = \prod_{\lambda \in \Lambda} f(\lambda)^{x_\lambda}.

where x λx_\lambda denotes the fiber over λ\lambda. In the second place, we pass from f f^- to a CMC functor Set Fin/ΛCSet^{Fin/\Lambda} \to C defined on weights W:Fin/ΛSetW: Fin/\Lambda \to Set by

W x(Fin/Λ) opW(x)f x.W \mapsto \int^{x \in (Fin/\Lambda)^{op}} W(x) \cdot f^x.

Now for a key definition:

Definition

A Λ\Lambda-typed or Λ\Lambda-sorted cartesian operad is a monoid in the monoidal category CMC(Set Fin/Λ,Set Fin/Λ)\mathbf{CMC}(Set^{Fin/\Lambda}, Set^{Fin/\Lambda}) (taking endofunctor composition as the monoidal product and the identity as monoidal unit).

A principal moral of our story is that a Λ\Lambda-typed cartesian operad is essentially the same thing as Λ\Lambda-sorted Lawvere theory. We need just a little from that story here.

Let Θ\Theta be a Λ\Lambda-sorted Lawvere theory (with canonical product-preserving functor k:(Fin/Λ) opΘk: (Fin/\Lambda)^{op} \to \Theta; recall also our earlier notation ι:Λ(Fin/Λ) op\iota: \Lambda \to (Fin/\Lambda)^{op} for the canonical inclusion). The Lawvere theory Θ\Theta gives rise to a product-preserving functor (Fin/Λ) opSet Fin/Λ(Fin/\Lambda)^{op} \to Set^{Fin/\Lambda} defined by

(x(Fin/Λ) op)(hom Θ(k,k(x)):Fin/ΛSet).(x \in (Fin/\Lambda)^{op}) \;\;\; \mapsto \;\;\;(\hom_{\Theta}(k-, k(x)): \;\; Fin/\Lambda \to Set).

According to our development, this gives rise to a CMC endofunctor which we denote Op(Θ):Set Fin/ΛSet Fin/ΛOp(\Theta): Set^{Fin/\Lambda} \to Set^{Fin/\Lambda}:

(W:Fin/ΛSet) x(Fin/Λ) ophom Θ(k,k(x))W(x).(W: Fin/\Lambda \to Set) \;\;\; \mapsto \;\;\; \int^{x \in (Fin/\Lambda)^{op}} \hom_{\Theta}(k-, k(x)) \cdot W(x).

Composition in Θ\Theta induces a monad multiplication for Op(Θ)Op(\Theta):

(Op(Θ)Op(Θ))(W) = y xhom Θ(k,k(y))hom Θ(k(y),k(x))W(x) x yhom Θ(k,k(y))hom Θ(k(y),k(x))W(x) xcomp1 W(x) xhom Θ(k,k(x))W(x)=Op(Θ)(W)\array{ (Op(\Theta) \circ Op(\Theta))(W) & = & \int^y \int^x \hom_{\Theta}(k-, k(y)) \cdot \hom_{\Theta}(k(y), k(x)) \cdot W(x) \\ &\cong & \int^x \int^y \hom_{\Theta}(k-, k(y)) \cdot \hom_{\Theta}(k(y), k(x)) \cdot W(x) \\ & \stackrel{\int^x comp \cdot 1_{W(x)}}{\to} & \int^x \hom_{\Theta}(k-, k(x)) \cdot W(x) = Op(\Theta)(W) }

and similarly identities in Θ\Theta induce a monad unit for Op(Θ)Op(\Theta). This defines the cartesian operad associated with the Lawvere theory Θ\Theta.

Definition

Let CC be a CMC category, and let M:Set Fin/ΛSet Fin/ΛM: Set^{Fin/\Lambda} \to Set^{Fin/\Lambda} be a Λ\Lambda-sorted cartesian operad. The monad induced by MM on [Λ,C][\Lambda, C] is the monad M CM_C obtained by transporting the monad

CMC(Set Fin/Λ,C)MCMC(Set Fin/Λ,C)\mathbf{CMC}(Set^{Fin/\Lambda}, C) \stackrel{- \circ M}{\to} \mathbf{CMC}(Set^{Fin/\Lambda}, C)

across the equivalence CMC(Set Fin/Λ,C)[Λ,C]\mathbf{CMC}(Set^{Fin/\Lambda}, C) \simeq [\Lambda, C].

Actually, it seems a good idea to overload the notation and use M CM_C for any one of three monads induced by MM:

since all three indicated categories are canonically equivalent – and let the choice be dictated by doctrinal needs.

In particular, to construct the free Θ\Theta-model in Prod(Θ,C)\mathbf{Prod}(\Theta, C) generated by a typing function f:ΛCf: \Lambda \to C, the obvious choice is the second. Here the monad

Op(Θ) C:Prod((Fin/Λ) op,C)Prod((Fin/Λ) op,C)Op(\Theta)_C: \mathbf{Prod}((Fin/\Lambda)^{op}, C) \to \mathbf{Prod}((Fin/\Lambda)^{op}, C)

takes the product-preserving functor f :(Fin/Λ) opCf^-: (Fin/\Lambda)^{op} \to C to another product-preserving functor (Fin/Λ) opC(Fin/\Lambda)^{op} \to C, which by following the formulas above is expressed by the coend

x(Fin/Λ) ophom Θ(k(x),k)f x.\int^{x \in (Fin/\Lambda)^{op}} \hom_{\Theta}(k(x), k-) \cdot f^x.

In essence this gives the free model generated by f:ΛCf: \Lambda \to C. More exactly, the free model (as a product-preserving functor Free(f):ΘCFree(f): \Theta \to C) is just

Free(f) xhom Θ(k(x),)f x.Free(f) \coloneqq \int^x \hom_{\Theta}(k(x), -) \cdot f^x.

This is manifestly a functor ΘC\Theta \to C.

Proposition

Free(f):ΘCFree(f): \Theta \to C is product-preserving.

Proof

We already know that Free(f)k:(Fin/Λ) opCFree(f) \circ k: (Fin/\Lambda)^{op} \to C is product-preserving, since that is exactly

xhom Θ(k(x),k)f x=Op(Θ) C(f )\int^x \hom_{\Theta}(k(x), k-) \cdot f^x = Op(\Theta)_C(f^-)

and Op(Θ) COp(\Theta)_C was after all designed to land in product-preserving functors Prod((Fin/Λ) op,C)\mathbf{Prod}((Fin/\Lambda)^{op}, C). But a functor G:ΘCG: \Theta \to C is product-preserving iff GkG \circ k is product-preserving: this is because product-preservation just comes down to preservation of projection and diagonal maps for all objects x,yx, y in Θ\Theta, and all that projection and diagonal data is already contained in (Fin/Λ) op(Fin/\Lambda)^{op} under the product-preserving “inclusion” k:(Fin/Λ) opΘk: (Fin/\Lambda)^{op} \to \Theta (which we recall is the identity on objects).

Proposition

Free:[Λ,C]Prod(Θ,C)Free: [\Lambda, C] \to \mathbf{Prod}(\Theta, C) is left adjoint to U:Prod(Θ,C)[Λ,C]U: \mathbf{Prod}(\Theta, C) \to [\Lambda, C].

Proof

Suppose M:ΘCM: \Theta \to C is product-preserving and that we have a natural transformation Free(f)MFree(f) \to M. We have natural bijections between families that are extranatural in the indicated arguments, as follows:

xhom Θ(k(x),θ)f xM(θ) hom Θ(k(x),θ)f xM(θ) f xM(θ) hom Θ(k(x),θ) f x θM(θ) hom Θ(k(x),θ) f xNat(hom Θ(k(x),),M)f xM(k(x))Yonedalemma \array{ \arrayopts{\rowlines{solid}} \displaystyle{\int^x} \hom_\Theta(k(x), \theta) \cdot f^x \to M(\theta) \\ \hom_\Theta(k(x), \theta) \cdot f^x \to M(\theta) \\ f^x \to M(\theta)^{\hom_\Theta(k(x),\theta)} \\ f^x \to \displaystyle{\int_\theta} M(\theta)^{\hom_\Theta(k(x), \theta)} \\ \frac {f^x \to Nat(\hom_\Theta(k(x), -), M)} {f^x \to M(k(x))} \; Yoneda\; lemma }

with both sides product-preserving in xOb((Fin/Λ) op)x \in Ob((Fin/\Lambda)^{op}). Under the equivalence Prod((Fin/Λ) op,C)[Λ,C]\mathbf{Prod}((Fin/\Lambda)^{op}, C) \simeq [\Lambda, C], the last is in natural bijection with maps

fM(kι)=U(M)f \to M(k \circ \iota) = U(M)

in [Λ,C][\Lambda, C]. This completes the proof, and thus also the proof of Theorem 1.

Further consequences

It goes without saying that if CC and therefore also C ΛC^\Lambda is complete, then so is any monadic category over C ΛC^\Lambda such as Mod C(Θ)Mod_C(\Theta). In general it is not true that a category that is monadic over a cocomplete category is itself cocomplete, but fortunately the following is true.

Proposition

If CC is CMC, then the category of models Mod C(Θ)Mod_C(\Theta) is cocomplete for any Λ\Lambda-sorted Lawvere theory Θ\Theta.

Proof

It is an old result of Linton that if BB is cocomplete and TT is a monad on BB, then the category of algebras A=B TA = B^T is cocomplete if it has reflexive coequalizers. This applies here to give the desired conclusion, in view of Proposition 1, Theorem 1, and the fact that C ΛC^\Lambda is cocomplete.

For convenience we reproduce a proof of Linton’s result here. Let U:ABU: A \to B be monadic with left adjoint F:BAF: B \to A; let TT be the monad UFU F; let η:1 BUF\eta : 1_B \to U F be the unit and ε:FU1 A\varepsilon: F U \to 1_A be the counit of the adjunction. First, a family of free TT-algebras {F(c i)} iI\{F(c_i)\}_{i \in I} has a coproduct: it’s just F( ic i)F(\sum_i c_i) since the left adjoint FF preserves coproducts.

Next, under our hypotheses, the category of TT-algebras AA has arbitrary coproducts, because the coproduct of a family {a i} iI\{a_i\}_{i \in I} of algebras can be exhibited as a coequalizer of a reflexive fork diagram consisting of coproducts of free algebras:

iFUa i iFηUa i iFUFUa i iFUεa i iεFUa i iFUa i.\sum_i F U a_i \stackrel{\sum_i F \eta U a_i}{\to} \sum_i F U F U a_i \overset{\sum_i \varepsilon F U a_i}{\underset{\sum_i F U \varepsilon a_i}{\rightrightarrows}} \sum_i F U a_i.

Finally, coequalizers (not just reflexive coequalizers) exist in AA, because AA has binary coproducts, and the coequalizer of a general pair of arrows agfaa' \stackrel{\overset{f}{\to}}{\underset{g}{\to}} a can be computed as the coequalizer of the reflexive fork

aincla+a(1 a,g)(1 a,f)a.a \stackrel{incl}{\to} a+a' \overset{(1_a,f)}{\underset{(1_a, g)}{\rightrightarrows}} a.
Remark

As pointed out to me by Mike Shulman, the standard presentation of colimits in terms of coproducts and coequalizers is actually in terms of coproducts and reflexive coequalizers (being a truncation of a simplicial object, namely a two-sided bar construction). This observation can be used in lieu of the final paragraph of the proof above of Linton’s result.

Let k:(Fin/Λ) opΘk: (Fin/\Lambda)^{op} \to \Theta and k:(Fin/Λ) opΘk': (Fin/\Lambda)^{op} \to \Theta' be Λ\Lambda-sorted Lawvere theories. A morphism of theories is a finite-product preserving functor ΘΘ\Theta \to \Theta'. This is the same as a functor g:ΘΘg: \Theta \to \Theta' such that k=gkk' = g \circ k (since the projection and diagonal map data on objects of Θ\Theta are already in (Fin/Λ) op(Fin/\Lambda)^{op}, and k,kk, k' are product-preserving).

Theorem

If CC is CMC and g:ΘΘg: \Theta \to \Theta' is a morphism of theories, then the functor

g *Prod(g,C):Prod(Θ,C)Prod(Θ,C)g^\ast \coloneqq \mathbf{Prod}(g, C): \; \mathbf{Prod}(\Theta', C) \to \mathbf{Prod}(\Theta, C)

is monadic.

Lemma

g *:Prod(Θ,C)Prod(Θ,C)g^\ast: \; \mathbf{Prod}(\Theta', C) \to \mathbf{Prod}(\Theta, C) preserves reflexive coequalizers and reflects isomorphisms (we already know Prod(Θ,C)\mathbf{Prod}(\Theta', C) has reflexive coequalizers).

Proof

That g *g^\ast reflects isomorphisms is easy: given that g *(f)g^\ast(f) is an iso, then also k *g *(f)=(k) *(f)k^\ast g^\ast(f) = (k')^\ast(f) is an iso, whence ff is an iso since (k) *(k')^\ast reflects isos.

Similarly, suppose i,ji, j is a reflexive pair of maps MNM \to N in Prod(Θ,C)\mathbf{Prod}(\Theta', C), with coequalizer p:NPp: N \to P, and suppose the reflexive pair g *(i),g *(j)g^\ast(i), g^\ast(j) in Prod(Θ,C)\mathbf{Prod}(\Theta, C) has coequalizer q:g *(N)Qq: g^\ast(N) \to Q. Then there is a unique map r:Qg *(P)r: Q \to g^\ast(P) such that g *(p)=rqg^\ast(p) = r \circ q; to show g *g^\ast preserves reflexive coequalizers, we must show rr is an iso. Since k *k^\ast preserves reflexive coequalizers, we see k *(q)k^\ast(q) is the coequalizer of

(k *g *(i),k *g *(j))=((k) *(i),(k) *(j))(k^\ast g^\ast(i), k^\ast g^\ast(j)) = ((k')^\ast(i), (k')^\ast(j))

as is (k) *(p)=k *g *(p)(k')^\ast(p) = k^\ast g^\ast(p) since (k) *(k')^\ast preserves reflexive coequalizers. This implies k *(r)k^\ast(r) is an iso, and so rr is an iso since k *k^\ast reflects isos.

Proof of Theorem

We invoke the crude monadicity theorem; in view of the preceding lemma, the only hypothesis left to verify is the existence of a left adjoint to g *g^\ast. But this clearly follows from the adjoint triangle theorem.

References

The consideration of CMC categories closely parallels the development of operad theory in terms of 2-rigs given here:

The preceding article was discussed further (with some errors corrected) in

Also providing a template for the abstract consideration of cartesian monoidally cocomplete categories is the seminal article of Kelly:

Revised on January 31, 2018 at 15:57:42 by Todd Trimble