В теории категорий , теория Ловер (названная в честь американского математика Уильям Ловер ) является категорией , которую можно рассматривать как категорический аналог понятию эквациональной теории .
Определение
Позволять быть скелетом из категории FinSet из конечных множеств и функций . Формально теория Ловера состоит из небольшой категории L с (строго ассоциативными ) конечными произведениями и строгого функтора тождества на объектах сохранение конечных продуктов.
Модель из теории Ловера в категории С с конечными продуктами является конечным продуктом сохраняя функтор M : L → C . Морфизм моделей часов : М → N , где М и N являются моделями L представляет собой естественное преобразование функторов.
Категория теорий Ловера
Отображение между теориями Ловера ( L , I ) и ( L ', я ') является конечным продуктом сохраняя функтор, коммутирует с I и I '. Такая карта обычно рассматривается как интерпретация ( L , I ) в ( L ′, I ′).
Теории Ловера вместе с отображениями между ними образуют категорию Закона .
Вариации
Изменения включают multisorted (или multityped ) теории Ловера , инфинитарной теории Ловера и теории конечно-продукта . [1]
Смотрите также
Заметки
Рекомендации
- Хайленд, Мартин ; Пауэр, Джон (2007), Теоретико-категориальное понимание универсальной алгебры: теории и монады Ловера (PDF)
- Ловер, Уильям Ф. (1964), функциональная семантика алгебраических теорий (докторская диссертация)