symmetric monoidal (∞,1)-category of spectra
An algebra over an endofunctor is like an algebra over a monad, but without a notion of associativity (given that a plain endofunctor is not equipped with a multiplication-operation that would make it a monad).
For a category and endofunctor , an algebra (or module) of is an object in and a morphism . ( is called the carrier of the algebra)
A homomorphism between two algebras and of is a morphism in such that the following square commutes:
Composition of such homomorphisms of algebras is given by composition of the underlying morphisms in . This yields the category of -algebras, which comes with a forgetful functor to .
The dual concept is a coalgebra for an endofunctor. Both algebras and coalgebras for endofunctors on are special cases of algebras for bimodules.
If is a pointed endofunctor with point , then by an algebra for one usually means a pointed algebra, i.e. one such that .
To a category theorist, algebras over a monad may be more familiar than algebras over just an endofunctor. In fact, when and are well-behaved, then algebras over an endofunctor are equivalent to algebras over a certain monad, the algebraically-free monad generated by (Pirog, Gambino-Hyland 04, section 6).
This is analogous to the relationship between an action of a monoid and a binary function (an action of a set): such a function is the same thing as an action of the free monoid on .
Returning to the endofunctor case, the general statement is:
The category of algebras of the endofunctor is equivalent to the category of algebras of the algebraically-free monad on , should such exist.
Actually, this proposition is merely a definition of the term “algebraically-free monad”. If has an algebraically-free monad, denoted say , then in particular the forgetful functor has a left adjoint, and is the monad on generated by this adjunction. Conversely, if such a left adjoint exists, then the monad it generates is algebraically-free on ; for a mechanised proof in cubical Agda, see (1Lab). An explicit construction of the algebraically free monad in terms of inductive types is given below.
Algebraically-free monads exist in particular when is a locally presentable category and is an accessible functor; see transfinite construction of free algebras.
It turns out that an algebraically-free monad on is also free in the sense that it receives a universal arrow from relative to the forgetful functor from monads to endofunctors. The converse, however, is not necessarily true: a free monad in this sense need not be algebraically-free. It is true when is complete, however.
Entirely analogous facts are true for pointed algebras over pointed endofunctors.
The initial algebra of an endofunctor provides categorical semantics for inductive types.
The construction of an algebraically free monad may be cast in the language of such initial algebras. Suppose is a category with coproducts and is an endofunctor. Let - be the category of -algebras, and let be the usual forgetful functor. A left adjoint to then takes an object of to the initial algebra of the endofunctor , provided this initial algebra exists. For, by the usual comma category description (see for example adjoint functor theorem), is the initial object of the category . However, an object of is a triple , equivalently a pair , equivalently an algebra of . Hence an initial object of is an initial algebra of an endofunctor.
The monad structure of the algebraically free monad may be straightforwardly extracted from this initial algebra description. This is made explicit in Pirog. For example, to describe the multiplication , let be an object; then has an algebra structure . It therefore also has a structure of algebra over the endofunctor , namely . But since is the initial algebra for the monad , we obtain a unique algebra map . This is the component of the monad multiplication.
A textbook account of the basic theory is in chapter 10 of
The relation to free monads is discussed in
Formalization in cubical Agda:
Last revised on July 10, 2024 at 00:44:07. See the history of this page for a list of all contributions to it.