In category theory, a Lawvere theory (named after American mathematician William Lawvere) is a category which can be considered a categorical counterpart of the notion of an equational theory.
Contents
Definition
Let
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 which 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, Fermat theory (named Fermat's difference quotient), and finite-product theory.