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

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

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

Означення

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

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

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

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

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

• Якщо 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-множин також є декартово замкнутою.

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

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

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

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

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

Оцінювання

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

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

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

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

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

${\mathrm{p}\mathrm{a}\mathrm{p}\mathrm{p}\mathrm{l}\mathrm{y}}_{X,Y,Z}:Z^{X\times Y}\times X\cong (Z^Y{)}^X\times X\stackrel{{\mathrm{e}\mathrm{v}}_{X,Z^Y}}{\to }{Z}^Y.$

Композиція

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

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

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

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

У другому випадку розглядаються функтори ${\mathrm{e}\mathrm{v}}_{X,Z}:Z^X\times X\to Z$ і ${\mathrm{e}\mathrm{v}}_{Y,Z}:Z^Y\times Y\to Z.$ Другий функтор одержується через функтор $id\times g\circ {\mathrm{e}\mathrm{v}}_{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\stackrel{\mathrm{i}\mathrm{d}\times {\mathrm{e}\mathrm{v}}_{X,Y}}{\to }{Z}^Y\times Y\stackrel{{\mathrm{e}\mathrm{v}}_{Y,Z}}{\to }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}{\mathrm{\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, що є правим спряженим до функтора добутків:

${\mathrm{hom}}_{C/Y}(X\times Y\stackrel{{\pi }_2}{\to }Y,Z\stackrel{p}{\to }Y)\cong {\mathrm{hom}}_C(X,{\mathrm{\Gamma }}_Y(p)).$

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

$Z^Y\cong {\mathrm{\Gamma }}_Y(Z\times Y\stackrel{{\pi }_2}{\to }Y).$

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

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

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

Див. також

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

Література

• Шаблон:Citation.
• Шаблон:Cite book
• Шаблон:Cite book
• Шаблон:Cite book