3
$\begingroup$

An essentially algebraic theoery, according to Adamek and Rosicky (second definition on nlab), consists of a many-sorted signature $\Sigma$ (consisting of function symbols on sorts $S$), a set $E$ of equations, a subset of total function symbols $\Sigma_t \subseteq \Sigma$, and a function $\mathrm{Def}$ that sends partial function symbols $f \in \Sigma \backslash \Sigma_t $ to sets of equations consisting of equations in variables of sorts that are in the source of $f$, and total function symbols.

It seems pretty clear to me how to construct a limit sketch from an essentially algebraic theory: an object for each sort, an object for each source of a function symbol along with a product diagram for that object, and equalizers defined by $\mathrm{Def}$ for each partial function, and the source of the partial functions are those equalizers.

Going the other way is not so clear to me. For theories with at most "one level" of equalizers, like categories, it's pretty clear, but I don't see a way of turning a theory with an operation that has source the equalizer of two functions whose source is an equalizer into an essentially algebraic theory. Specifically, consider the limit sketch we can get from

$f, g : A \to B$,

$h, k : \mathrm{Eq}(f,g) \to C$,

$p : \mathrm{Eq}(h,k) \to D$.

The issue is that $\mathrm{Def}$ equations can only be defined in terms of total functions, and here I want $\mathrm{Def}(p) = \{x:A \vdash f(x) = g(x),x:A \vdash h(x) = k(x) \} $ , but $h$ and $k$ are partial.

Is there a more direct way of getting this rather than taking the category of models of the sketch and then constructing the essentially algebraic theory out of that locally presentable category using their theorem 3.36? This is both difficult, and produces something that looks more like a classifying category (ie. the deductive closure of a theory) than a more presentation-like theory.

A similar question would be, in 3.37 Remark of Adamek and Rosicky, they say that these partial/total essentially algebraic theories are equivalent to well-ordered essentially algebraic theories where there is a well-ordering on the operations and operations are partially defined only in terms of operations that are lower in the well-ordering, by giving an equivalence with locally presentable categories. What then is that well-ordered essentially algebraic theory that you get from a partial/total essentially algebraic theory through this?

$\endgroup$

1 Answer 1

3
$\begingroup$

We'll add a new sort $E$ and force it to be isomorphic (by a specified isomorphism) to the equalizer of $f$ and $g$. Then we can replace $h$ and $k$ by total functions $E \to C$, and so $p$ will have domain of definition defined by equations between total functions.

To do this we just need to add $e : \mathrm{Eq}(f, g) \to E$ and $a : E \to A$ together with equations $f(a(x)) = g(a(x))$ (so that $a$ lands inside the equalizer), $e(a(x)) = x$, $a(e(x)) = x$.

The new limit sketch with objects $\{A, B, C, D, E\}$, generating morphisms $\{a : E \to A, f, g : A \to B, e : \mathrm{Eq}(f, g) \to E, h, k : E \to C, p : \mathrm{Eq}(h, k) \to D\}$, and equations as above is now of the form that can be directly converted to an essentially algebraic theory, and it has an category of models equivalent to that of the original limit sketch.

$\endgroup$

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .