Functorial semantics and HSP type theorems (Q1319054)

A full subcategory \({\mathcal C}_ 0\) of the category \({\mathcal C}\) of models of a Kleisli category \({\mathcal K}\) with respect to a given factorisation system \({\mathcal E}/{\mathcal M}\) of a complete base category \({\mathcal B}\) is called HSP subcategory if \({\mathcal C}_ 0\) is closed under certain epimorphisms, under \({\mathcal M}\)-monics, and under products. The aim of the present paper is to give a characterization of such HSP subcategories. Unlike to Birkhoff's theory the result introduced here depends on how one defines HSP (what kind of subobjects are allowed, idea of satisfying a certain Horn clause). The author proves after some preliminaries about factorization systems, \({\mathcal B}\)-based sketches, and models some necessary conditions for the existence of a left adjoint to a certain functor \(U\colon Mod({\mathcal K})\to {\mathcal B}\), where \({\mathcal K}\) is at least a \({\mathcal B}\)-based sketch. The next result is that the Kleisli category \({\mathcal K}\) of a triple \({\mathfrak T}\) on \({\mathcal B}\) is isomorphic to the full image of the left adjoint \(F^{\mathfrak T}\colon {\mathcal B}\to {\mathcal B}^{\mathfrak T}\) to \(U^{\mathfrak T}\colon {\mathcal B}^{\mathfrak T}\to {\mathcal B}\) arising from \(U\) in a natural manner. Furthermore, the corresponding Eilenberg-Moore category is isomorphic to the category of models of \({\mathcal K}\). Using results of Linton the author shows that the underlying functor \(U\colon {\mathcal C}\to {\mathcal B}\) is tripleable and the triple is \({\mathfrak T}\), whenever \({\mathfrak T}\) is a triple on \({\mathcal B}\) with Kleisli category \({\mathcal K}\) and \({\mathcal C}\) as category of models of the resultant theory- type sketch. An HSP subcategory of \({\mathcal C}\) is tripleable if \(U\colon {\mathcal C}\to {\mathcal B}\) is tripleable. So one obtains the main HSP theorem: Let \(F\colon {\mathcal B}\to {\mathcal K}\) be the free functor into a Kleisli category with respect to a complete base category \({\mathcal B}\) with factorization system \({\mathcal E}/{\mathcal M}\) and let \({\mathcal H}\) be a class of Horn clauses with respect to \({\mathcal E}/{\mathcal M}\). Then \({\mathcal C}= Mod_{\mathcal H} ({\mathcal K})\) is an HSP subcategory of \({\mathcal C}\). The converse is in general not true, because it is possible that new Horn clauses emerge. Thus the possibility of iterating the Horn clauses must be allowed in any converse to the HSP theorem. Some instructive examples and information about related work conclude the paper.