Полная версия

Главная arrow Логика arrow КАТЕГОРНАЯ ЛОГИКА

  • Увеличить шрифт
  • Уменьшить шрифт


<<   СОДЕРЖАНИЕ ПОСМОТРЕТЬ ОРИГИНАЛ   >>

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

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

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

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

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

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

Наконец, если h: С —> С2 имеет вид h20 /21 для Лр Ci -» С3 и Аг: Сз С2, то каждая связь в Л(Л) получается в из конечной

последовательности связей х2}, {ддозЬ {*3г*4},... , {*и-1г*л}> с и ? 1, в которой связи A(/?0 чередуются со связями Л(Л2) (в этой последовательности имеется по меньшей мере одна связь из Л(А|) или A.(hi)). Вершины х и хп представляют собой вхождения F или G в Ci или Ci и если п > 3, то все *2, ... , х„. являются вхождениями F или G в С3. Легко видеть, что не может быть последовательности связей вида х2}, {хх3}, ... , {х2пЛух2п}, {x2n^i} с п > 1, в которой все jcj, ..., х2п представляют собой вхождения F или G в С3.

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

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

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

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

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

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

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

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

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

мы конструируем стрелочный терм в нормальной форме

Ф^УССО,)))).

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

 
<<   СОДЕРЖАНИЕ ПОСМОТРЕТЬ ОРИГИНАЛ   >>