Декартова закрытая категория

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

Этимология

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

Определение

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

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

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

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

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

что естественно в X , Y и Z. ​

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

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

Основные конструкции

Оценка

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

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

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

$\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 они сводятся к обычным операциям:

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

Состав

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

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

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

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

Карты оценки могут быть объединены в цепочку:

$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$

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

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

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

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

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

Разделы

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

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

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

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

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

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

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

Примеры

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

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

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

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

Непримеры локально декартовых замкнутых категорий включают:

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

Приложения

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

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

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

Ученый-компьютерщик Джон Бэкус выступает за нотацию без переменных, или программирование на функциональном уровне , которое, оглядываясь назад, имеет некоторое сходство с внутренним языком декартовых замкнутых категорий. CAML более сознательно моделируется на основе декартовых закрытых категорий.

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

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

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

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

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

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

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

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

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

( х ^и ) ^С = ( х ^С ) ^и .

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

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

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

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

• х + у = у + х
• ( Икс + у ) + z знак равно Икс + ( у + z )
• Икс ×( у + z ) = Икс × у + Икс × z
• х ^{( у + г )} = х ^и ×x ^С
• 0 + х = х
• x ×0 = 0
• х ⁰ = 1

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

Ссылки

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

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

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