Lawvere theory


In category theory, a Lawvere theory 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 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. A morphism of models where M and N are models of L is a natural transformation of functors.

Category of Lawvere theories

A map between Lawvere theories and is a finite-product preserving functor that commutes with I and I′. Such a map is commonly seen as an interpretation of in.
Lawvere theories together with maps between them form the category Law.

Variations

Variations include multisorted Lawvere theory, infinitary Lawvere theory, Fermat theory, and finite-product theory.