Свободное сопряжение и когерентность

Рассмотрим свободное сопряжение между А* и В*, порожденное парой множество объектов. Каждому стрелочному терму h: С| —> С₂ из А* или В* мы сопоставляем множество связей A (h), представляющее собой множество неупорядоченных пар вхождений F или G в Ci или С₂. Л (/г) определяем индукцией по сложности h.

Если h есть 1с, то Ci и С₂ представляют собой два экземпляра С, и в Л (/г) мы помещаем связи между и-ым F из С и и-ым F из С₂ (отсчитывая слева) и точно так же для связей между и-ым G из С| и и-ым G из С₂.

Если h имеет вид F (g): F (B) —" F (В₂), то Л (/г) получается путем добавления к копии Л (/г) связи между первым F в F (B_t) и первым F в F (B₂). Если h имеет вид G (f): G (A,) -> G (А₂), то Л (/г) получается путем добавления к копии Л (/г) связи между первым G в G (A,) и первым G в G (C₂).

Если h имеет вид ср (/): FG (A |) -> А₂, то Л (ф (/)) получается путем добавления к копии Л (/) связи между первым F и первым G в FG (A |). Если И имеет вид y (g): Вi —> GF (B₂), то мы получаем A (y (g)).

путем добавления к копии Л (/) связи между первым G и первым F в GF (B₂).

Наконец, если h: С —> С2 имеет вид h₂⁰ /21 для Лр Ci -" С3 и Аг: Сз С2, то каждая связь в Л (Л) получается в из конечной последовательности связей {х_]ух₂}, {ддозЬ {*3г*4},…, {*_и-1г*л}> с и? 1, в которой связи A (/?0 чередуются со связями Л (Л₂) (в этой последовательности имеется по меньшей мере одна связь из Л (А|) или A.(hi)). Вершины х и х_п представляют собой вхождения F или G в Ci или Ci и если п > 3, то все *2, …, х". являются вхождениями F или G в С3. Легко видеть, что не может быть последовательности связей вида {х_]гх₂}, {х_2гх₃}, …, {х_2пЛух_2п}, {x_2n^i} с п > 1, в которой все jcj, …, х_2п представляют собой вхождения F или G в С3.

Заметим, что для И: С -> С₂ каждый F или G в С или С2 связан в Л (А) в точности с одним вхождением F или G в Ci или С2 (в [Eilenberg Kelly 1966] и [Kelly Mac Lane 1971] подобные связи называются графами).

Поскольку связи были определены для стрелочных термов из А* и В* в одной формулировке сопряжения, связи стрелочных термов из А* и В* в другой формулировке сопряжения получаются, если мы принимаем, что стрелочные термы последней определены в терминах первой из них. Например, основываясь на естественных преобразованиях <�р и у как они были определены ранее в этом разделе, мы получаем следующие связи для двух сторон равенства треугольника^f (B)° Fj^{= 1} пв) •

Основываясь на понятии нормальной формы, можно доказать следующую лемму, касающуюся связей стрелочных термов из А* и.

Лемма. Предположим, что h и И₂ представляют собой стрелочные термы из А* и В* в нормальной форме, имеющей тот же самый тип. Тогда A (/?i) = Л (Лг) тогда и только тогда, когда И будет тем же самый стрелочным термом, что и h₂.

С помощью этой леммы мы можем доказать следующую теорему, которая представляет собой разновидность теоремы когерентности (см., например, [Mac Lane 1971]).

Теорема когерентности. Если h, и h₂ представляют собой стрелочные термы из А* одного и того же типа, то h = h₂ в А* тогда и только тогда, когда A (Ai) = A (7j₂) и то же самое для В*

Таким образом, для того, чтобы проверить, коммутирует ли диаграмма стрелок, достаточно вычертить связи стрелок из диаграммы и проверить, равны ли они.

Теорема когерентности гарантирует, что существует точный функтор из А* в категорию, чьи объекты представляют собой конечные, возможно пустые, последовательности чередований F и G, которые, если они непусты, должны начинаться с F; стрелки этой категории являются связями. Аналогичным образом гарантируется, что существует точный функтор из В* в категорию, чьи объекты суть такие последовательности F и G , что непустые последовательности начинаются с G; вновь стрелки будут представлять собой связи. Если каждое из порождающих множеств объектов G и Н непусто, то функторы будут функторами на объекты и на стрелки. Если и G и Н являются единичными множествами, то эти функции будут изоморфизмами.

Связи, введенные нами, дают простой теоретико-модельный метод для нормализации стрелочных термов из Л* или В*. Этот метод заключаегся в вычерчивании связей стрелочных термов, а затем конструировании очевидным образом из этих связей стрелочный терм в нормальной форме с теми же самыми связями. Теорема о нормальной форме и теорема когерентности гарантируют, что эти конструкции всегда могут быть получены. Например, если А есть порождающий объектный терм, то из связей

мы конструируем стрелочный терм в нормальной форме Ф^УССО,)))).

Наши связи также снабжают нас доказательством единственности нормальной формы, не прибегая при этом к чему-то вроде слияния редукций, т. е. свойству Чёрча-Россера. А именно, мы можем показать, что если И = Иг имеет место в А* или в*, и И и И г являются нормальными формами И и Иг соответственно, то И есть та же самая стрелка, что и И г.