I'm trying to understand better what it means for a monad to be finitary. I know that Lawvere theories correspond to finitary monads, but I don't really understand the definition in terms of filtered colimits.


Normal lists satisfy


$$L(X) = 1 + X\cdot L(X).$$


Now suppose that at position n in the list, we can use either an
element of X or one of n extra values:


$$F(X) = 1 + X\cdot F(X + 1)$$


An element of F(0) is a numeral in ["factoradic" or "base factorial"](https://en.wikipedia.org/wiki/Factorial_number_system).


$F$ is a monad with the usual list operations. Is it finitary? If so, what does the corresponding Lawvere theory look like? If not, how does it fail to preserve filtered colimits?



Do "factoradic" lists form a finitary monad?
Yes, it is finitary. If you think about $X$ as a set of variable and about $T(X)$ as a set of structures of some sort, then $T : Set \to Set$ is finitary if every structure $t \in T(X)$ can use only finite number of variables (roughly speaking). Every list uses only a finite number of variables (up to its length), so does every $F$-structure.


Another example of a functor like yours is the functor of untyped lambda terms which satisfies the following equation:
$$C(X) = X + C(X) \times C(X) + C(X + 1)$$
Elements of $C(X)$ are untyped lambda terms whose free variables belong to $X$. Since any lambda term can use only a finite number of variables from $X$, this functor is also finitary.


An example of a non-finitary monad is the monad of trees with infinite number of children:
$$I(X) = X + (\mathbb{N} \to I(X))$$
Since an infinite tree can use an infinite number of variables, it is not finitary. A formal proof of this fact goes like this. Let $X$ be an infinte set. Then it is a directed colimit of its finite subsets, but every tree in the colimit $colim\_{Y \subset\_{fin} X}(I(Y))$ uses only a finite number of variables (namely, the variables from $Y$), so it is not (canonically) isomorphic to the set of all trees $I(X)$. Thus $I$ does not preserve directed colimits.


Algebraic theories is a more explicit way of talking about theories than Lawvere theories. You can always describe an algebraic theory that corresponds to a (finitary) monad $T$ as a theory with $T(\{x\_1, \ldots x\_n\})$ $n$-ary operations. Sometimes there is a more simple description. For example, the theory that corresponds to $L$ is equivalent to the theory of monoids. Another way to present this theory as the theory with one $n$-ary operation for every $n$ (and a bunch of axioms). You can think of such operation as the concatenation of $n$ elements of a monoid.


Now, you can present the theory for $F$ in a similar way. It will have the same operation as the theory for $L$, but it will also have operations that correspond to the concatenation of a list in which some elements are not elements of your structure, but the new elements that you add in the definition of $F$. Overall, it will have infinitely many $n$-ary operations for every $n > 0$. You can explicitly describe them in terms of lists in which you may have $n$ different holes in $n$-th place. In general, it is a non-trivial task to find a simple presentation for a monad in terms of operations. There is probably a more simple description of the theory for $F$ than the one that I have in mind.


