En la teoría de categorías , una teoría de Lawvere (llamada así en honor al matemático estadounidense William Lawvere ) es una categoría que puede considerarse una contraparte categórica de la noción de una teoría ecuacional .
Sea 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 funtor de identidad estricta con respecto a los objetos que preserva los productos finitos.
Un modelo de una teoría de Lawvere en una categoría C con productos finitos es un funtor que preserva el producto finito M : L → C . Un morfismo de modelos h : M → N donde M y N son modelos de L es una transformación natural de funtores.
Una función entre las teorías de Lawvere ( L , I ) y ( L ′, I ′) es un funtor que preserva el producto finito y que conmuta con I e I ′. Una función de este tipo se considera 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 Derecho .
Las variaciones incluyen la teoría de Lawvere multiclasificada (o multitipificada ) , la teoría de Lawvere infinitaria y la teoría de productos finitos . [1]
