= Solution
Let $\mathcal A=\mathbb T_{fp}$ be a small skeleton of the <finitely presented models of an algebraic theory>. The <classifying topos> assertion means that for every <Grothendieck topos> $\mathcal F$ there is an equivalence
$$
\boxed{\operatorname{Geom}(\mathcal F,[\mathcal A,\mathbf{Set}])\simeq\mathbb T\text{-}\operatorname{Mod}(\mathcal F),}
$$
natural under inverse image along <geometric morphisms>. On the left, morphisms are transformations between inverse image functors, and on the right they are model homomorphisms. A model in $\mathcal F$ interprets the sorts by objects, the operations by arrows, and the equations by equality of the resulting arrows. Finite products suffice for these algebraic operations.
The <generic model of an algebraic theory> is the tautological covariant functor: for each sort $S$ its component is
$$
U_S:\mathcal A\to\mathbf{Set},\qquad A\longmapsto A_S,
$$
with all operations interpreted pointwise. Pulling $U$ back by a <geometric morphism> gives its classified model. For a single-sorted theory, this is simply the underlying-set functor with its pointwise algebraic structure.
The orientation is important: $[\mathcal A,\mathbf{Set}]$ is the presheaf topos on $\mathcal A^{\mathrm{op}}$, and the generic model is covariant on finitely presented algebras. Such an algebra is a finite-generator, finite-relation presentation. In the algebraic syntactic category it corresponds to the formula imposing its relations, with arrows reversed. The finite-presentability/filtered-colimit description of algebraic models gives the above classifying equivalence; a detailed proof is not needed for this part.
Back to article page
