laws and equations

laws and equations

[Enrico Vitale]

Dear Colleagues,

Recently, Bill Lawvere proposed parallel pairs of morphisms
in an algebraic theory as the categorical concept of "equational
law". We have just observed that this is, for many sorted theories,
the first definition that makes sense! For example, the following
variant
of Birkhoff's Variety Theorem holds for many-sorted algebras:
a full subcategory is equationally presentable (in Bill's sense)
iff it is closed under products, subobjects, regular quotients and
directed unions. If equation is "traditionally" understood as
a pair of terms (elements of a free algebra of the given signature)
of the same sort, then Birkhoff's theorem is not true:

Example. Consider algebras on two sorts (say, a,b) with no
operations - that is, consider the category Set x Set.
Take the full subcategory V of all objects (A,B) such
that either A is empty or B has at most 1 element. This is an
HSP subcategory of Set x Set, but there does not exist any
equation that only works with one of the sorts such
that all the objects of V satisfy it. But in the theory which is a free
completion of the discrete category {a,b} under finite products
the parallel pair of projections
         p_2, p_3: a x b x b -> b
specifies V.

If, on the other hand, equations are understood as pairs of terms
together with a many-sorted set of variables (encoding the universal
quantification), the following example demonstrates that
we are beyond the realm of finitary logic:

Example. Consider algebras on infinitely many sorts with
no operations. The full subcategory of all objects which are
either subobjects of the terminal object, or have all but finitely
many sorts empty, is an HSP class. But it is not closed under
directed unions, and thus cannot be described in finitary logic.


Best regards
Jiri Adamek and Enrico Vitale