Четвертая. 
Сопряжение и когерентность

Предсопряжение в дедуктивных системах

Перед тем как рассмотреть понятие сопряжения, рассмотрим более общее понятие, которое будем называть предсопряжением, и которое выполняет те же функции в дедуктивных системах, что и сопряжение в дедуктивных категориях (таким образом, предсопряжение находится в таком же отношении к сопряжению, как дедуктивные системы к дедуктивным категориям)^[1]. Обозначим для удобства дальнейшего изложения дедуктивную систему как тройку (0,1 ,"), где D будет представлять собой граф, 1 есть стрелка тождества в D, а ° есть композиция в D. Тождество и композиция в различных дедуктивных системах всегда будем обозначать одними и теми же символами 1 и предполагая, что из контекста ясно, какой дедуктивной системе они принадлежат.

Пусть (А, 1,°) и (В, 1,°) будут представлять собой дедуктивные системы и пусть F будет морфизмом графов из Л в В и пусть G будет морфизмом графов из В в А. Далее, пусть ф будет операцией на стрелках А, которая сопоставляет каждой стрелке/: A i -> Л₂ из А стрелку ф (/): FG (A0 —> А₂ и пусть у будет операцией на стрелках В, такой, что она сопоставляет каждой стрелке g: 5, —> В₂ из В стрелку y (g): В -> FG (B) из В.

Будем говорить, что шестерка {A, B, F, G, g>, у) есть предсопряжение. Будем говорить, что это предсопряжение между А и В, именно в этом порядке (порядок, как видно будет далее, здесь очень важен). Упрощая обозначения, мы не будем различать тождества и композицию в (А, 1,°) и (В, 1,").

Морфизмы между предсопряжениями будем называть юнкторами^[2]. Юнктор из предсопряжения (A, B, F, G,(p, у) в предсопряжение.

{A 'B'F'G'cp',/) будет представлять собой пару функторов (М_А.Мд) из Л в Л’и из б в В' соответственно, которые сохраняют структуру предсопряжений.

Определим теперь понятие свободного предсопряжения J, порожденного парой множеств объектов (G, H). Множество объектов может рассматриваться как граф без стрелок.

Вначале введем понятие атомарных символов для объектов из G и Н, называемых порождающими объектными термами А н В соответственно. Порождающие объектные термы А и В будут принадлежать к объектным термам А и В, которые можно определить, полагая, что если В будет объектным термом В, то FB будет объектным термом А и что если А будет объектным термом А, то GA будет объектным термом В.

Определим теперь стрелочные термы А и В. Каждый стрелочный терм из А будет иметь единственный тип, представляющий собой пару (Ai, A₂) объектных термов А. Чтобы обозначить, что стрелочный терм/из А имеет тип (А,^4₂), будем писать f А, —> А₂. То же самое будет иметь место и для стрелочных термов из В.

Определение. Стрелочные термы из Л и В можно определить индуктивно следующим образом:

• • если А есть объектный терм из А, то 1А —> А будет стрелочным термом из А, и аналогично с заменой А на В:
• • если f :A —> А₂ и/: А₂ —> А₂ суть стрелочные термы из, то (f₂°f): А —> А₃, будет представлять собой стрелочный терм из А, и аналогично с заменой А на В;
• • если g: В —> В₂ есть стрелочный терм из В, то F (g): F (B) —" F (B₂) будет представлять собой стрелочный терм из А
• • если/ А -> А₂ есть стрелочный терм из А, то Gff): G (A,) —> G (A₂) будет представлять собой стрелочный терм из В;
• • если/ А -> А₂ есть стрелочный терм из А, то ^: FG (A О —> А₂ будет представлять собой стрелочный терм из Л;
• • если g: Si —" В₂ есть стрелочный терм из В, то y (g): В, —> GF (B₂) будет представлять собой стрелочный терм из В;

Объектные термы из А порождают объекты, а стрелочные термы порождают стрелки графа А, то же самое относится и к графу В. Более того, (А, 1 о) и {В, 1,") представляют собой дедуктивные системы, а (Л, В, Р, 6,<�р, у) представляет собой предсопряжение. Таким образом, это свободное предсопряжение J, порожденное (G, H).

• [1] А1 К. Дошен [Dosen 1999] говорит о junction и adjunction, что по-русскиможно было бы буквально передать как пряжение и сопряжение.
• [2] Опять-таки следуя Дошену (у него в тексте — junctors, по аналогии сfunctors).