Structure–Semantics Adjunction for Tractable FunctorsNatural bijection of the adjunctionFrom $G$ to $\Phi$From $\Phi$ to $G$Mutual inverses and naturalityThe counit and its isomorphism property – with concrete examplesExtracting the counitWhat $\hat{\varepsilon}_{\mathbb{T}}$ does concretelyA concrete example: the theory of groupsWhy this shows the counit is an isomorphismConsequences: full faithfulness and reflective subcategorySummary

 

Structure–Semantics Adjunction for Tractable Functors

Consider the full subcategory of $\mathsf{Cat}/\mathsf{Set}$$\mathsf{Cat}/\mathsf{Set}$ consisting of tractable functors, i.e. those $U:\mathcal{C}\to \mathsf{Set}$$U:\mathcal{C}\to\mathsf{Set}$ such that for all $m,n\in \mathbb{N}$$m,n\in\mathbb{N}$, $\mathsf{Nat}(U^m,U^n)$$\mathsf{Nat}(U^m,U^n)$ is a set.
Denote this category by

$$\mathsf{Tract}(\mathsf{Cat}/\mathsf{Set})$$

Let $\mathbb{T}$$\mathbb{T}$ be an algebraic theory. We have the forgetful functor $U_{\mathbb{T}}:\mathsf{Mod}(\mathbb{T})\to \mathsf{Set}$$U_{\mathbb{T}}:\mathsf{Mod}(\mathbb{T})\to\mathsf{Set}$ defined by $U_{\mathbb{T}}(A)=A(1)$$U_{\mathbb{T}}(A)=A(1)$.
Hence we obtain a functor

$$\mathsf{Alg}(-,\mathsf{Set}):{\mathsf{Theory}}^{\mathrm{op}}⟶\mathsf{Tract}(\mathsf{Cat}/\mathsf{Set}),\mathbb{T}⟼(\mathsf{Mod}(\mathbb{T}),U_{\mathbb{T}}).$$

This functor admits a left adjoint, called Struct. Concretely, given a tractable functor $U:\mathcal{C}\to \mathsf{Set}$$U:\mathcal{C}\to\mathsf{Set}$ we construct a Lawvere theory ${\mathbb{T}}_U$$\mathbb{T}_U$:

• objects are the natural numbers $n\in \mathbb{N}$$n\in\mathbb{N}$ (representing $U^n$$U^n$);

• morphisms $m\to n$$m\to n$ are the natural transformations $\mathsf{Nat}(U^m,U^n)$$\mathsf{Nat}(U^m,U^n)$.

Let $U:\mathcal{C}\to \mathsf{Set}$$U:\mathcal{C}\to\mathsf{Set}$ and $V:\mathcal{D}\to \mathsf{Set}$$V:\mathcal{D}\to\mathsf{Set}$ be two tractable functors. A morphism $(\mathcal{C},U)\to (\mathcal{D},V)$$(\mathcal{C},U)\to(\mathcal{D},V)$ in $\mathsf{Tract}$$\mathsf{Tract}$ is a functor $F:\mathcal{C}\to \mathcal{D}$$F:\mathcal{C}\to\mathcal{D}$ making the triangle commute:

Now we define $\mathsf{Struct}$$\mathsf{Struct}$ on morphisms. Given $F:(\mathcal{C},U)\to (\mathcal{D},V)$$F:(\mathcal{C},U)\to(\mathcal{D},V)$, we define a theory morphism

$$\mathsf{Struct}(F):{\mathbb{T}}_V⟶{\mathbb{T}}_U.$$

• On objects: $\mathsf{Struct}(F)(n)=n$$\mathsf{Struct}(F)(n)=n$.

• On morphisms: take $\alpha \in {\mathbb{T}}_V(m,n)=\mathsf{Nat}(V^m,V^n)$$\alpha\in\mathbb{T}_V(m,n)=\mathsf{Nat}(V^m,V^n)$. For each $X\in \mathcal{C}$$X\in\mathcal{C}$, $F(X)\in \mathcal{D}$$F(X)\in\mathcal{D}$, we have a component ${\alpha }_{F(X)}:V^m(F(X))\to V^n(F(X))$$\alpha_{F(X)}:V^m(F(X))\to V^n(F(X))$.
  Because $V(F(X))=U(X)$$V(F(X))=U(X)$, this is a function $U(X{)}^m\to U(X{)}^n$$U(X)^m\to U(X)^n$. Naturality in $X$$X$ follows from the naturality of $\alpha$$\alpha$ and functoriality of $F$$F$; therefore we obtain a natural transformation $\mathsf{Struct}(F)(\alpha )\in \mathsf{Nat}(U^m,U^n)$$\mathsf{Struct}(F)(\alpha)\in\mathsf{Nat}(U^m,U^n)$ with components

  $$(\mathsf{Struct}(F)(\alpha ){)}_X={\alpha }_{F(X)}.$$

---

Natural bijection of the adjunction

We need to establish a natural isomorphism

$${\mathrm{\Theta }}_{U,\mathbb{T}}:\mathsf{Tract}((\mathcal{C},U),\mathsf{Alg}(\mathbb{T}))\stackrel{\cong }{\to }{\mathsf{Theory}}^{\mathrm{op}}({\mathbb{T}}_U,\mathbb{T}),$$

or equivalently

$$\mathrm{\Theta }:\mathsf{Tract}((\mathcal{C},U),(\mathsf{Mod}(\mathbb{T}),U_{\mathbb{T}}))\stackrel{\cong }{\to }\mathsf{Theory}(\mathbb{T},{\mathbb{T}}_U).$$

• The left‑hand side consists of functors $G:\mathcal{C}\to \mathsf{Mod}(\mathbb{T})$$G:\mathcal{C}\to\mathsf{Mod}(\mathbb{T})$ making the diagram

  $$\begin{array}{ccc}\mathcal{C}& \stackrel{G}{⟶}& \mathsf{Mod}(\mathbb{T})\\ & {}_U\searrow & {\downarrow }_{U_{\mathbb{T}}}\\ & & \mathsf{Set}\end{array}$$

  commute.

• The right‑hand side consists of product‑preserving functors $\mathrm{\Phi }:\mathbb{T}\to {\mathbb{T}}_U$$\Phi:\mathbb{T}\to\mathbb{T}_U$ that are the identity on objects.

From $G$$G$ to $\mathrm{\Phi }$$\Phi$

Given $G$$G$ with $U_{\mathbb{T}}\circ G=U$$U_{\mathbb{T}}\circ G = U$. For a morphism $\alpha :m\to n$$\alpha:m\to n$ in $\mathbb{T}$$\mathbb{T}$ we must produce a natural transformation $\mathrm{\Phi }(\alpha )\in \mathsf{Nat}(U^m,U^n)$$\Phi(\alpha)\in\mathsf{Nat}(U^m,U^n)$. For any $X\in \mathcal{C}$$X\in\mathcal{C}$, $G(X)$$G(X)$ is a model $G(X):\mathbb{T}\to \mathsf{Set}$$G(X):\mathbb{T}\to\mathsf{Set}$, and

$$G(X)(m)\cong G(X)(1{)}^m=(U_{\mathbb{T}}(G(X)){)}^m=U(X{)}^m.$$

Hence we define

$$(\mathrm{\Phi }(\alpha ){)}_X:=G(X)(\alpha ):U(X{)}^m⟶U(X{)}^n.$$

For a morphism $f:X\to Y$$f:X\to Y$ in $\mathcal{C}$$\mathcal{C}$, $G(f)$$G(f)$ is a model homomorphism, which implies

$$G(X)(\alpha )\circ G(f)(1{)}^m=G(f)(1{)}^n\circ G(Y)(\alpha ),$$

and $G(f)(1)=U(f)$$G(f)(1)=U(f)$. This is exactly the naturality condition required, so $\mathrm{\Phi }(\alpha )$$\Phi(\alpha)$ is indeed natural.
Because each $G(X)$$G(X)$ preserves products, the product structure transports pointwise to the pairings, making $\mathrm{\Phi }$$\Phi$ a morphism of theories.

From $\mathrm{\Phi }$$\Phi$ to $G$$G$

Given a theory morphism $\mathrm{\Phi }:\mathbb{T}\to {\mathbb{T}}_U$$\Phi:\mathbb{T}\to\mathbb{T}_U$. For each $X\in \mathcal{C}$$X\in\mathcal{C}$ we construct a model $G(X):\mathbb{T}\to \mathsf{Set}$$G(X):\mathbb{T}\to\mathsf{Set}$:

• On objects: $G(X)(n):=U(X{)}^n$$G(X)(n) := U(X)^n$ (formally $G(X)(n)=(\mathrm{\Phi }(n))(X)$$G(X)(n)=(\Phi(n))(X)$, but $\mathrm{\Phi }(n)=n$$\Phi(n)=n$).

• On morphisms: for $\alpha :m\to n$$\alpha:m\to n$ in $\mathbb{T}$$\mathbb{T}$, set $G(X)(\alpha ):=\mathrm{\Phi }(\alpha {)}_X:U(X{)}^m\to U(X{)}^n$$G(X)(\alpha) := \Phi(\alpha)_X : U(X)^m \to U(X)^n$.

Since $\mathrm{\Phi }$$\Phi$ preserves products, $G(X)$$G(X)$ preserves products.
For a morphism $f:X\to Y$$f:X\to Y$ in $\mathcal{C}$$\mathcal{C}$, define a natural transformation $G(f):G(X)\Rightarrow G(Y)$$G(f):G(X)\Rightarrow G(Y)$ with components

$$G(f{)}_n:=U(f{)}^n:U(X{)}^n\to U(Y{)}^n.$$

Naturality of $\mathrm{\Phi }(\alpha )$$\Phi(\alpha)$ guarantees the model homomorphism condition, and clearly $U_{\mathbb{T}}(G(X))=G(X)(1)=U(X)$$U_{\mathbb{T}}(G(X)) = G(X)(1) = U(X)$, so $U_{\mathbb{T}}\circ G=U$$U_{\mathbb{T}}\circ G = U$.

Mutual inverses and naturality

The two constructions are mutually inverse: starting from $G$$G$, going to $\mathrm{\Phi }$$\Phi$ and back to $G^{\prime }$$G'$ gives $G^{\prime }(X)(\alpha )=\mathrm{\Phi }(\alpha {)}_X=G(X)(\alpha )$$G'(X)(\alpha)=\Phi(\alpha)_X=G(X)(\alpha)$, exactly the same functor; the reverse direction works analogously. Naturality in $\mathcal{C}$$\mathcal{C}$ and $\mathbb{T}$$\mathbb{T}$ follows directly from the ingredients, hence the bijection is natural.

Indeed, this adjunction tells us that given a model of an algebraic theory, we can reconstruct the theory via its forgetful functor.
If $\mathbb{T}$$\mathbb{T}$ is a Lawvere theory and $U:\mathsf{Mod}(\mathbb{T})\to \mathsf{Set}$$U:\mathsf{Mod}(\mathbb{T})\to\mathsf{Set}$ its forgetful functor, then

$$\mathbb{T}\cong {\mathbb{T}}_U.$$

---

The counit and its isomorphism property – with concrete examples

We now give a detailed, concrete account of the counit of the structure–semantics adjunction, showing why it is an isomorphism. We work entirely within the framework of Lawvere theories and tractable functors, but illustrate each step with familiar algebraic theories such as groups.

Extracting the counit

Take $(\mathcal{C},U)=\mathsf{Alg}(\mathbb{T})=(\mathsf{Mod}(\mathbb{T}),U_{\mathbb{T}})$$(\mathcal{C},U) = \mathsf{Alg}(\mathbb{T}) = (\mathsf{Mod}(\mathbb{T}), U_{\mathbb{T}})$.
On the left side of $\mathrm{\Theta }$$\Theta$ we have the identity morphism

$${\mathrm{id}}_{\mathsf{Alg}(\mathbb{T})}\in \mathsf{Tract}(\mathsf{Alg}(\mathbb{T}),\mathsf{Alg}(\mathbb{T})).$$

The inverse of $\mathrm{\Theta }$$\Theta$ sends this identity to an arrow in ${\mathbf{Theory}}^{\mathrm{op}}$$\mathbf{Theory}^{\mathrm{op}}$

$${\epsilon }_{\mathbb{T}}:{\mathbb{T}}_{U_{\mathbb{T}}}⟶\mathbb{T}(\text{in }{\mathbf{Theory}}^{\mathrm{op}}),$$

which, after reversing the direction, corresponds to an ordinary theory morphism

$${\hat{\epsilon }}_{\mathbb{T}}:\mathbb{T}⟶{\mathbb{T}}_{U_{\mathbb{T}}}.$$

What ${\hat{\epsilon }}_{\mathbb{T}}$$\hat{\varepsilon}_{\mathbb{T}}$ does concretely

• On objects: ${\hat{\epsilon }}_{\mathbb{T}}(n)=n$$\hat{\varepsilon}_{\mathbb{T}}(n) = n$ (identity on natural numbers).

• On morphisms: For $\alpha :m\to n$$\alpha:m\to n$ in $\mathbb{T}$$\mathbb{T}$, the image ${\hat{\epsilon }}_{\mathbb{T}}(\alpha )$$\hat{\varepsilon}_{\mathbb{T}}(\alpha)$ is a natural transformation $U_{\mathbb{T}}^m\Rightarrow U_{\mathbb{T}}^n$$U_{\mathbb{T}}^m \Rightarrow U_{\mathbb{T}}^n$ whose component at a model $M\in \mathsf{Mod}(\mathbb{T})$$M\in\mathsf{Mod}(\mathbb{T})$ is simply

  $$({\hat{\epsilon }}_{\mathbb{T}}(\alpha ){)}_M=M(\alpha ):M(m)\to M(n).$$

  (Recall that $M$$M$ preserves products, so $M(m)\cong M(1{)}^m=U_{\mathbb{T}}(M{)}^m$$M(m)\cong M(1)^m = U_{\mathbb{T}}(M)^m$.)

Thus ${\hat{\epsilon }}_{\mathbb{T}}$$\hat{\varepsilon}_{\mathbb{T}}$ is the evaluation map that “interprets” each abstract operation as a concrete family of set‑functions, uniformly across all models.

A concrete example: the theory of groups

Let $\mathbb{T}={\mathbb{T}}_{\mathsf{Grp}}$$\mathbb{T} = \mathbb{T}_{\mathsf{Grp}}$ be the Lawvere theory of groups. Its category of models is $\mathsf{Grp}$$\mathsf{Grp}$, and $U_{\mathbb{T}}:\mathsf{Grp}\to \mathsf{Set}$$U_{\mathbb{T}}:\mathsf{Grp}\to\mathsf{Set}$ sends a group to its underlying set.

The theory extracted from $(\mathsf{Grp},U_{\mathbb{T}})$$(\mathsf{Grp}, U_{\mathbb{T}})$.
The theory ${\mathbb{T}}_{U_{\mathbb{T}}}$$\mathbb{T}_{U_{\mathbb{T}}}$ has objects $\mathbb{N}$$\mathbb{N}$ and morphisms ${\mathbb{T}}_{U_{\mathbb{T}}}(m,n)=\mathsf{Nat}(U_{\mathbb{T}}^m,U_{\mathbb{T}}^n)$$\mathbb{T}_{U_{\mathbb{T}}}(m,n) = \mathsf{Nat}(U_{\mathbb{T}}^m, U_{\mathbb{T}}^n)$.
A natural transformation $U_{\mathbb{T}}^m\Rightarrow U_{\mathbb{T}}^n$$U_{\mathbb{T}}^m \Rightarrow U_{\mathbb{T}}^n$ gives, for every group $G$$G$, a function $G^m\to G^n$$G^m \to G^n$ that is natural with respect to group homomorphisms. For example:

• $m=1,n=1$$m=1, n=1$: natural maps $G\to G$$G\to G$ are precisely the group‑theoretic terms in one variable ($x$$x$, $x^{-1}$$x^{-1}$, $e$$e$, $x^2$$x^2$, …) – exactly ${\mathbb{T}}_{\mathsf{Grp}}(1,1)$$\mathbb{T}_{\mathsf{Grp}}(1,1)$.

• $m=2,n=1$$m=2, n=1$: natural maps $G\times G\to G$$G\times G\to G$ correspond to binary group terms ($xy$$xy$, $yx$$yx$, $x^{-1}y$$x^{-1}y$, projections, constants, …) – exactly ${\mathbb{T}}_{\mathsf{Grp}}(2,1)$$\mathbb{T}_{\mathsf{Grp}}(2,1)$.

Thus ${\mathbb{T}}_{U_{\mathbb{T}}}$$\mathbb{T}_{U_{\mathbb{T}}}$ is literally the same as the original theory of groups.

The evaluation map in the group case.
The theory morphism ${\hat{\epsilon }}_{{\mathbb{T}}_{\mathsf{Grp}}}:{\mathbb{T}}_{\mathsf{Grp}}\to {\mathbb{T}}_{U_{\mathbb{T}}}$$\hat{\varepsilon}_{\mathbb{T}_{\mathsf{Grp}}} : \mathbb{T}_{\mathsf{Grp}} \to \mathbb{T}_{U_{\mathbb{T}}}$ sends

• the abstract multiplication $\mu :2\to 1$$\mu:2\to 1$ to the natural transformation with components ${\mu }_G:G\times G\to G$$\mu_G:G\times G\to G$, $(x,y)\mapsto xy$$(x,y)\mapsto xy$;

• the abstract inverse $i:1\to 1$$i:1\to 1$ to the natural transformation with components $i_G:G\to G$$i_G:G\to G$, $x\mapsto x^{-1}$$x\mapsto x^{-1}$;

• the abstract unit $e:0\to 1$$e:0\to 1$ to the natural transformation picking the identity element in each group.

• Injectivity: if two abstract terms behave identically on all groups, they must be the same term (test on free groups).

• Surjectivity: any natural family $G^m\to G^n$$G^m \to G^n$ compatible with all homomorphisms is given by a term – a classical result of universal algebra.

Hence ${\hat{\epsilon }}_{{\mathbb{T}}_{\mathsf{Grp}}}$$\hat{\varepsilon}_{\mathbb{T}_{\mathsf{Grp}}}$ is an isomorphism in $\mathbf{Theory}$$\mathbf{Theory}$.

Why this shows the counit is an isomorphism

By definition of the adjunction, the counit ${\epsilon }_{\mathbb{T}}$$\varepsilon_{\mathbb{T}}$ in ${\mathbf{Theory}}^{\mathrm{op}}$$\mathbf{Theory}^{\mathrm{op}}$ corresponds to ${\hat{\epsilon }}_{\mathbb{T}}^{-1}$$\hat{\varepsilon}_{\mathbb{T}}^{-1}$. Because ${\hat{\epsilon }}_{\mathbb{T}}$$\hat{\varepsilon}_{\mathbb{T}}$ is an isomorphism of theories, ${\epsilon }_{\mathbb{T}}$$\varepsilon_{\mathbb{T}}$ is an isomorphism in ${\mathbf{Theory}}^{\mathrm{op}}$$\mathbf{Theory}^{\mathrm{op}}$.
Thus:

$$\boxed{{\displaystyle {\epsilon }_{\mathbb{T}}\text{ is an isomorphism for every Lawvere theory }\mathbb{T}}}$$

Consequences: full faithfulness and reflective subcategory

Since the counit is an isomorphism, the right adjoint $\mathsf{Alg}$$\mathsf{Alg}$ is fully faithful.
Its essential image consists exactly of those tractable functors that are (up to isomorphism) of the form $(\mathsf{Mod}(\mathbb{T}),U_{\mathbb{T}})$$(\mathsf{Mod}(\mathbb{T}), U_{\mathbb{T}})$.

A fully faithful right adjoint has its image as a reflective subcategory; therefore the image of $\mathsf{Alg}$$\mathsf{Alg}$ is reflective, with reflector $\mathsf{Struct}$$\mathsf{Struct}$. The unit

$${\eta }_{(\mathcal{C},U)}:(\mathcal{C},U)⟶(\mathsf{Mod}({\mathbb{T}}_U),U_{{\mathbb{T}}_U})$$

embeds any concrete category $(\mathcal{C},U)$$(\mathcal{C},U)$ into the models of the theory it generates. For the special case where $(\mathcal{C},U)$$(\mathcal{C},U)$ is already a model category with its forgetful functor, the unit is an inverse to the counit, hence an equivalence.

Summary

The evaluation map ${\hat{\epsilon }}_{\mathbb{T}}$$\hat{\varepsilon}_{\mathbb{T}}$ sends each abstract operation to the concrete natural family it defines on models.
Functorial semantics tells us this map is always bijective, so

$$\mathbb{T}\cong {\mathbb{T}}_{U_{\mathbb{T}}}$$

via the counit. Consequently, the theory is completely encoded in its category of models together with the forgetful functor, and the structure–semantics adjunction gives a precise duality between syntax (the theory) and semantics (the concrete category of models).