Equivalence between models of a sketch and models of a theory

75 Views Asked by At

Barr and Wells page 131 states in the context of linear sketches that:

$M_0$ induces an equivalence of categories:

$Mod(\mathcal{S}, Set) \leftrightarrow Func(Th(\mathcal{S}), Set)$

between the models of $\mathcal{S}$ in $Set$ and the models of its theory.

I'm first confused by the use of $Set$ instead of a general category $\mathcal{C}$.

Is this a standard result in the literature so that I can look the equivalence? It is not very evident what the functors relating the two are.

Update

For the action of the functors on morphisms, I have been suggested to try to do the following. Given that $F: \mathcal{C} \to \mathcal{D}, G: \mathcal{D} \to \mathcal{C}$ are functors which are inverse of each other on objects, track a morphism along the chain:

$Hom(FC,D) \to Hom(GFC, GD) = Hom(C, GD) \to Hom(FC,FGD) = Hom(FC,D)$

to show that after the chain I get the same morphism, this should show that the application of $G$ is injective and of $F$ is surjective and then I could exchange the role of $F$ and $G$.

1

There are 1 best solutions below

3
On BEST ANSWER

Yes, this is a standard result in the literature, but the "theory of a linear sketch" is perhaps more commonly known as the "free category presented by generators and relations".

A linear sketch consists of a graph (a collection $V$ of vertices and a collection $E$ of directed edges) and a collection $D$ of diagrams in the graph. You should think of the edges in $E$ as generators and the diagrams in $D$ as relations. The construction of the "theory" turns the linear sketch into a category by adding identities and composing the generators, and imposing commutativity of the diagrams in $D$.

You're correct that we then get an equivalence of categories $$\text{Mod}(\mathcal{S},\mathcal{C}) \equiv \text{Func}(\text{Th}(\mathcal{S}),\mathcal{C})$$ for any category $\mathcal{C}$, not just $\mathsf{Set}$. I think Barr and Wells restrict to $\mathsf{Set}$ because it's traditional when talking about "models of a theory" to focus on models in the category of sets.

The description in Barr and Wells is certainly sketchy, but it seems to me that they do describe what the functors involved in the equivalence are. The point is that the sketch $\mathcal{S}$ "sits inside" the category $\text{Th}(\mathcal{S})$ and generates it. So on one hand, if we have a functor $F\colon \text{Th}(\mathcal{S})\to \mathcal{C}$, then $F$ restricts to a map from $\mathcal{S}$ to $U(\mathcal{C})$, giving a model of $\mathcal{S}$ in $\mathcal{C}$. And on the other hand, if we have a map from $\mathcal{S}$ to $U(\mathcal{C})$, giving a model of $\mathcal{S}$ in $\mathcal{C}$, then this map extends uniquely to a functor $\text{Th}(\mathcal{S})\to \mathcal{C}$, since every arrow in $\text{Th}(\mathcal{S})$ is a composition of arrows from $\mathcal{S}$, which must get mapped to the corresponding composition in $\mathcal{C}$.


In the comments, you asked about how the functors involved in the equivalence act on morphisms. Like I did above, I'll try to give you the basic idea, but I'll leave it to you to fill in the details.

Suppose we have a natural transformation $\eta\colon F\to G$, where $F,G\in \text{Func}(\text{Th}(\mathcal{S}),\mathcal{C})$. We want to turn $\eta$ into a morphism between the models $F|_\mathcal{S}\colon \mathcal{S}\to U(\mathcal{C})$ and $G|_\mathcal{S}\colon \mathcal{S}\to U(\mathcal{C})$. Well, a morphism of models is just a natural transformation $F|_\mathcal{S}\to G|_\mathcal{S}$, and we can take $\eta|_{\mathcal{S}}$. More explicitly, for every object $X$ in $\mathcal{S}$, there is a component $\eta_X\colon F(X)\to G(X)$ for $X$, and for each arrow $f\colon X\to Y$ in $\mathcal{S}$, we have the commutative square $G(f)\circ \eta_X = \eta_Y\circ F(f)$, since $\eta$ is a natural transformation.

In the other direction, suppose we have a morphism $\theta\colon M\to N$, where $M$ and $N$ are models of $\mathcal{S}$ in $\mathcal{C}$. Then $M$ and $N$ extend to functors $\overline{M},\overline{N}\colon \text{Th}(\mathcal{S})\to\mathcal{C}$. By definition of morphism of models, for every object $X$ in $\mathcal{S}$, we have an arrow $\theta_X\colon \overline{M}(X) = M(X)\to N(X) = \overline{N}(X)$. The sketch $\mathcal{S}$ and the category $\text{Th}(\mathcal{S})$ have the same objects, so it remains to show that the components $\theta_X$ cohere to a natural transformation $\overline{M}\to \overline{N}$. Each arrow $f\colon X\to Y$ in $\text{Th}(\mathcal{S})$ is an identity or a composition of arrows in $\mathcal{S}$, so applying naturality of $\theta$ with respect to each of these arrows in $\mathcal{S}$, we obtain naturality of $\theta$ with respect to $f$.