Объект натуральных чисел

В теории категорий объект натуральных чисел ( NNO ) — это объект, наделенный рекурсивной структурой, подобной натуральным числам . Точнее, в категории E с конечным объектом 1, NNO N задается как:

1. глобальный элемент z  : 1 → N , и
2. стрелка s  : N → N ,​

такой, что для любого объекта A из E , глобального элемента q  : 1 → A и стрелки f  : A → A существует уникальная стрелка u  : N → A такая, что:

1. и ∘ z = q , и
2. ты ∘ s знак равно ж ∘ ты . ^{[1] [2] [3]}

Другими словами, треугольник и квадрат на следующей диаграмме коммутируют.

Пару ( q , f ) иногда называют рекурсивными данными для u , заданными в форме рекурсивного определения :

1. ⊢ и ( z ) = q
2. y ∈ _E N ⊢ u ( y ) = f ( u ( y ))

Приведенное выше определение является универсальным свойством NNO, то есть они определены с точностью до канонического изоморфизма . Если стрелка u , как определено выше, просто должна существовать, то есть уникальность не требуется, то N называется слабым NNO.

Эквивалентные определения

NNO в декартовых замкнутых категориях (CCC) или топосах иногда определяются следующим эквивалентным способом (благодаря Ловеру ): для каждой пары стрелок g  : A → B и f  : B → B существует уникальное h  : N × A → B такое, что квадраты на следующей диаграмме коммутируют. ^[4]

Эта же конструкция определяет слабые ННО в декартовых категориях, которые не являются декартово замкнутыми.

В категории с конечным объектом 1 и бинарными копроизведениями (обозначаемыми +) NNO можно определить как начальную алгебру эндофунктора , который действует на объекты как X ↦ 1 + X и на стрелки как f ↦ id ₁ + f . ^[5]

Характеристики

• Каждый ННО является исходным объектом категории диаграмм вида

${\displaystyle 1{\xrightarrow {~\quad q\quad ~}}A{\xrightarrow {~\quad f\quad ~}}A}$

• Если декартово замкнутая категория имеет слабые ННО, то каждый ее фрагмент также имеет слабый ННО.
• NNO могут использоваться для нестандартных моделей теории типов аналогично нестандартным моделям анализа. Такие категории (или топосы) имеют тенденцию иметь "бесконечно много" нестандартных натуральных чисел. ^{[ необходимо уточнение ]} (Как всегда, есть простые способы получить нестандартные NNO; например, если z = sz , в этом случае категория или топос E тривиальны.)
• Фрейд показал, что z и s образуют диаграмму копроизведения для NNO; также, ! _N  : N → 1 является коуравнителем s и 1 _N , т. е . каждая пара глобальных элементов N связана посредством s ; более того, эта пара фактов характеризует все NNO.

Примеры

• В Set , категории множеств , стандартные натуральные числа являются NNO. ^[6] Конечный объект в Set является синглетоном , а функция из синглетона выбирает один элемент множества. Натуральные числа 𝐍 являются NNO, где z является функцией от синглетона к 𝐍 , образ которого равен нулю, а s является функцией-последователем . (Мы могли бы фактически позволить z выбрать любой элемент из 𝐍, и полученный NNO был бы изоморфен этому.) Можно доказать, что диаграмма в определении коммутирует, используя математическую индукцию .
• В категории типов теории типов Мартина-Лёфа (с типами как объектами и функциями как стрелками) стандартный тип натуральных чисел nat является NNO. Можно использовать рекурсор для nat, чтобы показать, что соответствующая диаграмма коммутирует.
• Предположим, что является топосом Гротендика с конечным объектом и что для некоторой топологии Гротендика на категории . Тогда если является постоянным предпучком на , то NNO в является свипированием и можно показать, что он принимает форму ${\displaystyle {\mathcal {E}}}$ ${\displaystyle \top }$ ${\displaystyle {\mathcal {E}}\simeq \mathbf {Shv} ({\mathfrak {C}},J)}$ ${\displaystyle J}$ ${\displaystyle {\mathfrak {C}}}$ ${\displaystyle \Gamma _{\mathbb {N} }}$ ${\displaystyle {\mathfrak {C}}}$ ${\displaystyle {\mathcal {E}}}$ ${\displaystyle \Gamma _{\mathbb {N} }}$ $${\displaystyle \mathbb {N} _{\mathcal {E}}\cong \left(\Gamma _{\mathbb {N} }\right)^{++}\cong \coprod _{n\in \mathbb {N} }\top .}$$

Смотрите также

• Аксиомы арифметики Пеано
• Категориальная логика

Ссылки

1. Джонстон 2002, A2.5.1.
2. Ловер 2005, стр. 14.
3. Лейнстер, Том (2014). «Переосмысление теории множеств». American Mathematical Monthly . 121 (5): 403–415. arXiv : 1212.6543 . Bibcode : 2012arXiv1212.6543L. doi : 10.4169/amer.math.monthly.121.05.403. S2CID  5732995.
4. Джонстон 2002, A2.5.2.
5. Барр, Майкл; Уэллс, Чарльз (1990). Теория категорий для вычислительной науки . Нью-Йорк: Prentice Hall. стр. 358. ISBN 0131204866. OCLC  19126000.
6. Джонстон 2005, стр. 108.ошибка sfn: нет цели: CITEREFJohnstone2005 ( помощь )

• Джонстон, Питер Т. (2002). Эскизы слона: сборник теории топоса . Оксфорд: Oxford University Press. ISBN 0198534256. OCLC  50164783.
• Ловер, Уильям (2005) [1964]. «Элементарная теория категории множеств (длинная версия) с комментариями». Переиздания в Theory and Applications of Categories . 11 : 1–35.

Внешние ссылки

• Конспект лекций Роберта Харпера , в котором обсуждаются ННО в разделе 2.2: https://www.cs.cmu.edu/~rwh/courses/hott/notes/notes_week3.pdf
• Запись в блоге Клайва Ньюстеда о n -Category Cafe: 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