Декартова закрытая категория - Cartesian closed category

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

Этимология

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

Определение

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

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

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

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

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

который является естественным в обоих X и Z .

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

Если категория обладает тем свойством, что все ее категории срезов являются декартово замкнутыми, то она называется локально декартово замкнутой . Обратите внимание, что если 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 ^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 }}}

где стрелка справа есть р ^Y и стрелка на дне соответствует идентичности на Y . Тогда Γ _Y ( р ) называется объектом секций из р . Часто его обозначают сокращенно Γ _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 всех множеств с функциями как морфизмами декартово замкнута. Продукт Х × 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 ⁻¹ .y)) для все г в G , F : Y → Z и Y в Y .
Категория конечных G -множеств также декартово замкнута.
Категория Cat всех малых категорий (с функторами как морфизмами) декартово замкнута; экспонента C ^D задается категорией функторов, состоящей из всех функторов из D в C , с естественными преобразованиями как морфизмами.
Если C - малая категория , то категория функторов Set ^C, состоящая из всех ковариантных функторов из C в категорию множеств с естественными преобразованиями как морфизмы, декартово замкнута. Если Р и О являются два функтора из C в Set , то экспоненциальный F ^G является функтор, значение которого на объекте X из С задается набором всех естественных преобразований из ( Х , -) × G к F .
- Предыдущий пример G -множеств можно рассматривать как частный случай категорий функторов: каждую группу можно рассматривать как категорию с одним объектом, а G -множества - не что иное, как функторы из этой категории в Set
- Категория всех ориентированных графов декартово замкнута; это категория функторов, как объясняется в разделе категория функторов.
- В частности, категория симплициальных множеств (которые являются функторами X : ∆ ^op → Set ) декартово замкнута.
В более общем смысле, каждый элементарный топос является декартово замкнутым.
В алгебраической топологии с декартовыми замкнутыми категориями особенно легко работать. Ни категория топологических пространств с непрерывными отображениями, ни категория гладких многообразий с гладкими отображениями не являются декартово замкнутыми. Поэтому были рассмотрены замещающие категории: категория компактно порожденных хаусдорфовых пространств декартово замкнута, как и категория пространств Фрелихера .
В теории порядка , полные частичные порядки ( фо s) имеет естественную топологию, в топологию Скотта , чья непрерывных отображения делают образует декартову замкнутую категорию (то есть, объекты являются НСП, а морфизмы являются непрерывными Скоттами карты). Как каррирование, так и применение являются непрерывными функциями в топологии Скотта, а каррирование вместе с применением обеспечивает сопряженные функции.
Гейтингова алгебра является декартовым замкнута (ограниченной) решетка . Важный пример возникает из топологических пространств. Если X - топологическое пространство, то открытые множества в X образуют объекты категории O ( X ), для которой существует единственный морфизм из U в V, если U является подмножеством V, и без морфизма в противном случае. Это ч.у.м. является декартово замкнутой категории: «продукт» из U и V представляет собой пересечение U и V и экспоненциального U ^V является внутренним из $U ∪ ( X \ V )$ .
Категория с нулевым объектом является декартово замкнутой тогда и только тогда, когда она эквивалентна категории только с одним объектом и одним морфизмом идентичности. В самом деле, если 0 - начальный объект, а 1 - конечный объект, а у нас есть , то он имеет только один элемент. ${\ displaystyle 0 \ cong 1}$ ${\ displaystyle 0 \ cong 1}$ ${\ Displaystyle \ mathrm {Hom} (X, Y) \ cong \ mathrm {Hom} (1, Y ^ {X}) \ cong \ mathrm {Hom} (0, Y ^ {X}) \ cong 1}$ ${\ Displaystyle \ mathrm {Hom} (X, Y) \ cong \ mathrm {Hom} (1, Y ^ {X}) \ cong \ mathrm {Hom} (0, Y ^ {X}) \ cong 1}$
- В частности, любая нетривиальная категория с нулевым объектом, например абелева категория , не является декартово замкнутой. Таким образом, категория модулей над кольцом не является декартово замкнутой. Однако у функторного тензорного произведения с фиксированным модулем есть правый сопряженный элемент . Тензорное произведение не является категориальным произведением, поэтому это не противоречит сказанному выше. Вместо этого мы получаем, что категория модулей моноидально замкнута . ${\ displaystyle - \ otimes M}$

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

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

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

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

Приложения

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

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

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

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

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

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

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

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

Правый сопряженный продукт называется зависимым произведением . ${\ displaystyle \ Pi _ {p}: от C / X \ до 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 _ {х: P (y)}}$ ${\ Displaystyle \ Pi _ {х: P (y)}}$

Теория уравнений

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

( х ^у ) ^г = ( х ^г ) ^у .

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

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

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

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

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

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

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

Декартова закрытая категория в nLab
Сообщение в блоге о взаимосвязи между CCC и лямбда-исчислением : https://golem.ph.utexas.edu/category/2006/08/cartesian_closed_categories_an_1.html

[1] Джон К. Баез и Майк Стэй, " Физика, топология, логика и вычисления: Розеттский камень ", (2009) ArXiv 0903.0340 в New Structures for Physics , ed. Bob Coecke, Lecture Notes in Physics vol. 813 , Springer, Берлин, 2011 г., стр. 95-174.

[2] Перейти ↑ Saunders., Mac Lane (1978). Категории для рабочего математика (второе изд.). Нью-Йорк, штат Нью-Йорк: Springer New York. ISBN 1441931236. OCLC 851741862 .

[3] "декартова закрытая категория в nLab" . ncatlab.org . Проверено 17 сентября 2017 .

[4] Локально декартова закрытая категория в nLab

[5] HP Barendregt, The Lambda Calculus , (1984) North-Holland ISBN 0-444-87508-5 (см. Теорему 1.2.16)

[6] "Ct.category theory - декартова замкнутая категория коммутативных моноидов?" .

[7] С. Соловьев. "Категория конечных множеств и декартовы замкнутые категории", Журнал советской математики, 22, 3 (1983)

[8] Фиоре, Космо и Балат. Замечания об изоморфизмах типизированных лямбда-исчислений с пустым типом и типом суммы [1]

Languages

In other projects