Декартово замкнуті категорії — тип категорій у математиці у яких, грубо кажучи, кожен морфізм заданий на добутку двох об'єктів можна природно ідентифікувати із морфізмом на одному із множників. Декартово замкнуті категорії особливо широко використовуються у математичній логіці і програмуванні.

З точки зору програмування декартово замкнуті категорії реалізують інкапсуляції аргументів функцій — кожен аргумент представляється об'єктом категорії і використовується як чорний ящик. Разом з тим виразності декартово замкнутих категорій цілком достатньо, щоб оперувати з функціями способом, прийнятим в λ-численні. Це робить їх природними категорного моделями типізованого λ-числення.

Означення Категорія називається декартово замкнутою, якщо вона задовольняє трьом умовам:

У є термінальний об'єкт; Будь-які два об'єкти , в мають добуток ; Для будь-яких двох об'єктів і у існує експоненційний об'єкт .

Категорія, така, що для будь-якого її об'єкта категорія об'єктів над ним є декартово замкнутою, називається локально декартово замкнутою.

Приклади декартово замкнутих категорій

Категорія множин природним чином є декартово замкнутою категорією, оскільки функції з однієї множини в іншу утворюють множину і, отже, є об'єктом. Також в ній існують декартові добутки і термінальний об'єкт — синґлетон.

Якщо G є групою, то категорія всіх G-множин є декартово замкнутою. Якщо Y і Z є G-множинами, то ZY є множиною всіх функцій із Y у Z із дією G заданою як (g.F)(y) = g.(F(g−1.y)) для всіх g у G, F:Y → Z і y у Y.

Категорія всіх скінченних G-множин також є декартово замкнутою.

Категорія всіх малих категорій (і функторів, як морфізмів) є декартово замкнутою; експоненціалом є категорія функторів з у з натуральними перетвореннями, як морфізмами. Також існує категорія добутку і термінальний об'єкт — категорія з одного об'єкта і одного морфізма.

Елементарний топос є декартово замкнутою категорією за означенням.

Категорія топологічних просторів із неперервними відображеннями і категорія гладких многовидів із гладкими відображеннями не є декартово замкнутими. Прикладами декартово замкнутих категорій у топології є категорія компактно породжених гаусдорфових просторів і просторів Фролішера.

Алгебра Гейтінга також є стандартним прикладом декартово замкнутої категорії. Оскільки булева алгебра є її окремим випадком, вона теж завжди декартово замкнутою.

Основні побудови

Оцінювання

Згідно означення експоненційного об'єкта для об'єктів Z і Y існує морфізм оцінювання:

.

Зокрема для категорії множин цей морфізм має стандартний вигляд:

Більш загально можна побудувати часткове відображення:

Композиція

Нехай дано морфізм p : X → Y між двома об'єктами декартово замкнутої категорії. Тоді можна отримати також важливі морфізми між експоненційними об'єктами:

Для означення першого розглянемо експоненційні відображення і морфізми оцінювання: і Тоді також одержується морфізм і з універсальної властивості експоненційних об'єктів існує єдиний морфізм що задовольняє додаткові умови комутативності діаграм.

У другому випадку розглядаються функтори і Другий функтор одержується через функтор Згідно із універсальної властивості експоненційних об'єктів існує єдиний морфізм що задовольняє додаткові умови комутативності діаграм.

Для pZ також використовують позначення p* і p∘-, для Zp також p* і -∘p.

Для морфізмів оцінки можна отримати композицію

Із універсальної властивості експоненційного об'єкта звідси одержується морфізм

який називається відображенням композиції.

Для категорії множин таким чином одержується звичайна композиція відображень:

Перетини

Для морфізма p:X → Y, припустимо, що існує розшарований добуток:

де стрілка справа є pY а стрілка знизу відповідає одиничному морфізму на Y. Тоді ΓY(p) називається об'єктом перетинів p. Він часто також позначається ΓY(X).

Якщо ΓY(p) існує для всіх морфізмів p у Y, то можна ввести функтор ΓY : C/Y → C, що є правим спряженим до функтора добутків:

Експоненційний об'єкт можна також записати як:

Застосування У декартово замкнутій категорії «функція двох змінних» (морфізм ) завжди може бути представлена ​​як «функція однієї змінної» (морфізм ). У програмуванні ця операція відома як каррінг; це дозволяє інтерпретувати просто типізоване лямбда-числення в будь-якій декартово замкнутій категорії. Декартово замкнуті категорії є категорною моделлю для типізованого -числення і комбінаторної логіки.

Відповідність Каррі — Ховарда надає ізоморфізм між інтуїціоністською логікою, просто типізованим лямбда-численням і декартово замкнутими категоріями. Певні декартово замкнуті категорії (топоси) пропонувалися як основні об'єкти альтернативних основ математики замість традиційної теорії множин.

Див. також

Експоненційний об'єкт

Література

.