On the construction of free algebras for equational systems (Q1014644)

The authors define a general concept of an equational system \(\mathbb S\) on a category \({\mathcal C}\): it is given by two endofunctors \(\Sigma,\Gamma\) on \({\mathcal C}\) (the ``functorial signature'' and the ``functorial context'', respectively) and two functors \(L,R:\Sigma\)-\({\mathcal A}lg\to \Gamma\)-\({\mathcal A}lg\) (the ``functorial equations'') with \(U_\Gamma \circ L=U_\Gamma\circ R= U_\Sigma\) (where the \(U_\times\) are the appropriate forgetful functors). The category \(\mathbb S\)-\({\mathcal A}lg\) of \(\mathbb S\)-algebras is then defined as the equalizer of \(L\) and \(R\). All details are given to show how this (strictly) generalizes the concept of enriched algebraic theory. The main results give some colimit conditions on \({\mathcal C},\Sigma\) and \(\Gamma\) sufficient for the free algebras to exist and be contructible in a certain carefully described way. These conditions also imply that the forgetful functor \(\mathbb S\)-\({\mathcal A}lg\to {\mathcal C}\) is monadic and that \(\mathbb S\)-\({\mathcal A}lg\) is cocomplete. Applications to concepts recently defined in the theoretical computer science community are treated in details, for example the Pi-calculus, the \(\Sigma\)-monoids and the nominal equational logic.