Strongly finitary monads and multi-sorted varieties enriched in cartesian closed concrete categories

TL;DR

This paper generalizes classical categorical algebra results by establishing a duality between enriched varieties and strongly finitary monads in a broad class of cartesian closed categories, including multi-sorted cases.

Contribution

It extends existing duality results to arbitrary complete, cocomplete, cartesian closed categories that are concrete over Set, and introduces multi-sorted enriched varieties.

Findings

Duality between enriched varieties and strongly finitary monads

Extension to multi-sorted cases and arbitrary categories

Concrete examples of enriched varieties

Abstract

It is a classical result of categorical algebra, due to Lawvere and Linton, that finitary varieties of algebras (in the sense of Birkhoff) are dually equivalent to finitary monads on $Set$. Recent work of Ad\'amek, Dost\'al, and Velebil has established that analogous results also hold in certain enriched contexts. Specifically, taking $V$ to be one of the cartesian closed categories $\mathsf{Pos}$, $\mathsf{UltMet}$, $\omega$-$\mathsf{CPO}$, or $\mathsf{DCPO}$ of respectively posets, (extended) ultrametric spaces, $\omega$-cpos, or dcpos, Ad\'amek, Dost\'al, and Velebil have shown that a suitable category of $V$-enriched varieties of algebras is dually equivalent to the category of strongly finitary $V$-monads on $V$. In this paper, we extend and generalize these results in two ways: by allowing $V$ to be an arbitrary complete and cocomplete cartesian closed category that is concrete over $Set$, and by also considering the multi-sorted case. Given a set $S$ of sorts, we define a suitable notion of (finitary) $V$-enriched $S$-sorted variety, and we say that a $V$-monad on the product $V$-category $V^S$ is strongly finitary if its underlying $V$-endofunctor is the left Kan extension of its restriction to a suitable full sub-$V$-category of $V^S$. Our main result is that the category of $V$-enriched $S$-sorted varieties is dually equivalent to the category of strongly finitary $V$-monads on $V^S$. By taking $S$ to be a singleton and $V$ to be $\mathsf{Pos}$, $\mathsf{UltMet}$, $\omega$-$\mathsf{CPO}$, or $\mathsf{DCPO}$, we thus recover the aforementioned results of Ad\'amek, Dost\'al, and Velebil. We provide several classes of examples of $V$-enriched $S$-sorted varieties, many of which admit very concrete, syntactic formulations.