Discrete equational theories
Jiří Rosický
TL;DR
This work extends discrete equational theories to a general, locally $\lambda$-presentable symmetric monoidal closed category $\mathcal{V}$ by defining discrete theories whose arities are induced from a base $X_0$. It proves that such discrete theories correspond precisely to $\lambda$-ary enriched monads on $\mathcal{V}$ preserving surjections, enabling Birkhoff-type theorems for the associated algebra categories; under mild hypotheses the surjections form the left side of a factorization system, connecting to known results in metric spaces and broadening them to other enriched contexts. The main contributions include a comprehensive equivalence framework for discrete theories across Pos and Met, a mu-Birkhoff subcategory characterization, and a detailed analysis showing how these results specialize to and extend prior work (e.g., MPP) while noting limitations via Appendix results. Overall, the paper unifies and extends universal algebra with enriched and quantitative perspectives, providing new tools for reasoning about theories and their algebras in diverse categorical settings.
Abstract
We introduce discrete equational theories where operations are induced by those having discrete arities. We characterize the corresponding monads as monads preserving surjections. Using it, we prove Birkhoff type theorems for categories of algebras of discrete theories. This extends known results from metric spaces to general symmetric monoidal closed categories.