В теории категорий объект натуральных чисел ( NNO ) - это объект, наделенный рекурсивной структурой, подобной натуральным числам . Точнее, в категории E с конечным объектом 1 NNO N задается следующим образом:
- глобальный элемент г : 1 → N , и
- стрелка s : N → N ,
такая, что для любого объекта A из E , глобального элемента q : 1 → A и стрелки f : A → A существует единственная стрелка u : N → A такая, что:
Другими словами, треугольник и квадрат на следующей диаграмме коммутируют.
Пара ( q , f ) иногда называется рекурсивными данными для u , заданными в форме рекурсивного определения :
- ⊢ u ( z ) = q
- y ∈ E N ⊢ u ( s y ) = f ( u ( y ))
Приведенное выше определение является универсальным свойством NNO, то есть они определены с точностью до канонического изоморфизма . Если стрелка u, как определено выше, просто должна существовать, то есть уникальность не требуется, то N называется слабым NNO.
Эквивалентные определения
NNO в декартовых замкнутых категориях (CCC) или топоах иногда определяются следующим эквивалентным способом (из-за Ловера ): для каждой пары стрелок g : A → B и f : B → B существует единственный h : N × A → B такие, что квадраты на следующей диаграмме коммутируют. [4]
Эта же конструкция определяет слабые NNO в декартовых категориях, которые не являются декартово замкнутыми.
В категории с терминальным объектом 1 и бинарными копроизведениями (обозначаемых +), AN NNO может быть определен как исходная алгебра в endofunctor , который действует на объектах с помощью X ↦ 1 + X и на стрелки с помощью F ↦ [ID 1 , х ] . [5]
Характеристики
- Каждый НСО является исходным объектом категории диаграмм вида
- Если декартово замкнутая категория имеет слабые NNO, то каждый ее фрагмент также имеет слабые NNO.
- ННО могут быть использованы для нестандартных моделей в теории типа в аналогично тому , нестандартные модели анализа. Такие категории (или топои) имеют тенденцию иметь «бесконечно много» нестандартных натуральных чисел. [ требуется пояснение ] (Как всегда, есть простые способы получить нестандартные NNO; например, если z = sz , и в этом случае категория или топос E тривиальны.)
- Фрэйд показал , что г и s образуют копроизведение диаграмму для ННО; также, ! N : N → 1 представляет собой коуравнитель из й и 1 Н , то есть , каждая пара глобальных элементов N соединена посредством S ; кроме того, эта пара фактов характеризует все ННО.
Примеры
- В Set , категории множеств , стандартные натуральные числа - это NNO. [6] Терминальный объект в Set является синглтоном , а функция из синглтона выбирает единственный элемент набора. Натуральные числа 𝐍 представляют собой NNO, где z - функция от одноэлементного числа до 𝐍, изображение которой равно нулю, а s - функция-последователь . (На самом деле мы могли бы позволить z выбирать любой элемент из 𝐍, и результирующий NNO был бы изоморфен этому.) Можно доказать, что диаграмма в определении коммутирует, используя математическую индукцию .
- В категории типов теории типов Мартина-Лёфа (с типами как объектами и функциями как стрелками) стандартный тип натуральных чисел nat является ННО. Можно использовать рекурсор для nat, чтобы показать, что соответствующая диаграмма коммутирует.
- Предположить, что является Гротендика топос с терминала объекта и это для некоторой топологии Гротендика по категории . Тогда если постоянный предпучок на , то ННО в это связка и может быть показан в форме
Смотрите также
Рекомендации
- ^ Джонстон 2002 , A2.5.1.
- ^ Ловера 2005 , стр. 14.
- Перейти ↑ Leinster, Tom (2014). «Переосмысление теории множеств». Американский математический ежемесячник . 121 (5): 403–415. arXiv : 1212,6543 . Bibcode : 2012arXiv1212.6543L . DOI : 10,4169 / amer.math.monthly.121.05.403 .
- ^ Джонстон 2002 , A2.5.2.
- ^ Барр, Майкл; Уэллс, Чарльз (1990). Теория категорий для информатики . Нью-Йорк: Прентис-Холл. п. 358. ISBN 0131204866. OCLC 19126000 .
- ^ Джонстон 2005 , стр. 108.
- Джонстон, Питер Т. (2002). Эскизы слона: Сборник теории топоса . Оксфорд: Издательство Оксфордского университета. ISBN 0198534256. OCLC 50164783 .
- Ловер, Уильям (2005) [1964]. «Элементарная теория категории множеств (полная версия) с комментариями» . Отпечатки в теории и приложениях категорий . 11 : 1–35.
Внешние ссылки
- Лекционные заметки Роберта Харпера, в которых обсуждаются NNOs в Разделе 2.2: https://www.cs.cmu.edu/~rwh/courses/hott/notes/notes_week3.pdf
- Сообщение в блоге Клайва Ньюстеда о кафе n -Category: https://golem.ph.utexas.edu/category/2014/01/an_elementary_theory_of_the_ca.html
- Заметки о типах данных как алгебрах для эндофункторов, сделанные компьютерным ученым Филипом Вадлером : http://homepages.inf.ed.ac.uk/wadler/papers/free-rectypes/free-rectypes.txt
- Примечания к nLab : https://ncatlab.org/nlab/show/ETCS