nLab
infinitary Lawvere theory

Infinitary Lawvere theories

Idea

An infinitary Lawvere theory is a generalisation of a Lawvere theory to allow infinitary operations. As a motivating example, consider the theory of suplattices, where we have, for every cardinal number nn, an operation to take the supremum of nn elements.

Size issues can be tricky for infinitary Lawvere theories. NaΓ―vely, you would expect an infinitary Lawvere theory of complete lattices too, but there is none, because a smallness condition fails. (This is connected to the nonexistence of free complete lattices.)

In accordance with the red herring principle, an infinitary Lawvere theory should not be thought of a special case of a Lawvere theory. To avoid this, one may call the latter a finitary Lawvere theory.

There are also many-sorted infinitary Lawvere theories, as well as ΞΊ\kappa-ary Lawvere theories for any regular cardinal ΞΊ\kappa.

Definitions

A many-sorted infinitary Lawvere theory is a locally small category π’Ÿ\mathcal{D} with all small products and with a small collection β„›\mathcal{R} of objects (called sorts) such that every object is a small product of these sorts.

Given a small set SS, an SS-sorted infinitary Lawvere theory is a locally small category π’Ÿ\mathcal{D} with all small products and equipped with an SS-indexed family β„›\mathcal{R} of objects (called sorts) such that every object is a small product of these sorts. (Note that an SS-indexed family of objects is precisely a functor to π’Ÿ\mathcal{D} from the discrete category on SS.)

If (π’Ÿ,β„›)(\mathcal{D},\mathcal{R}) is an SS-sorted infinitary Lawvere theory, then π’Ÿ\mathcal{D} is a many-sorted infinitary Lawvere theory; conversely, any many-sorted infinitary Lawvere theory may be interpreted as an SS-sorted infinitary Lawvere theory, where SS is (the set of isomoprhism classes of) an appropriate family β„›\mathcal{R} and the SS-indexed family is given by the identity indexing.

An unsorted infinitary Lawvere theory is a locally small category π’Ÿ\mathcal{D} with all small products and equipped with an object RR (so that (π’Ÿ,R)(\mathcal{D},R) is a pointed category) such that every object is isomorphic to R nR^n for some small cardinal number nn. An infinitary Lawvere theory is by default an unsorted infinitary Lawvere theory, invoking the red herring principle. Note that an unsorted infinitary Lawvery theory is the same thing as a 11-sorted infinitary Lawvere theory.

We will give the definitions of further special cases for unsorted infinitary Lawvere theories, but these definitions may also be generalised to the many-sorted case.

Given a regular cardinal ΞΊ\kappa, a ΞΊ\kappa-ary Lawvere theory is a locally small pointed category (π’Ÿ,R)(\mathcal{D},R) with all nn-ary products for n<ΞΊn \lt \kappa such that every object is isomorphic to R nR^n for some n<ΞΊn \lt \kappa. Every ΞΊ\kappa-ary Lawvere theory may be interpreted as an infinitary Lawvere theory by using the free category with all small products on π’Ÿ\mathcal{D}. More generally, every ΞΊ\kappa-ary Lawvere theory may be interpreted as a Ξ»\lambda-ary Lawvere theory if κ≀λ\kappa \leq \lambda.

A bounded infinitary Lawvere theory is an infinitary Lawvere theory which is (under the interpretation above) equivalent to some ΞΊ\kappa-ary Lawvere theory.

A finitary Lawvere theory is a locally small pointed category (π’Ÿ,R)(\mathcal{D},R) with all finitary products such that every object is isomorphic to R nR^n for some natural number nn. A Lawvere theory is by default a finitary Lawvere theory, invoking the red herring principle. Note that a finitary Lawvere theory is the same thing as an β„΅ 0\aleph_0-ary Lawvere theory.

Size issues

Freyd and Street (1995) have shown that a category π’Ÿ\mathcal{D} is small if and only if both π’Ÿ\mathcal{D} and the functor category [π’Ÿ,Set][\mathcal{D},Set] are locally small. Analogously, it seems that a category π’Ÿ\mathcal{D} with products may be given the structure of a many-sorted infinitary Lawvere theory if and only if both π’Ÿ\mathcal{D} and Prod[π’Ÿ,Set]Prod[\mathcal{D},Set] (the category of product-preserving functors from π’Ÿ\mathcal{D} to SetSet, a full subcategory of [π’Ÿ,Set][\mathcal{D},Set]) are locally small. In both cases, the β€˜only if’ part is straightfoward, but we haven’t yet proved the β€˜if’ part.

See the n-Forum for more preliminary results.

Algebraic Categories

Conjecture

A multi-sorted infinitary Lawvere theory π’Ÿ\mathcal{D} defines a monadic category over Set by taking the functor category consisting of all product-preserving covariant functors from π’Ÿ\mathcal{D} in to SetSet.

Let us write this functor category as Prod[π’Ÿ,Set]Prod[\mathcal{D},Set] and start by showing that it is a locally small category.

Lemma

The category Prod[π’Ÿ,Set]Prod[\mathcal{D},Set] of product-preserving functors and natural transformations is locally small.

Proof

Let V 1,V 2:π’Ÿβ†’SetV_1, V_2 \colon \mathcal{D} \to Set be two product-preserving covariant functors. From the definition of a multi-sorted infinitary category we see that we may choose a set of sorts, say SS. Let D sβˆˆπ’ŸD_s \in \mathcal{D} be the image of s∈Ss \in S.

As SS is a set, the product

∏ s∈SSet(V 1(D s),V 2(D s)) \prod_{s \in S} Set(V_1(D_s), V_2(D_s))

is a set. We define a function [V 1,V 2]β†’βˆ s∈SSet(V 1(D s),V 2(D s))[V_1,V_2] \to \prod_{s \in S} Set(V_1(D_s), V_2(D_s)) by sending a natural transformation Ξ±:V 1β†’V 2\alpha \colon V_1 \to V_2 to the product of its values at each D sD_s. That is,

(1)α↦(Ξ± D s) s∈S. \alpha \mapsto \big(\alpha_{D_s}\big)_{s \in S}.

Let Dβˆˆπ’ŸD \in \mathcal{D} be an arbitrary object. From the definition of a multi-sorted infinitary Lawvere theory, there is an isomorphism

d:Dβ‰…βˆ s∈SD s X s d \colon D \cong \prod_{s \in S} D_s^{X_s}

for some sets X sX_s. For each s∈Ss \in S and x∈X sx \in X_s, there is a projection p s,x:∏ s∈SD s X sβ†’D sp_{s,x} \colon \prod_{s \in S} D_s^{X_s} \to D_s. As V 1V_1 and V 2V_2 are product-preserving, we have isomorphisms

β‰…βˆ s∈SV i(D s) X s \cong \prod_{s \in S} V_i(D_s)^{X_s}

commuting with the projections. Thus for each s∈Ss \in S and x∈X sx \in X_s, we have the following commutative diagram.

Layer 1 V 1 ( ∏ s ∈ S D s X s ) V_1\left( \prod_{s \in S} D_s^{X_s}\right) V 2 ( ∏ s ∈ S D s X s ) V_2\left( \prod_{s \in S} D_s^{X_s}\right) V 1 ( D s ) V_1\left(D_s\right) V 2 ( D s ) V_2\left(D_s\right) V 1 ( p s , x ) V_1(p_{s,x}) V 2 ( p s , x ) V_2(p_{s,x}) Ξ· D s \eta_{D_s} Ξ· ∏ s ∈ S D s X s \eta_{\prod_{s \in S} D_s^{X_s}} ∏ s ∈ S V 1 ( D s ) X s \prod_{s \in S} V_1(D_s)^{X_s} ∏ s ∈ S V 2 ( D s ) X s \prod_{s \in S} V_2(D_s)^{X_s} p s , x p_{s,x} p s , x p_{s,x} β‰… \cong β‰… \cong

Since this holds for all s∈Ss \in S and x∈X sx \in X_s, by the basic properties of products, there is a unique morphism ∏ s∈SV 1(D s) X sβ†’βˆ s∈SV 2(D s) X s\prod_{s \in S} V_1(D_s)^{X_s} \to \prod_{s \in S} V_2(D_s)^{X_s} making the diagram commute. This morphism is normally written ∏ s∈SΞ± D s X s\prod_{s \in S} \alpha_{D_s}^{X_s}. Thus under the isomorphism dd above, Ξ± D\alpha_D is taken to ∏ s∈SΞ± D s X s\prod_{s \in S} \alpha_{D_s}^{X_s}. As this holds for all Dβˆˆπ’ŸD \in \mathcal{D}, Ξ±\alpha is completely determined by the Ξ± D s\alpha_{D_s}, whence the map in (1) is injective.

Hence [V 1,V 2][V_1,V_2] is a subset of a set and thus a set.

Now that we have a locally small category, the next step is to show that the forgetful functor has a left adjoint. Firstly, we need to define this forgetful functor. As we are in the most general case, the forgetful functor does not go to SetSet but to SS-indexed tuples of sets (or an SS-graded set), where SS is a choice of set of sorts for π’Ÿ\mathcal{D}. To make things a little simpler, we assume that the sorting functor Sβ†’π’ŸS \to \mathcal{D} is injective on isomorphism classes so that if sβ‰ sβ€²s \ne s' in SS then D s≇D sβ€²D_s \ncong D_{s'} in π’Ÿ\mathcal{D}. With this assumption, the forgetful functor Prod[π’Ÿ,Set]β†’Set SProd[\mathcal{D},Set] \to Set^S is the evaluation functor:

V↦(s↦V(D s)),α↦(s↦α D s). V \mapsto \big(s \mapsto V(D_s)\big), \qquad \alpha \mapsto \big(s \mapsto \alpha_{D_s}\big).
Lemma

The forgetful functor Prod[π’Ÿ,Set]β†’Set SProd[\mathcal{D},Set] \to Set^S has a left adjoint. The left adjoint is given on objects by:

(s↦X s)β†¦π’Ÿ(∏ s∈SD s X s,βˆ’) \big(s \mapsto X_s\big) \mapsto \mathcal{D}\left(\prod_{s \in S} D_s^{X_s}, -\right)
Proof

To ease the notation, let us write UU for the forgetful (β€œunderlying set(s)”) functor and FF for the free functor.

To show the adjunction, we define the unit and counit natural transformations:

η:I→UF,ϡ:FU→I \eta \colon I \to U F, \qquad \epsilon \colon F U \to I

Let us consider η\eta. To define this, we evaluate it at an SS-graded set, XX, to get a morphism of graded sets, η X\eta_X. Such a morphism is itself a natural transformation so we evaluate again at s 0∈Ss_0 \in S. At this point, we have a function (in SetSet)

Ξ· X,s 0:X s 0β†’π’Ÿ(∏ s∈SD s X s,D s 0). \eta_{X,s_0} \colon X_{s_0} \to \mathcal{D}\left(\prod_{s \in S} D_s^{X_s}, D_{s_0}\right).

This is simple to describe: it is assignment to x∈X s 0x \in X_{s_0} of the projection onto the xxth D s 0D_{s_0}-factor:

∏ s∈SD s X sβ†’D s 0 X s 0β†’p xD s 0. \prod_{s \in S} D_s^{X_s} \to D_{s_0}^{X_{s_0}} \overset{p_x}{\to} D_{s_0}.

The counit, Ο΅\epsilon, is a little more complicated to describe. Let V:π’Ÿβ†’SetV \colon \mathcal{D} \to Set be a covariant product-preserving functor. Evaluated at VV, Ο΅ V\epsilon_V is a natural transformation

π’Ÿ(∏ s∈SD s V(D s),βˆ’)β†’V \mathcal{D}\left(\prod_{s \in S} D_s^{V(D_s)}, -\right) \to V

By the Yoneda lemma, such natural transformations are in bijective correspondence with elements of V(∏ s∈SD s V(D s))V\left(\prod_{s \in S} D_s^{V(D_s)}\right). As VV is product-preserving, there is a natural isomorphism:

V(∏ s∈SD s V(D s))β‰…βˆ s∈SV(D s) V(D s) V\left(\prod_{s \in S} D_s^{V(D_s)}\right) \cong \prod_{s \in S} V(D_s)^{V(D_s)}

Now for any set ZZ, there is an obvious element in Z ZZ^Z: the one that has a zz in the zzth place (which corresponds to the identity function Zβ†’ZZ \to Z). Taking the product of these gives an element in ∏ s∈SV(D s) V(D s)\prod_{s \in S} V(D_s)^{V(D_s)} which we use to define Ο΅ V\epsilon_V.

Let us now prove that these provide the desired adjunction. For one half, we need to consider the composition:

F→FηFUF→ϡFF F \overset{F \eta}{\to} F U F \overset{\epsilon F}{\to} F

Let us apply this to a graded set X=(s↦X s)X = (s \mapsto X_s). Then we are looking at a natural transformation from

π’Ÿ(∏ s∈SD s X s,βˆ’) \mathcal{D}\left(\prod_{s \in S} D_s^{X_s}, -\right)

to itself. By the standard Yoneda argument, it is sufficient to look at the induced function on

π’Ÿ(∏ s∈SD s X s,∏ s∈SD s X s) \mathcal{D}\left(\prod_{s \in S} D_s^{X_s}, \prod_{s \in S} D_s^{X_s}\right)

and in particular at the image of the identity therein.

The first part comes from FΞ·F\eta at F(X)F(X). For each s 0∈Ss_0 \in S, we have a function Ξ· X,s 0:X s 0β†’π’Ÿ(∏ s∈SD s X s,D s 0)\eta_{X,s_0} \colon X_{s_0} \to \mathcal{D}\left(\prod_{s \in S} D_s^{X_s}, D_{s_0}\right) and thus a morphism

(2)∏ s∈SD s π’Ÿ(∏ sβ€²βˆˆSD sβ€² X sβ€²,D s)β†’βˆ s∈SD s X s \prod_{s \in S} D_s^{\mathcal{D}\left(\prod_{s' \in S} D_{s'}^{X_{s'}},D_s\right)} \to \prod_{s \in S} D_s^{X_s}

What this does is the following: it sends component corresponding to the (s,x)(s,x)th projection to the xxth component and all other components are forgotten. Thus we have a morphism:

π’Ÿ(∏ s∈SD s X s,∏ s∈SD s X s)β†’π’Ÿ(∏ s∈SD s π’Ÿ(∏ sβ€²βˆˆSD sβ€² X sβ€²,D s),∏ s∈SD s X s) \mathcal{D}\left( \prod_{s \in S} D_s^{X_s}, \prod_{s \in S} D_s^{X_s}\right) \to \mathcal{D}\left( \prod_{s \in S} D_s^{\mathcal{D}\left(\prod_{s' \in S} D_{s'}^{X_{s'}},D_s\right)}, \prod_{s \in S} D_s^{X_s}\right)

Under this, the identity morphism goes to the projection morphism described just above.

Now we apply Ο΅F\epsilon F to get a morphism:

π’Ÿ(∏ s∈SD s π’Ÿ(∏ sβ€²βˆˆSD sβ€² X sβ€²,D s),∏ s∈SD s X s)β†’π’Ÿ(∏ s∈SD s X s,∏ s∈SD s X s) \mathcal{D}\left( \prod_{s \in S} D_s^{\mathcal{D}\left(\prod_{s' \in S} D_{s'}^{X_{s'}},D_s\right)}, \prod_{s \in S} D_s^{X_s}\right) \to \mathcal{D}\left( \prod_{s \in S} D_s^{X_s}, \prod_{s \in S} D_s^{X_s}\right)

To find this element, we consider the diagram:

π’Ÿ(∏ s∈SD s π’Ÿ(∏ sβ€²βˆˆSD sβ€² X sβ€²,D s),∏ s∈SD s π’Ÿ(∏ sβ€²βˆˆSD sβ€² X sβ€²,D s)) β†’Ο΅ π’Ÿ(∏ s∈SD s X s,∏ s∈SD s π’Ÿ(∏ sβ€²βˆˆSD sβ€² X sβ€²,D s)) β‰… ∏ s∈Sπ’Ÿ(∏ sβ€³βˆˆSD sβ€³ X sβ€³,D s) π’Ÿ(∏ sβ€²βˆˆSD sβ€² X sβ€²,D s) ↓ ↓ ↓ π’Ÿ(∏ s∈SD s π’Ÿ(∏ sβ€²βˆˆSD sβ€² X sβ€²,D s),∏ s∈SD s X s) β†’Ο΅ π’Ÿ(∏ s∈SD s X s,∏ s∈SD s X s) β‰… ∏ s∈Sπ’Ÿ(∏ sβ€³βˆˆSD sβ€³ X sβ€³,D s) X s \array{ \mathcal{D}\left( \prod_{s \in S} D_s^{\mathcal{D}\left(\prod_{s' \in S} D_{s'}^{X_{s'}},D_s\right)}, \prod_{s \in S} D_s^{\mathcal{D}\left(\prod_{s' \in S} D_{s'}^{X_{s'}},D_s\right)}\right) &\overset{\epsilon }{\to}& \mathcal{D}\left( \prod_{s \in S} D_s^{X_s}, \prod_{s \in S} D_s^{\mathcal{D}\left(\prod_{s' \in S} D_{s'}^{X_{s'}},D_s\right)}\right) & \cong & \prod_{s \in S} \mathcal{D}\left( \prod_{s'' \in S} D_{s''}^{X_{s''}}, D_s\right)^{\mathcal{D}\left(\prod_{s' \in S} D_{s'}^{X_{s'}},D_s\right)} \\ \downarrow & & \downarrow & & \downarrow \\ \mathcal{D}\left( \prod_{s \in S} D_s^{\mathcal{D}\left(\prod_{s' \in S} D_{s'}^{X_{s'}},D_s\right)}, \prod_{s \in S} D_s^{X_s}\right) &\overset{\epsilon }{\to}& \mathcal{D}\left( \prod_{s \in S} D_s^{X_s}, \prod_{s \in S} D_s^{X_s}\right) & \cong & \prod_{s \in S}\mathcal{D}\left( \prod_{s'' \in S} D_{s''}^{X_{s''}}, D_s\right)^{X_s} }

In this diagram, we have left off the subscript on Ο΅\epsilon for conciseness. The vertical morphism is that induced by the projection from (2). Since we want to have this projection itself in the lower-left, an obvious place to start is with the identity in the top-left. The right-hand square commutes since the vertical maps are projections. Starting with the identity in the top-left, we get the β€œYoneda element” corresponding to Ο΅\epsilon in the top-right. That element can be written (f) f(f)_f. The vertical map selects the p s,xp_{s,x}th element of the list and puts it in the (s,x)(s,x)th slot. As this is the projection p s,xp_{s,x}, when moving back to the lower-middle, we obtain the identity morphism as required.

Now let us turn to the other half. We need to consider the composition:

U→ηUUFU→UϡU U \overset{\eta U}{\to} U F U \overset{U \epsilon}{\to} U

So we need to start with a covariant product-preserving functor V:π’Ÿβ†’SetV \colon \mathcal{D} \to Set and apply UU. Then we are looking at a morphism of graded sets from

(s↦V(D s)) \big(s \mapsto V(D_s)\big)

to itself. So we pick s 0∈Ss_0 \in S and look at the function

V(D s 0)β†’π’Ÿ(∏ s∈SD s V(D s),D s 0)β†’V(D s 0). V(D_{s_0}) \to \mathcal{D}\left(\prod_{s \in S} D_s^{V(D_s)}, D_{s_0}\right) \to V(D_{s_0}).

We start with the function defined by the unit Ξ·\eta:

V(D s 0)β†’π’Ÿ(∏ s∈SD s V(D s),D s 0) V(D_{s_0}) \to \mathcal{D}\left(\prod_{s \in S} D_s^{V(D_s)}, D_{s_0}\right)

which sends v∈V(D s 0)v \in V(D_{s_0}) to the projection ∏ s∈SD s V(D s)β†’D s 0\prod_{s \in S} D_s^{V(D_s)} \to D_{s_0} which corresponds to the vvth factor of the s 0s_0th factor.

Now we apply Ο΅\epsilon. This gives us a natural transformation

π’Ÿ(∏ s∈SD s V(D s),βˆ’)β†’V(βˆ’) \mathcal{D}\left(\prod_{s \in S} D_s^{V(D_s)}, - \right) \to V(-)

which we evaluate at D s 0D_{s_0} (technically, which we evaluate at (s↦D s)(s \mapsto D_s) which we then evaluate at s 0s_0). This natural transformation is determined by an element of V(∏ s∈SD s V(D s))V\left(\prod_{s \in S} D_s^{V(D_s)}\right) and the element that we want is the image of that element under the function induced by the projection:

V(∏ s∈SD s V(D s))β†’V(p s 0,v)V(D s 0) V\left(\prod_{s \in S} D_s^{V(D_s)}\right) \overset{V(p_{s_0,v})}{\to} V(D_{s_0})

As VV is product-preserving, we can rearrange this to:

∏ s∈SV(D s) V(D s)β†’p s 0,vV(D s 0). \prod_{s \in S} V(D_s)^{V(D_s)} \overset{p_{s_0,v}}{\to} V(D_{s_0}).

The projection selects the (s 0,v)(s_0,v)th term of the element in question, and this element is, by definition, vv. Hence the induced function on V(D s 0)V(D_{s_0}) is the identity and the adjunction is shown.

Revised on January 1, 2012 05:21:07 by Mike Shulman (173.8.161.189)