Lawvere theory
In category theory, a Lawvere theory (named after American mathematician William Lawvere) is a category that can be considered a categorical counterpart of the notion of an equational theory.
Definition[]
Let be a skeleton of the category FinSet of finite sets and functions. Formally, a Lawvere theory consists of a small category L with (strictly associative) finite products and a strict identity-on-objects functor preserving finite products.
A model of a Lawvere theory in a category C with finite products is a finite-product preserving functor M : L → C. A morphism of models h : M → N where M and N are models of L is a natural transformation of functors.
Category of Lawvere theories[]
A map between Lawvere theories (L, I) and (L′, I′) is a finite-product preserving functor that commutes with I and I′. Such a map is commonly seen as an interpretation of (L, I) in (L′, I′).
Lawvere theories together with maps between them form the category Law.
Variations[]
Variations include multisorted (or multityped) Lawvere theory, infinitary Lawvere theory, and finite-product theory.[1]
See also[]
- Algebraic theory
- Clone (algebra)
- Monad (category theory)
Notes[]
- ^ Lawvere theory in nLab
References[]
- Categorical logic