nLab algebra for an endofunctor

Redirected from "F-algebra".
Contents

Context

Category theory

Algebra

Contents

Idea

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).

Definition

Definition

For a category CC and endofunctor FF, an algebra (or module) of FF is an object XX in CC and a morphism α:F(X)X\alpha\colon F(X) \to X. (XX is called the carrier of the algebra)

A homomorphism between two algebras (X,α)(X, \alpha) and (Y,β)(Y, \beta) of FF is a morphism m:XYm\colon X \to Y in CC such that the following square commutes:

F(X) F(m) F(Y) α β X m Y. \array{ F(X) & \overset{F(m)}{\longrightarrow} & F(Y) \\ \mathllap{{}^{\alpha}}\big\downarrow && \big\downarrow\mathrlap{{}^{\beta}} \\ X & \underset{m}{\longrightarrow} & Y } \,.

Composition of such homomorphisms of algebras is given by composition of the underlying morphisms in CC. This yields the category of FF-algebras, which comes with a forgetful functor to CC.

Remark

The dual concept is a coalgebra for an endofunctor. Both algebras and coalgebras for endofunctors on CC are special cases of algebras for bimodules.

If FF is a pointed endofunctor with point η:IdF\eta : Id \to F, then by an algebra for FF one usually means a pointed algebra, i.e. one such that αη X=id X\alpha \circ \eta_X = id_X.

Properties

Relation to algebras over a monad

To a category theorist, algebras over a monad may be more familiar than algebras over just an endofunctor. In fact, when CC and FF are well-behaved, then algebras over an endofunctor FF are equivalent to algebras over a certain monad, the algebraically-free monad generated by FF (Pirog, Gambino-Hyland 04, section 6).

This is analogous to the relationship between an action M×BBM \times B \to B of a monoid MM and a binary function A×BBA \times B \to B (an action of a set): such a function is the same thing as an action of the free monoid A *A^* on BB.

Returning to the endofunctor case, the general statement is:

Proposition

The category of algebras of the endofunctor F:𝒞𝒞F\colon \mathcal{C} \to \mathcal{C} is equivalent to the category of algebras of the algebraically-free monad on FF, should such exist.

Actually, this proposition is merely a definition of the term “algebraically-free monad”. If FF has an algebraically-free monad, denoted say F *F^*, then in particular the forgetful functor FAlgCF Alg \to C has a left adjoint, and F *F^* is the monad on CC generated by this adjunction. Conversely, if such a left adjoint exists, then the monad it generates is algebraically-free on FF; 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 CC is a locally presentable category and FF is an accessible functor; see transfinite construction of free algebras.

Remark

It turns out that an algebraically-free monad on FF is also free in the sense that it receives a universal arrow from FF 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 CC is complete, however.

Entirely analogous facts are true for pointed algebras over pointed endofunctors.

Relationship to inductive types

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 CC is a category with coproducts and F:CCF: C \to C is an endofunctor. Let FF-algalg be the category of FF-algebras, and let U:F-algCU: F\text{-}alg \to C be the usual forgetful functor. A left adjoint to UU then takes an object dd of CC to the initial algebra Φ(d)\Phi(d) of the endofunctor cd+F(c)c \mapsto d + F(c), provided this initial algebra exists. For, by the usual comma category description (see for example adjoint functor theorem), Φ(d)\Phi(d) is the initial object of the category (dU)(d \downarrow U). However, an object of (dU)(d \downarrow U) is a triple (c,α:F(c)c,β:dc)(c, \alpha: F(c) \to c, \beta: d \to c), equivalently a pair (c,γ:d+F(c)c)(c, \gamma: d + F(c) \to c), equivalently an algebra of cd+F(c)c \mapsto d + F(c). Hence an initial object of (dU)(d \downarrow U) is an initial algebra of an endofunctor.

The monad structure of the algebraically free monad F *=UΦF^\ast = U\Phi may be straightforwardly extracted from this initial algebra description. This is made explicit in Pirog. For example, to describe the multiplication μ:F *F *F *\mu: F^\ast F^\ast \to F^\ast, let dd be an object; then F *dF^\ast d has an algebra structure [i,θ]:d+F(F *d)F *d[i, \theta]: d + F(F^\ast d) \to F^\ast d. It therefore also has a structure of algebra over the endofunctor cF *d+F(c)c \mapsto F^\ast d + F(c), namely [1,θ]:F *d+F(F *d)F *d[1, \theta]: F^\ast d + F(F^\ast d) \to F^\ast d. But since F *F *dF^\ast F^\ast d is the initial algebra for the monad cF *d+F(c)c \mapsto F^\ast d + F(c), we obtain a unique algebra map F *F *dF *dF^\ast F^\ast d \to F^\ast d. This is the component μ d\mu_d of the monad multiplication.

References

A textbook account of the basic theory is in chapter 10 of

The relation to free monads is discussed in

  • Nicola Gambino, Martin Hyland, Wellfounded trees and dependent polynomial functors. In Types for proofs and programs, volume 3085 of Lecture Notes in Comput. Sci., pages 210–225. Springer-Verlag, Berlin, 2004 (web)

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.