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

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

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

Означення

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

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

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

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

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

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

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

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

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

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

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

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

Оцінювання

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

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

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

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

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

$\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}.$

Композиція

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

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

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

Для означення першого розглянемо експоненційні відображення і морфізми оцінювання: $\mathrm {ev} _{Z,X}:X^{Z}\times Z\to X$ і $\mathrm {ev} _{Z,Y}:Y^{Z}\times Z\to Y.$ Тоді також одержується морфізм $g\circ \mathrm {ev} _{Z,X}:X^{Z}\times Z\to Y$ і з універсальної властивості експоненційних об'єктів існує єдиний морфізм $p^{Z}:X^{Z}\to Y^{Z},$ що задовольняє додаткові умови комутативності діаграм.

У другому випадку розглядаються функтори $\mathrm {ev} _{X,Z}:Z^{X}\times X\to Z$ і $\mathrm {ev} _{Y,Z}:Z^{Y}\times Y\to Z.$ Другий функтор одержується через функтор $id\times g\circ \mathrm {ev} _{Y,Z}:Z^{Y}\times X\to Z.$ Згідно із універсальної властивості експоненційних об'єктів існує єдиний морфізм $Z^{p}:Z^{Y}\to Z^{X},$ що задовольняє додаткові умови комутативності діаграм.

Для p^Z також використовують позначення p_* і p∘-, для Z^p також p^* і -∘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}$

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

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

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

Перетини

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

${\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, що є правим спряженим до функтора добутків:

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

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

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

Застосування

У декартово замкнутій категорії «функція двох змінних» (морфізм f: X×Y → Z) завжди може бути представлена ​​як «функція однієї змінної» (морфізм λf : X → Z^Y). У програмуванні ця операція відома як каррінг; це дозволяє інтерпретувати просто типізоване лямбда-числення в будь-якій декартово замкнутій категорії. Декартово замкнуті категорії є категорною моделлю для типізованого $\lambda$-числення і комбінаторної логіки.

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

Див. також

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

Література

• Awodey, Steve (2006), Category theory, Oxford logic guides, т. 49, Oxford University Press, ISBN 978-0-19-856861-2.
• Crole, Roy L. (1994). Categories for Types. Cambridge University Press. ISBN 0521450926.
• Lambek, Joachim; Scott, P.J. (1986). Introduction to Higher Order Categorical Logic. Cambridge Studies in Advanced Mathematics. Т. 7. Cambridge University Press. ISBN 0-521-35653-9.
• Pierce, Benjamin C. (1991). Basic Category Theory for Computer Scientists. MIT Press. ISBN 978-0-262-66071-6. Архів оригіналу за 25 квітня 2021. Процитовано 18 березня 2020.