![]() | ||
In category theory, a branch of mathematics, a monad (also triple, triad, standard construction and fundamental construction) is an endofunctor (a functor mapping a category to itself), together with two natural transformations. Monads are used in the theory of pairs of adjoint functors, and they generalize closure operators on partially ordered sets to arbitrary categories.
Contents
Introduction
A monad is a certain type of endofunctor. For example, if
The monad axioms can be seen at work in a simple example: let
This means that the monad
takes a set
by including any set
can be made out of a natural concatenation or 'flattening' of 'strings of strings'. This amounts to two natural transformations
and
They will satisfy some axioms about identity and associativity that result from the adjunction properties.
Another example is when
Those axioms are formally similar to the monoid axioms. They are taken as the definition of a general monad (not assumed a priori to be connected to an adjunction) on a category.
If we specialize to categories arising from partially ordered sets
Every monad arises from some adjunction, in fact typically from many adjunctions. Two constructions introduced below, the Kleisli category and the category of Eilenberg–Moore algebras, are extremal solutions of the problem of constructing an adjunction that gives rise to a given monad.
The example about free groups given above can be generalized to any type of algebra in the sense of a variety of algebras in universal algebra. Thus, every such type of algebra gives rise to a monad on the category of sets. Importantly, the algebra type can be recovered from the monad (as the category of Eilenberg–Moore algebras), so monads can also be seen as generalizing universal algebras. Even more generally, any adjunction is said to be monadic (or tripleable) if it shares this property of being (equivalent to) the Eilenberg–Moore category of its associated monad. Consequently, Beck's monadicity theorem, which gives a criterion for monadicity, can be used to show that an arbitrary adjunction can be treated as a category of algebras in this way.
The notion of monad was invented by Roger Godement in 1958 under the name "standard construction." In the 1960s and 1970s, many people used the name "triple." The now standard term "monad" is due to Saunders Mac Lane.
Formal definition
If
We can rewrite these conditions using following commutative diagrams:
See the article on natural transformations for the explanation of the notations
The first axiom is akin to the associativity in monoids, the second axiom to the existence of an identity element. Indeed, a monad on
Comonads and their importance
The categorical dual definition is a formal definition of a comonad (or cotriple); this can be said quickly in the terms that a comonad for a category
Since a comonoid is not a basic structure in abstract algebra, this is less familiar at an immediate level.
The importance of the definition comes in a class of theorems from the categorical (and algebraic geometry) theory of descent. What was realised in the period 1960 to 1970 is that recognising the categories of coalgebras for a comonad was an important tool of category theory (particularly topos theory). The results involved are based on Beck's theorem. Roughly what goes on is this: while it is simple set theory that a surjective mapping of sets is as good as the equivalence relation "x is in the same fiber as y" on the domain of the mapping, for geometric morphisms what you should do is pass to such a coalgebra subcategory.
Examples
The rich set of examples is given by adjunctions (see Monads and adjunctions), and the free group example mentioned above belongs to that set.
Here is another example, on the category
takes a set of sets to its union. These data describe a monad.
Closure operators are monads on preorder categories.
Algebras for a monad
Suppose that
A
commute.
A morphism
commutes.
The category
Given the monad
Monads and adjunctions
An adjunction
Conversely, it is interesting to consider the adjunctions which define a given monad
An adjunction
Uses
Monads are used in functional programming to express types of sequential computation (sometimes with side-effects). See monads in functional programming, and the more mathematically oriented Wikibook module b:Haskell/Category theory.
In categorical logic, an analogy has been drawn between the monad-comonad theory, and modal logic via closure operators, interior algebras, and their relation to models of S4 and Intuitionistic logics.
Generalization
It is possible to define monads in a 2-category