Re: Equational correspondence and equational embedding

[Robin Houston <r.houston@cs.man.ac.uk>]

To my category-infected mind, it seems that what you really need
is a little category theory. :-)

I take it that your equations should define an equivalence relation?
(It seems strange to call them 'equations' if not.) If that's right,
then an "equational theory" is the same thing as an essentially-discrete
category, i.e. a category that is equivalent to a discrete one, and
an "equational correspondence" is an equivalence of categories.

With the definition of "equational embedding" you give, your
conjecture is false. For example, let the equational theories
S and T each have two terms x and y, with equations

 x =_S x     y =_S y    x =_S y
 x =_T x     y =_T y

We can define an equational embedding S -> T by mapping both
terms to x, and we can define an equational embedding T -> S
by mapping x to x and y to y, but there can be no equational
correspondence between S and T (since 1 != 2).

It would seem more natural, at least from a categorical point
of view, to define an equational embedding to be a full functor,
i.e. a function f: S -> T such that

   s =_S s'  iff  f(s) =_T f(s').

With that definition, your conjecture is true by the
Schröder-Bernstein theorem.

Robin