Теория Ловера

В теории категорий теория Ловера (названная в честь американского математика Уильяма Ловера ) — это категория , которую можно считать категориальным аналогом понятия эквациональной теории .

Определение

Позволять $\aleph _{0}$ быть скелетом категории FinSet конечных множеств и функций . Формально теория Лоувера состоит из небольшой категории L с (строго ассоциативными ) конечными произведениями тождества на объектах. и строгим функтором $I:\aleph _{0}^{\text{op}}\rightarrow L$ сохранение конечных продуктов.

Моделью C теории Лоувера в категории с конечными произведениями является функтор, сохраняющий конечное произведение M : L → C . Морфизм моделей h : M → N , где M и N — модели L, является естественным преобразованием функторов.

Категория

Отображение ′) представляет собой между теориями Лоувера ( L , I ) и ( L ′, I функтор, сохраняющий конечное произведение, который коммутирует с I и I ′. Такое отображение обычно рассматривается как интерпретация ( L , I ) в ( L ', I ').

Теории Ловере вместе с отображениями между ними образуют категорию Закон .

Вариации

Вариации включают многосортную (или многотипную ) теорию Ловера , бесконечную теорию Ловера и теорию конечного произведения .

См. также

• Алгебраическая теория
• Клон (алгебра)
• Монада (теория категорий)

Ссылки

• Хайланд, Мартин ; Пауэр, Джон (2007), «Теоретико-категорное понимание универсальной алгебры: теории Ловера и монады» (PDF) , Электронные заметки по теоретической информатике , 172 (Вычисления, значение и логика: статьи, посвященные Гордону Плоткину): 437– 458, CiteSeerX   10.1.1.158.5440 , номер документа : 10.1016/j.entcs.2007.02.019
• Ловер, Уильям Ф. (1963), «Функториальная семантика алгебраических теорий» , докторская диссертация , том. 50, нет. 5, Колумбийский университет, стр. 869–872, Bibcode : 1963PNAS...50..869L , doi : 10.1073/pnas.50.5.869 , PMC   221940 , PMID   16591125