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 $\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:\aleph _{0}^{\text{op}}\rightarrow L$ 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, Fermat theory (named Fermat's difference quotient), and finite-product theory.[1]

gollark: I don't get it. The debug thing works totally on the bot's end and yet "connection error"?

gollark: ++exec```pythonprint("hi")```

gollark: ++exec --debug```pythonprint("hi")```

gollark: ++exec```pythonprint("hi")```

Notes

Lawvere theory in nLab

References

Hyland, Martin; Power, John (2007), The Category Theoretic Understanding of Universal Algebra: Lawvere Theories and Monads (PDF)
Lawvere, William F. (1964), Functorial Semantics of Algebraic Theories (PhD Thesis)

This article is issued from Wikipedia. The text is licensed under Creative Commons - Attribution - Sharealike. Additional terms may apply for the media files.

[1] Lawvere theory in nLab