Algebraic theories

Algebraic theories are logical theories that are purely equational, with no quantifiers allowed (except the implicit universal ones). They are among the simplest logical systems in the hierarchy of categorical logic.

Notions of algebraic theory

Diagrammatic theories or preheaf theories (nonstandard terminology, not to be confused with theories of presheaf type ):

  • specifications are sketches (with no cones or cocones)
  • syntactic categories are just the (small) categories, with no extra structure
  • categories of models are categories of presheaves

Marta Bunge characterized, up to equivalence, categories of presheaves (“diagrammatic categories”) as the cocomplete, atomic , regular categories.

Algebraic theories :

  • specifications are finite product sketches
  • syntactic categories are the multi-sorted Lawvere theories , aka finite product theories
  • categories of models are the “algebraic categories” (terminology varies)
  • syntax-semantics are related by Lawvere duality (see Awodey 2009)

Essentially algebraic theories :

Essentially algebraic theories are closely related to generalized algebraic theories, a kind of dependently typed algebraic theory.

Literature

Books and lecture notes

  • Awodey & Bauer, 2019, lecture notes: Introduction to categorical logic, Ch. 1: Algebraic theories (pdf)
    • An excellent introduction: very clear with minimal prerequisites
  • Crole, 1993: Categories for types, Ch. 3: Algebraic type theory
    • Good book to start with, providing details omitted in other sources
  • Barr & Wells, 1985: Toposes, triples, and theories, Ch. 4: Theories
    • Based on finite product sketches
  • Borceux, 1994: Handbook of categorical algebra, Vol 2, Ch. 3: Algebraic theories
    • Theorem 3.9.1: Characterization of algebraic categories (for single-sorted theories)
  • Manes, 1976: Algebraic theories (doi)
  • Adamek & Rosicky, 1994: Locally presentable and accessible categories, Ch. 3: Algebraic categories
  • Adamek, Rosicky, Vitale, 2011: Algebraic theories: A categorical introduction to general algebra (doi)
    • Title notwithstanding, this quite technical book is for specialists only
    • Features several characterizations of algebraic categories (single-sorted and multi-sorted)

Clones

Clones are cartesian multicategories with one object. They are the operadic analogue of, and are equivalent to, Lawvere theories.

  • Fujii, 2020: Introduction to universal algebra and clones (arxiv)

Monads

For the close connection between Lawvere theories and finitary monads, see the page on monads.