В теории категорий теория Ловера (названная в честь американского математика Уильяма Ловера ) — это категория , которую можно считать категориальным аналогом понятия эквациональной теории .
Пусть будет скелетом категории FinSet конечных множеств и функций . Формально теория Ловера состоит из малой категории L с (строго ассоциативными ) конечными произведениями и строгим тождественным на объектах функтором, сохраняющим конечные произведения.
Модель теории Ловера в категории C с конечными произведениями — это сохраняющий конечное произведение функтор M : L → C. Морфизм моделей h : M → N , где M и N — модели L, является естественным преобразованием функторов.
Отображение между теориями Ловера ( L , I ) и ( L ′, I ′) является функтором, сохраняющим конечное произведение, который коммутирует с I и I ′. Такое отображение обычно рассматривается как интерпретация ( L , I ) в ( L ′, I ′).
Теории Закона вместе с картами между ними образуют категорию Закон .
Вариации включают многосортную (или многотипную ) теорию Ловера , бесконечную теорию Ловера и теорию конечного произведения . [1]
