Finitely Based Congruence Varieties
We show that for a large class of varieties of algebras, the equational theory of the congruence lattices of the members is not finitely based.
arXiv subjects
Publications and source records attributed to Ralph Freese.
We show that for a large class of varieties of algebras, the equational theory of the congruence lattices of the members is not finitely based.
Suppose $p(x,y,z)$ and $q(x,y,z)$ are terms. If there is a common "ancestor" term $s(z_{1},z_{2},z_{3},z_{4})$ specializing to $p$ and $q$ through identifying some variables \begin{align*} p(x,y,z) & \approx s(x,y,z,z)\\ q(x,y,z) & \approx s(x,x,y,z), \end{align*} then the equation \[ p(x,x,z)\approx q(x,z,z) \] is trivially obtained by syntactic unification of $s(x,y,z,z)$ with $s(x,x,y,z).$ In this note we show that for lattice terms, and more generally for terms of lattice-ordered algebras, the converse is true, too. Given terms $p,q,$ and an equation \begin{equation} p(u_{1},\ldots,u_{m})\approx q(v_{1},\ldots,v_{n})\label{eq:p_eq_q} \end{equation} where $\{u_{1},\ldots,u_{m}\}=\{v_{1},\ldots,v_{n}\},$ there is always an "ancestor term" $s(z_{1},\ldots,z_{r})$ such that $p(x_{1},\ldots,x_{m})$ and $q(y_{1},\ldots,y_{n})$ arise as substitution instances of $s,$ whose unification results in the original equation. In category theoretic terms the above proposition, when restricted to lattices, has a much more concise formulation: Free-lattice functors weakly preserves pullbacks of epis.
We consider the following practical question: given a finite algebra A in a finite language, can we efficiently decide whether the variety generated by A has a difference term? We answer this question (positively) in the idempotent case and then describe algorithms for constructing difference term operations.