Lawvere theory

Let $\backslash aleph\_0$ 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 $I:\backslash aleph\_0^\backslash text\{op\}\backslash rightarrow\; L$ preserving finite products.

A model of a Lawvere theory in a category C with finite products is a finite-product preserving functor {{nowrap|M : L → C}}. A morphism of models {{nowrap|h : M → N}} where M and N are models of L is a natural transformation of functors.

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 include multisorted (or multityped) Lawvere theory, infinitary Lawvere theory, and finite-product theory.{{nlab|id=Lawvere+theory|title=Lawvere theory}}

• Algebraic theory
• Clone (algebra)
• Monad (category theory)

{{reflist}}

• {{Citation |last1=Hyland |first1=Martin |last2=Power |first2=John |authorlink=Martin Hyland |date=2007 |title=The Category Theoretic Understanding of Universal Algebra: Lawvere Theories and Monads |journal=Electronic Notes in Theoretical Computer Science |volume=172 |issue=Computation, Meaning, and Logic: Articles dedicated to Gordon Plotkin |pages=437–458 |doi=10.1016/j.entcs.2007.02.019 |citeseerx=10.1.1.158.5440 |url=https://www.dpmms.cam.ac.uk/~jmeh1/Research/Publications/2007/hp07.pdf}}
• {{Citation |last1=Lawvere |first1=William F. |authorlink=William Lawvere |date=1963 |title=Functorial Semantics of Algebraic Theories |publisher=Columbia University |work=PhD Thesis |volume=50 |issue=5 |pages=869–872 |doi=10.1073/pnas.50.5.869 |pmid=16591125 |pmc=221940 |bibcode=1963PNAS...50..869L |url=http://www.tac.mta.ca/tac/reprints/articles/5/tr5abs.html|doi-access=free }}

Category:Categorical logic