Free-lattice functors weakly preserve epi-pullbacks

Abstract

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,\dots ,u_m\}=\{v_1,\dots ,v_n\},$ there is always an "ancestor term" $s(z_1,\dots ,z_r)$ such that $p(x_1,\dots ,x_m)$ and $q(y_1,\dots ,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.

References in corpus (2)

• The weakest nontrivial idempotent equations
• Free-algebra functors from a coalgebraic perspective