Let be a small skeleton of the finitely presented models of an algebraic theory. The classifying topos assertion means that for every Grothendieck topos there is an equivalence
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 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 its component is
with all operations interpreted pointwise. Pulling 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: is the presheaf topos on , 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.

Articles by others on the same topic (0)

There are currently no matching articles.