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

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

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

Означення

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

У $C$ є термінальний об'єкт;
Будь-які два об'єкти $X$ , $Y$ в $C$ мають добуток $X \times 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 \times Y \to Z$ ) завжди може бути представлена як «функція однієї змінної» (морфізм $λ f : X \to 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.

This article is issued from Wikipedia. The text is licensed under Creative Commons - Attribution - Sharealike. Additional terms may apply for the media files.