Reference request: finitely presented algebras classify an equational theory

Question

The title pretty much says it all: I've read somewhere of the fact that algebras (i.e. models in $\mathbf{Set}$) for an equational theory can be seen as lex functors from the opposite category of finitely presented algebras to $\mathbf{Set}$. However, I wasn't able to find any proof of this assertion anywhere.

Answer 1

What you want is a corollary to Gabriel-Ulmer duality. For example, your result is Theorem 10 (presented without much proof) in Lack's and Powers' Gabriel-Ulmer Duality and Lawvere Theories Enriched over a General Base. Algebraic Theories of Quasivarieties by Adámek and Porst gives a detailed proof for Gabriel-Ulmer duality. However, that itself requires knowing about locally finitely presentable categories and that finitely presentable objects in a category of models of an algebraic theory are, indeed, finitely presented algebras.

Basically, Gabriel-Ulmer duality states that $\mathbf{Lex}^{op}\simeq\mathbf{LFP}$ where this is a biequivalence of 2-categories. $\mathbf{Lex}$ is the 2-category of small finitely complete categories, finite limit preserving functors, and natural transformations, and $\mathbf{LFP}$ is the 2-category of locally finitely presentable categories, filtered colimit preserving right adjoint functors, and natural transformations. One direction of the biequivalence is via the embedding $\mathbf{Lex}(-,\mathbf{Set}) : \mathbf{Lex}^{op}\to\mathbf{LFP}$.

A locally finitely presentable category is one that has colimits and is generated by a set of finitely presentable objects via filtered colimits, i.e. every object is a filtered colimit of finitely presentable objects. The skeleton of the full subcategory of finitely presentable objects is a small(!) finitely cocomplete category, so its opposite is finitely complete. This is (part of) the part of the biequivalence going from $\mathbf{LFP}\to\mathbf{Lex}^{op}$. Let $\mathcal{C}$ be a locally finitely presentable category, and call $\mathcal{C}_{fp}$ the skeleton of the full subcategory of finitely presentable objects described above. Then $\mathcal{C}_{fp}^{op}\in\mathbf{Lex}$ and $\mathcal{C}\simeq\mathbf{Lex}(\mathcal{C}_{fp}^{op},\mathbf{Set})$ which is the result you want (given that finitely presentable objects live up to their name in categories of models of an algebraic theory).