Birkhoff's variety theorem for relative algebraic theories
Yuto Kawase
TL;DR
This paper extends universal algebra beyond Set by developing $oldsymbol{\mathscr{A}}$-relative algebraic theories for locally finitely presentable categories using partial Horn logic. It establishes an equivalence between $oldsymbol{\mathscr{A}}$-relative algebraic theories and finitary monads on $oldsymbol{\mathscr{A}}$, with models preserved under the correspondence. A generalized Birkhoff-type variety theorem is proved, replacing subobjects with $oldsymbol{\Sigma}$-closed subobjects and quotients with $U$-retracts, and requiring closure under filtered colimits; this captures equational-like classes in the relative setting and clarifies the syntactic dependence of the theorem. The paper also develops the framework of presenting the category of relative algebras as strictly finitary monadic over a base category of models and details the role of presentable factorization systems in supporting the generalized results. Together, these results realize a syntactic approach to universal algebra over categories such as $ extbf{Pos}$ and $ extbf{Cat}$, enabling algebraic theories beyond the classical Set-based setting and providing tools for reasoning about finitary monads in broader categorical contexts.
Abstract
An algebraic theory, sometimes called an equational theory, is a theory defined by finitary operations and equations, such as the theories of groups and of rings. It is well known that algebraic theories are equivalent to finitary monads on $\mathbf{Set}$. In this paper, we generalize this phenomenon to locally finitely presentable categories using partial Horn logic. For each locally finitely presentable category $\mathscr{A}$, we define an "algebraic concept" relative to $\mathscr{A}$, which will be called an $\mathscr{A}$-relative algebraic theory, and show that $\mathscr{A}$-relative algebraic theories are equivalent to finitary monads on $\mathscr{A}$. In establishing such equivalence, a generalized Birkhoff's variety theorem plays an important role.