Сопряжение в дедуктивных категориях

Предсопряжение (A, B, F, G,у) представляет собой сопряжение тогда и только тогда, когда:

Легко проверить, что определенное подобным образом понятие сопряжения равносильно стандартным определениям сопряжения, которые можно найти в литературе по теории категорий. Естественные преобразования ср и у, которые представляют собой единицу и коединицу сопряжения, определяются следующим образом:

Определим теперь понятие свободного сопряжения J*, порожденного предсопряжением J. Пусть J будет (A, B, F, G,ср, у) и рассмотрим пары (=Ау=в), такие, что =а представляет собой отношение эквивалентности на стрелках А, а =в есть отношение эквивалентности на стрелках В, удовлетворяющих соответствующим условиям конгруэнтности по отношению к °, F, G,(р и у и удовлетворяющее также условиям, выведенным из пунктов (i)-(iv) определения сопряжения путем замены = на =д или =в соответственно. Назовем подобные пары (=а,=в) парами сопряженных отношений эквивалентности на J.

Нетрудно убедиться, что если мы возьмем все пары сопряженных отношений эквивалентности на J и возьмем пересечение =_Ап всех отношений =а и пересечение =вп всех отношений =в в подобных парах, то получим вновь пару сопряженных отношений эквивалентности (=Ап,=вгд- Рассмотрим теперь для каждой стрелки / из А классы эквивалентности [/] = <*./ {/':/ =ап/'}, и аналогично для В, и определим на них следующие операции:

Объекты из А и В вместе с классами эквивалентности образуют категории (Д*, 1,°) и (В*, 1,°). Тогда (A*.B*, F.G.

где F, G, cp и у определены для А* и В* (т.е. на классах эквивалентности), будет представлять собой сопряжение. Оно то и будет называться свободным сопряжением J*, порожденным J.

Свободное сопряжение J*, порожденное свободным предсопряжением J, порожденным парой объектов (G, H), будет называться свободным сопряжением J*, порожденным (G, H). Стрелочные термы категорий А* и В* из J* являются, соответственно, теми же, что и стрелочные термы дедуктивных систем А и В из J.