(draft)
The main theorem is that a functor on a variety (in the sense of universal algebra) has a presentation by operations and equations if and only if the functor preserves sifted colimits.
The theory of sifted colimits is well explained in Adamek-Rosicky-Vitale. We only cover some highlights.
In all of the following is a variety in the sense of univeral algebra, that is, a category of algebras specified (finitary) operations equations. (We will assume all operations to be finitary in the following, even if we drop the qualifier.)
Filtered categories are precisely categories such that colimits over commute with finite limits in Set. There is also a characterization of filtered categories independent of sets – a category is filtered if and only if the diagonal functor is final for each finite category .
Sifted categories are the categories such that colimits over commute with finite products. These categories are characterized by the property that the diagonal functor is final.
Facts:
An object of a category is finitely presentable if its hom-functor preserves filtered colimits. A category is locally finitely presentable (lfp) if it is cocomplete and has a set of finitely presentable objects such that each object of is a filtered colimit of objects from .
An object is strongly finitely presentable if its hom-functor preserves sifted colimits. A category is strongly locally finitely presentable (slfp) if it is cocomplete and has a set of strongly finitely presentable objects such that each object of is a sifted colimit of objects from .
Let be a variety in the sense of universal algebra.
Facts:
Let be the categories of algebras for the functor .
Theorem: If is a variety and preserves sifted colimits then is a variety.
Proposition:
Given an adjunction such that the right-adjoint is monadic (or of descent type) all objects have a presentation "by generators and relations"
In words, is the quotient of the free algebra over generators by equations in .
We apply this "monadic presentation" now to the situation where is an endofunctor. In fact, we apply it twice and combine two representations:
Step 1: We represent a sifted colimit preserving endofunctor on a variety such that the "generators" and "relations" are given by sifted colimit preserving endofunctors on Set.
Step 2: We represent a sifted colimit on Set as the quotient of polynomial functor.
Let be the category of sifted colimit preserving functors .
Fact: The category is slfp if is.
A functor between slfp categories is called algebraically exact provided that it preserves limits and sifted colimits.
Fact: If is algebraically exact it has a left adjoint.
Let be a variety and . Define
via and
via .
Fact: is algebraically exact and .
After the first step, we obtain a quotient . Here, results from applying the free construction to the Set-functor . What we need next is a presentation by operations and equations of .
Every sifted colimit preserving on (=filtered colimit preserving functor=finitary functor) can be presented as the quotient of a polynomial functor.
Indeed, if is finitary then we have a natural transformation
with each being surjective (even for infinite sets ).
Note that can be seen both as a tuple and as a function . Hence we can evaluate the term by applying to .
This gives us a representation of as a functor by operations and equations where the set of -ary operations is and the set of equations in variables is the kernel of .
Theorem: A functor on a variety has a presentation by operations and equations iff the functor preserves sifted colimits.
To prove "if", one shows that every sifted colimit preserving functor on a variety is a quotient
where .
In particular the are modal formulas
where and .
The set of operations and the set of equations constitute the presentation of .
Theorem: Let be a variety and a presentation of . Then is isomorphic to Alg(L), where equations in and are understood as equations over .
Example: The variety of modal algebras is presented by the operations and equations of Boolean algebra plus a unary operation and two equations specifying that preserves finite meets.
Kurz-Rosicky: Strongly Complete Logics for Coalgebras, 2012.
Note that is a modal formula where and . ↩︎