Декартово замкнутая категория

Тип категории в теории категорий

В теории категорий категория является декартово замкнутой, если , грубо говоря, любой морфизм, определенный на произведении двух объектов, может быть естественным образом отождествлен с морфизмом, определенным на одном из факторов. Эти категории особенно важны в математической логике и теории программирования, поскольку их внутренний язык — это просто типизированное лямбда-исчисление . Они обобщаются замкнутыми моноидальными категориями , внутренний язык которых, линейные системы типов , подходят как для квантовых , так и для классических вычислений. ^[1]

Этимология

Назван в честь Рене Декарта (1596–1650), французского философа, математика и ученого, чья формулировка аналитической геометрии привела к возникновению понятия декартова произведения , которое позднее было обобщено до понятия категориального произведения .

Определение

Категория C называется декартово замкнутой ^[2] тогда и только тогда, когда она удовлетворяет следующим трем свойствам:

• Имеет конечный объект .
• Любые два объекта X и Y из C имеют произведение X  × Y в C.
• Любые два объекта Y и Z из C имеют экспоненциальную функцию Z ^Y в C .

Первые два условия можно объединить в одно требование, чтобы любое конечное (возможно пустое) семейство объектов C допускало произведение в C , ввиду естественной ассоциативности категориального произведения и потому, что пустое произведение в категории является конечным объектом этой категории.

Третье условие эквивалентно требованию, чтобы функтор – × Y (т. е. функтор из C в C , который отображает объекты X в X  × Y и морфизмы φ в φ × id _Y ) имел правый сопряженный , обычно обозначаемый – ^Y , для всех объектов Y в C . Для локально малых категорий это можно выразить существованием биекции между hom -множествами

${\displaystyle \mathrm {Hom} (X\times Y,Z)\cong \mathrm {Hom} (X,Z^{Y})}$

что естественно в X , Y и Z. ^[3 ]

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

Если категория обладает тем свойством, что все ее категории срезов являются декартово замкнутыми, то она называется локально декартово замкнутой . ^[4] Обратите внимание, что если C является локально декартово замкнутой, она не обязательно должна быть декартово замкнутой; это происходит тогда и только тогда, когда C имеет конечный объект.

Базовые конструкции

Оценка

Для каждого объекта Y единица экспоненциального присоединения является естественным преобразованием

${\displaystyle \mathrm {ev} _{Y,Z}:Z^{Y}\times Y\to Z}$

называется (внутренней) оценочной картой. В более общем смысле, мы можем построить частичную карту применения как составную

${\displaystyle \mathrm {papply} _{X,Y,Z}:Z^{X\times Y}\times X\cong (Z^{Y})^{X}\times X{\xrightarrow {\mathrm {ev} _{X,Z^{Y}}}}Z^{Y}.}$

В частном случае категории Set они сводятся к обычным операциям:

${\displaystyle \mathrm {ev} _{Y,Z}(f,y)=f(y).}$

Состав

Оценка экспоненты с одним аргументом при морфизме p  : X → Y дает морфизмы

${\displaystyle p^{Z}:X^{Z}\to Y^{Z},}$

${\displaystyle Z^{p}:Z^{Y}\to Z^{X},}$

соответствующие операции композиции с p . Альтернативные обозначения для операции p ^Z включают p _* и p∘- . Альтернативные обозначения для операции Z ^p включают p ^* и -∘p .

Оценочные карты могут быть объединены в цепочку следующим образом:

${\displaystyle Z^{Y}\times Y^{X}\times X{\xrightarrow {\mathrm {id} \times \mathrm {ev} _{X,Y}}}Z^{Y}\times Y{\xrightarrow {\mathrm {ev} _{Y,Z}}}Z}$

соответствующая стрелка под экспоненциальным присоединением

${\displaystyle c_{X,Y,Z}:Z^{Y}\times Y^{X}\to Z^{X}}$

называется (внутренней) композиционной картой.

В частном случае категории Set это обычная операция композиции:

${\displaystyle c_{X,Y,Z}(g,f)=g\circ f.}$

Разделы

Для морфизма p : X → Y предположим, что существует следующий квадрат обратного проецирования, который определяет подобъект X ^Y , соответствующий отображениям, композиция которых с p является тождеством:

${\displaystyle {\begin{array}{ccc}\Gamma _{Y}(p)&\to &X^{Y}\\\downarrow &&\downarrow \\1&\to &Y^{Y}\end{array}}}$

где стрелка справа — это p ^Y , а стрелка снизу соответствует тождеству на Y . Тогда Γ _Y ( p ) называется объектом сечений p . Его часто сокращают до Γ _Y ( X ).

Если Γ _Y ( p ) существует для каждого морфизма p с областью значений Y , то его можно собрать в функтор Γ _Y  : C / Y → C на категории срезов, который является правым сопряженным к варианту функтора произведения:

${\displaystyle \hom _{C/Y}(X\times Y{\xrightarrow {\pi _{2}}}Y,Z{\xrightarrow {p}}Y)\cong \hom _{C}(X,\Gamma _{Y}(p)).}$

Экспоненту по Y можно выразить через сечения:

${\displaystyle Z^{Y}\cong \Gamma _{Y}(Z\times Y{\xrightarrow {\pi _{2}}}Y).}$

Примеры

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

• Категория Set всех множеств с функциями в качестве морфизмов является декартово замкнутой. Произведение X × Y является декартовым произведением X и Y , а Z ^Y является множеством всех функций из Y в Z . Сопряженность выражается следующим фактом: функция f :  X × Y → Z естественным образом отождествляется с каррированной функцией g  : X → Z ^Y , определяемой как g ( x )( y ) = f ( x , y ) для всех x из X и y из Y .
• Категория конечных множеств с функциями в качестве морфизмов является декартово замкнутой по той же причине.
• Если G — группа , то категория всех G -множеств декартово замкнута. Если Y и Z — два G -множества, то Z ^Y — множество всех функций из Y в Z с действием G , определяемым формулой ( g.F ) ( y ) = g.F ( g ⁻ 1.y ) для всех g в G , F : Y → Z и y в Y.
• Категория конечных G -множеств также декартово замкнута.
• Категория Cat всех малых категорий (с функторами в качестве морфизмов) является декартово замкнутой; экспонента C ^D задается категорией функторов, состоящей из всех функторов из D в C , с естественными преобразованиями в качестве морфизмов.
• Если C — малая категория , то функторная категория Set ^C, состоящая из всех ковариантных функторов из C в категорию множеств с естественными преобразованиями в качестве морфизмов, является декартово замкнутой. Если F и G — два функтора из C в Set , то экспонента F ^G — это функтор , значение которого на объекте X категории C задается множеством всех естественных преобразований из ( X ,−) ×  G в F.
  • Предыдущий пример G -множеств можно рассматривать как частный случай категорий функторов: каждую группу можно рассматривать как категорию с одним объектом, а G -множества — это не что иное, как функторы из этой категории в Set.
  • Категория всех ориентированных графов является декартово замкнутой; это категория функторов, как объяснено в категории функторов.
  • В частности, категория симплициальных множеств (являющихся функторами X  : Δ ^op → Set ) декартово замкнута.
• Еще более обобщенно, каждый элементарный топос является декартово замкнутым.
• В алгебраической топологии с декартово замкнутыми категориями работать особенно легко. Ни категория топологических пространств с непрерывными отображениями, ни категория гладких многообразий с гладкими отображениями не являются декартово замкнутыми. Поэтому были рассмотрены заменяющие категории: категория компактно порожденных хаусдорфовых пространств является декартово замкнутой, как и категория пространств Фрёлихера .
• В теории порядка полные частичные порядки ( cpo s) имеют естественную топологию, топологию Скотта , чьи непрерывные отображения образуют декартову замкнутую категорию (то есть объекты являются cpos, а морфизмы являются непрерывными отображениями Скотта ). И каррирование , и применение являются непрерывными функциями в топологии Скотта, а каррирование вместе с применением обеспечивают сопряженную функцию. ^[5]
• Алгебра Гейтинга — это декартово замкнутая (ограниченная) решетка . Важный пример возникает из топологических пространств. Если X — топологическое пространство, то открытые множества в X образуют объекты категории O( X ), для которой существует единственный морфизм из U в V , если U — подмножество V , и нет морфизма в противном случае. Этот частично упорядоченный набор является декартово замкнутой категорией: «произведение» U и V — это пересечение U и V , а экспонента U ^V — это внутренность U ∪ ( X \ V ) .
• Категория с нулевым объектом является декартово замкнутой тогда и только тогда, когда она эквивалентна категории с единственным объектом и одним тождественным морфизмом. Действительно, если 0 — начальный объект, а 1 — конечный объект, и мы имеем , то которая имеет только один элемент. ^[6] ${\displaystyle 0\cong 1}$ ${\displaystyle \mathrm {Hom} (X,Y)\cong \mathrm {Hom} (1,Y^{X})\cong \mathrm {Hom} (0,Y^{X})\cong 1}$
  • В частности, любая нетривиальная категория с нулевым объектом, такая как абелева категория , не является декартово замкнутой. Поэтому категория модулей над кольцом не является декартово замкнутой. Однако тензорное произведение функтора с фиксированным модулем имеет правый сопряженный . Тензорное произведение не является категорическим произведением, поэтому это не противоречит вышесказанному. Вместо этого мы получаем, что категория модулей является моноидально замкнутой . ${\displaystyle -\otimes M}$

Примерами локально декартовых замкнутых категорий являются:

• Каждый элементарный топос локально декартово замкнут. Этот пример включает Set , FinSet , G -множества для группы G , а также Set ^C для малых категорий C .
• Категория LH, объектами которой являются топологические пространства, а морфизмами — локальные гомеоморфизмы , локально декартово замкнута, поскольку LH/X эквивалентна категории пучков ⁠ ⁠ ${\displaystyle Sh(X)}$ . Однако LH не имеет конечного объекта и, таким образом, не является декартово замкнутой.
• Если C имеет обратные образы и для каждой стрелки p  : X → Y функтор p ^*  : C/Y → C/X, заданный взятием обратных образов, имеет правый сопряженный, то C локально декартово замкнут.
• Если C локально декартово замкнуто, то все его категории срезов C/X также локально декартово замкнуты.

Примерами локально декартово замкнутых категорий являются:

• Кот не является локально декартово замкнутым.

Приложения

В декартовых замкнутых категориях «функция двух переменных» (морфизм f  : X × Y → Z ) всегда может быть представлена ​​как «функция одной переменной» (морфизм λ f  : X → Z ^Y ). В приложениях компьютерных наук это известно как каррирование ; это привело к осознанию того, что просто типизированное лямбда-исчисление может быть интерпретировано в любой декартовой замкнутой категории.

Соответствие Карри–Ховарда–Ламбека обеспечивает глубокий изоморфизм между интуиционистской логикой, просто типизированным лямбда-исчислением и декартовыми замкнутыми категориями.

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

Специалист по информатике Джон Бэкус выступает за свободную от переменных нотацию, или программирование на уровне функций , которое в ретроспективе имеет некоторое сходство с внутренним языком декартовых замкнутых категорий. ^[7] CAML более осознанно смоделирован на основе декартовых замкнутых категорий.

Зависимая сумма и произведение

Пусть C — локально декартово замкнутая категория. Тогда C имеет все обратные пути, поскольку обратный путь двух стрелок с областью значений Z задается произведением в C/Z .

Для каждой стрелки p  : X → Y пусть P обозначает соответствующий объект C/Y . Взятие обратных прогонов вдоль p дает функтор p ^*  : C/Y → C/X , который имеет как левый, так и правый сопряженный.

Левая сопряженная сумма называется зависимой суммой и задается композицией . ${\displaystyle \Sigma _{p}:C/X\to C/Y}$ ${\displaystyle p\circ (-)}$

Правый сопряженный элемент называется зависимым произведением . ${\displaystyle \Pi _{p}:C/X\to C/Y}$

Экспонента по P в C/Y может быть выражена через зависимое произведение по формуле . ${\displaystyle Q^{P}\cong \Pi _{p}(p^{*}(Q))}$

Причина этих названий в том, что при интерпретации P как зависимого типа функторы и соответствуют образованиям типов и соответственно. ${\displaystyle y:Y\vdash P(y):\mathrm {Type} }$ ${\displaystyle \Sigma _{p}}$ ${\displaystyle \Pi _{p}}$ ${\displaystyle \Sigma _{x:P(y)}}$ ${\displaystyle \Pi _{x:P(y)}}$

Эквациональная теория

В каждой декартовой замкнутой категории (используя экспоненциальную запись), ( X ^Y ) ^Z и ( X ^Z ) ^Y изоморфны для всех объектов X , Y и Z . Запишем это как «уравнение »

( х ^у ) ^z = ( х ^z ) ^у .

Можно спросить, какие еще такие уравнения справедливы во всех декартовых замкнутых категориях. Оказывается, все они логически вытекают из следующих аксиом: ^[8]

• х ×( у × z ) = ( х × y )× z
• х × у = у × х
• x ×1 = x (здесь 1 обозначает конечный объект C )
• 1 ^х = 1
• х ¹ = х
• ( х × у ) ^z = х ^z × у ^z
• ( х ^у ) ^z = х ^{( у × z )}

Бикартезовские закрытые категории

Бикартезовы замкнутые категории расширяют декартовы замкнутые категории с бинарными копроизведениями и начальным объектом , с произведениями, распределяющимися по копроизведениям. Их эквациональная теория расширяется следующими аксиомами, что приводит к чему-то похожему на школьные аксиомы Тарского , но с нулем:

• х + у = у + х
• ( х + у ) + z = х + ( у + z )
• х ×( у + z ) = х × у + х × z
• х ^{( у + z )} = х ^у × х ^z
• 0 + х = х
• х ×0 = 0
• х ⁰ = 1

Однако следует отметить, что приведенный выше список не является полным; изоморфизм типов в свободном BCCC не является конечно аксиоматизируемым, и его разрешимость все еще остается открытой проблемой. ^[9]

Ссылки

1. Baez, John C. ; Stay, Mike (2011). "Физика, топология, логика и вычисления: Розеттский камень" (PDF) . В Coecke, Bob (ред.). Новые структуры для физики . Lecture Notes in Physics. Vol. 813. Springer. стр. 95–174. arXiv : 0903.0340 . CiteSeerX  10.1.1.296.1044 . doi :10.1007/978-3-642-12821-9_2. ISBN 978-3-642-12821-9. S2CID  115169297.
2. Saunders, Mac Lane (1978). Категории для работающего математика (2-е изд.). Springer. ISBN 1441931236. OCLC  851741862.
3. "декартово замкнутая категория в nLab". ncatlab.org . Получено 2017-09-17 .
4. Локально декартово замкнутая категория в n Lab
5. Барендрегт, HP (1984). «Теорема 1.2.16». Лямбда-исчисление . Северная Голландия. ISBN 0-444-87508-5.
6. "Теория категорий Ct. - является ли категория коммутативных моноидов декартово замкнутой?".
7. Бэкус, Джон (1981). Программы функционального уровня как математические объекты . Нью-Йорк, Нью-Йорк, США: ACM Press. doi :10.1145/800223.806757.
8. Соловьев, СВ (1983). «Категория конечных множеств и декартово замкнутые категории». J Math Sci . 22 (3): 1387–1400. doi :10.1007/BF01084396. S2CID  122693163.
9. Fiore, M.; Cosmo, R. Di; Balat, V. (2006). «Замечания об изоморфизмах в типизированных лямбда-исчислениях с пустыми и суммами типов» (PDF) . Annals of Pure and Applied Logic . 141 (1–2): 35–50. doi :10.1016/j.apal.2005.09.001.

• Seely, RAG (1984). «Локально декартовы замкнутые категории и теория типов». Математические труды Кембриджского философского общества . 95 (1): 33–48. doi :10.1017/S0305004100061284. ISSN  1469-8064. S2CID  15115721.

Внешние ссылки

• Декартово закрытая категория в n Lab
• Баез, Джон (2006). «CCC и λ-исчисление». Кафе n-Category: групповой блог по математике, физике и философии . Техасский университет.