En la teoría de categorías , una teoría de Lawvere (llamada así por el matemático estadounidense William Lawvere ) es una categoría que puede considerarse una contraparte categórica de la noción de teoría ecuacional .
Definición
Dejar ser un esqueleto de la categoría FinSet de conjuntos y funciones finitos . Formalmente, una teoría de Lawvere consiste en una pequeña categoría L con productos finitos (estrictamente asociativos ) y un estricto functor de identidad sobre objetos. preservando productos finitos.
Un modelo de una teoría Lawvere en una categoría C con los productos finitos es un finito-producto preservar funtor M : L → C . Un morfismo de modelos h : M → N donde M y N son modelos de L es una transformación natural de functores.
Categoría de teorías de Lawvere
Un mapa entre las teorías de Lawvere ( L , I ) y ( L ′, I ′) es un funtor de conservación de producto finito que conmuta con I e I ′. Este mapa se ve comúnmente como una interpretación de ( L , I ) en ( L ′, I ′).
Las teorías de Lawvere, junto con los mapas entre ellas, forman la categoría Ley .
Variaciones
Las variaciones incluyen multisorted (o multityped ) teoría Lawvere , teoría Lawvere infinitary , y teoría finito-producto . [1]