English

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

Category Theory 2023-10-10 v1 Logic in Computer Science Logic

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 SetSet. Recent work of Ad\'amek, Dost\'al, and Velebil has established that analogous results also hold in certain enriched contexts. Specifically, taking VV to be one of the cartesian closed categories Pos\mathsf{Pos}, UltMet\mathsf{UltMet}, ω\omega-CPO\mathsf{CPO}, or DCPO\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 VV-enriched varieties of algebras is dually equivalent to the category of strongly finitary VV-monads on VV. In this paper, we extend and generalize these results in two ways: by allowing VV to be an arbitrary complete and cocomplete cartesian closed category that is concrete over SetSet, and by also considering the multi-sorted case. Given a set SS of sorts, we define a suitable notion of (finitary) VV-enriched SS-sorted variety, and we say that a VV-monad on the product VV-category VSV^S is strongly finitary if its underlying VV-endofunctor is the left Kan extension of its restriction to a suitable full sub-VV-category of VSV^S. Our main result is that the category of VV-enriched SS-sorted varieties is dually equivalent to the category of strongly finitary VV-monads on VSV^S. By taking SS to be a singleton and VV to be Pos\mathsf{Pos}, UltMet\mathsf{UltMet}, ω\omega-CPO\mathsf{CPO}, or DCPO\mathsf{DCPO}, we thus recover the aforementioned results of Ad\'amek, Dost\'al, and Velebil. We provide several classes of examples of VV-enriched SS-sorted varieties, many of which admit very concrete, syntactic formulations.

Keywords

Cite

@article{arxiv.2310.04587,
  title  = {Strongly finitary monads and multi-sorted varieties enriched in cartesian closed concrete categories},
  author = {Jason Parker},
  journal= {arXiv preprint arXiv:2310.04587},
  year   = {2023}
}

Comments

36 pages