Lawvere theory

From Wikipedia, the free encyclopedia
Jump to: navigation, search

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.

Definition[edit]

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 : LC. A morphism of models h : MN where M and N are models of L is a natural transformation of functors.

Category of Lawvere theories[edit]

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[edit]

Variations include multisorted (or multityped) Lawvere theory, infinitary Lawvere theory, Fermat theory (named Fermat's difference quotient), and finite-product theory.[1]

See also[edit]

Notes[edit]

References[edit]