Применения логических исчислений к изучению естественных преобразований в категориях Соловьев, Сергей Владимирович

Краткое описание

Соловьев, Сергей Владимирович.
Применения логических исчислений к изучению естественных преобразований в категориях : диссертация ... кандидата физико-математических наук : 01.01.06. - Ленинград, 1984. - 157 с. : ил.
Оглавление диссертациикандидат физико-математических наук Соловьев, Сергей Владимирович
ВВЕДЕНИЕ
I. Одаой из важных тем общей теории категорий является изучение естественных преобразований б категориях, снабженных дополнительнойктурой, состоящей из выделенных объектов, выделенных функторов (чаще всего в этой роли фигурировали функторы типа тензорного произведения, внутреннего 1гопг -функтора, прямой суммы или прямого произведения) и выделенных естественных преобразований (типа естественного изоморфизма коммутативности тензорного произведения, естественного изоморфизма сопряженности тензорного произведения и внутреннего К^-функтора, или естественных проекций прямого произведения), при условии, что все эти данные подчиняются определенным соотношениям (скажем, ОС - , где С обозначает естественный изоморфизм коммутативности тензорного произведения)
В диссертации к проблемам этой тематики применяется ряд методов и конструкций, "подсказанных" математической логикой (теорией доказательств, теорией формальных систем) и на этой основе решен ряд конкретных задач, касающихся естественных преобразований суперпозиций выделенных функторов в категориях с дополнительной структурой.
История воцроса восходит к началу 60-х годов (см. [I] ). Естественные преобразования в категориях с дополнительной структурой активно изучались с того времени С.Маклейном, С. Эйленбергом, И.Ламбе-ком и рядом других математиков (см., например, [2] , [3] , [5] , [8] , [18] , [29] , [30] ).
Рассматривались в основном задачи, связанные с естественными преобразованиями, которые могут быть представлены некоторыми термами, построенными из символов выделенных естественных, преобразований при помощи символов выделенных функторов и символа композиции (тавив естественные преобразования мы будем называть, в духе работ С.Маклейна [2] , [25] каноническими естественными преобразованиями; их точное определение для рассматриваемых в этой работе типов категорий дается ниже, в
§ 2), в частности задачи о корегентнооти канонических естественных цреобразований (верно ли, что все диаграммы в том иди ином классе диаграмм канонических естественных цреобразований комздутативны).
Полученные результаты находили применение в различных областях математики: ври построении бесконечнократннх пространств петель в алгебраической топологии (см. [2] , [4] , [5] ); при построении "длинных точных последовательностей" в гомологической алгебре [6]; при определении операций Стинрода в абелевых категориях [7] и т.д. Н.П.Титов нашел неожиданные применения результатов о когерентности к вопросам описания работы систем ЭВМ [8 ] •
2. В ряде случаев для решения задач упомянутых типов с успехом применялась теория исчислений. Связующим звеном между теорией категорий и теорией исчислений служит тот факт, что с классом категорий, имеющих заданную дополнительную структуру, может быть связано (вообще говоря, многими способами) некоторое исчисление секвенциального типа, которое оказывается свободной категорией того же класса при следующем "распределении ролей": формулы играют роль объектов; роль морсоизмов из А в В отводится класоам эквивалентных друг другу выводов секвенции А-В (или их кодов) при некотором отношении эквивалентности =■ , оцределяемом на основании соотношений, выполнение которых требуется в рассматриваемом классе категорий (в частности, класс эквивалентности аксиомы А^А играет роль единичного морфизма); роль композиции играет правило сечэния ——^—^ ; роль функторов играют пропозициональные связки (на объектах) и правила введения соответствующей связки на морфизмах); роль естественных преобразований играют схемы аксиом или иногда (например, для изоморфизмов сопряженности) правила вывода.
Впервые, по-видимому, начал применять исчисления для изучения канонических естественных преобразований И.Ламбек (см. [9] - [И]), обнаруживший не только связь мевду исчислениями и категориями, имевшую описанный выше характер, но и то, что исчислениям, рассматриваемым в связи со шогими интересными классами категорий, можно придать формулировку, допускающую применение хорошо известных методов теории доказательств, например, устранение сечения. Ряд дальнейшие результатов можно найти в статьях [з] , [12] - [16] и в книге [17] • В [17] описываются исчисления, отвечающие большинству представленных в литературе вариантов дополнительной структуры в категориях. (В основном эти исчисления оказались близки к различным фрагментам интуиционистского исчисления высказываний).
3. Однако предоставляемые теорией исчислений возможности использовались не в полном объеме. Привлекаемая в этих работах техника теории исчислений сводилась в основном к различным вариантам теорем об устранимости сечения (в исчислениях генценовокого) типа и о нормализуемости выводов (в исчислениях натурального типа, чему соответствовала возможность обойтись без композиций (за исключением некоторых специальных случаев) в термах, представлящих канонические естественные преобразования.
В данной диссертации рассматривается и решается ряд новых задач теории категорий (и некоторые ранее известные); при этом используются некоторые методы теории исчислений, которые раньше в этой связи не применялись. Среди новых задач теории категорий рассматривается* например, задача описания всех (а не только канонических) естественных преобразований всевозможных суперпозиций виделенных функторов над данной категорией. В тех случаях, когда удается решить ее (скажем, для категории конечнопорозденных проективных модулей над кашутативным кольцом 1 с I и суперпозиций &х и кот; ) теория исчислений помогает свести общий случай к сравнительно несложным алгебраическим теоремам. Из ранее не применявшихся в такш направлении методов теории исчислений отметим преобразования выводов, включающие (в отличие от процедуры устранения сечения) преобразование конечной секвенции (особую роль будут играть операции, обладающие некоторыми свойствами обратимости); анализ "зацеплений" вхождений переменных в секвенцию; метод оценок (придания истинных значений пропозициональным переменным).