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

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

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

ОзначенняРедагувати

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

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

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

  • Категорія множин природним чином є декартово замкнутою категорією, оскільки функції з однієї множини в іншу утворюють множину і, отже, є об'єктом. Також в ній існують декартові добутки і термінальний об'єкт — синґлетон.
  • Якщо G є групою, то категорія всіх G-множин є декартово замкнутою. Якщо Y і Z є G-множинами, то ZY є множиною всіх функцій із Y у Z із дією G заданою як (g.F)(y) = g.(F(g−1.y)) для всіх g у G, F:YZ і y у Y.
  • Категорія всіх скінченних G-множин також є декартово замкнутою.
  • Категорія Cat всіх малих категорій (і функторів, як морфізмів) є декартово замкнутою; експоненціалом CD є категорія функторів з D у C з натуральними перетвореннями, як морфізмами. Також існує категорія добутку і термінальний об'єкт — категорія 1 з одного об'єкта і одного морфізма.
  • Алгебра Гейтінга також є стандартним прикладом декартово замкнутої категорії. Оскільки булева алгебра є її окремим випадком, вона теж завжди декартово замкнутою.

Основні побудовиРедагувати

ОцінюванняРедагувати

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

 .

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

 

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

 

КомпозиціяРедагувати

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

 
 

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

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

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

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

 

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

 

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

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

 

ПеретиниРедагувати

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

 

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

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

 

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

 

ЗастосуванняРедагувати

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

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

Див. такожРедагувати

ЛітератураРедагувати