Linton's theorem (equational theory)
From Wikipedia, the free encyclopedia
Linton's theorem concerns the correspondence between monad and Lawvere theories. These two notions are the two main category theoretic formulations of universal algebra.[1] Although these results are not explicitly stated, they were essentially introduced by Linton (1969). The following (2) and (3) were first explicitly stated and proven by Dubuc (1970, Theorem III.), even in the more general setting of enriched category.[2] The fact that a monad is a category theoretic formulation of universal algebra is not intuitive, given its historical origins. In actually, monads originated in algebraic topology and typically arise from a pair of adjoint functors.[1] However, there is the following result concerning between monads and universal algebra, which is attributed to Linton: the category of models of a Lawvere theory is equivalent to the categories of Eilenberg–Moore algebras of the monad corresponding to that Lawvere theory.
Modern statement of Linton's theorem
- The category of finitary monads on is equivalent to the category of Lawvere theories and, subject to a generalization in the definition of Lawvere theory, every monad arises thus, uniquely up to coherent isomorphism.[1]
- Infinitary Lawvere theories are equivalent to monads on .[2]
- The category of models of an infinitary Lawvere theory is equivalent to the category of algebras of its monad.[2]
