Введение

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

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

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

u ∘ z = q и
u ∘ s = f ∘ u. Иными словами, треугольник и квадрат на следующей диаграмме коммутируют. Пара (q, f) иногда называется рекурсионными данными для u, представленными в виде рекурсивного определения:

⊢ u(z) = q
y ∈ E, N ⊢ u(s y) = f(u(y))

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

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

ННО в картезианских закрытых категориях (CCC) или топосах иногда определяются следующим эквивалентным образом (по Лоуверу): для каждой пары стрелок g: A → B и f: B → B существует единственная стрелка h: N × A → B, такая что квадраты на следующей диаграмме коммутативны. Та же конструкция определяет слабые ННО в картезианских категориях, которые не являются картезианскими закрытыми. В категории с терминальным объектом 1 и бинарными копроизведениями (обозначаемыми +), ННО может быть определена как начальная алгебра эндофунктора, действующего на объекты по правилу и на стрелки по правилу .

Примеры

В категории множеств, стандартные натуральные числа являются NNO. Терминальный объект в Set – это синглтон, и функция из синглтона выделяет единственный элемент множества. Натуральные числа 𝐍 являются NNO, где 0 – это функция из синглтона в 𝐍, образ которой равен нулю, а s – функция следования. (Мы могли бы позволить 0 выделять любой элемент 𝐍, и полученный NNO был бы изоморфен этому.) Можно доказать, что диаграмма в определении коммутирует, используя математическую индукцию. В категории типов теории типов Мартина Лёфа (с типами как объектами и функциями как стрелками), стандартный тип натуральных чисел nat является NNO. Можно использовать рекурсор для nat, чтобы показать, что соответствующая диаграмма коммутирует. Предположим, что 𝐄 – это топос Гротендика с терминальным объектом 1 и что 𝒥 – некоторая топология Гротендика на категории 𝐄. Тогда, если 𝐅 – постоянный прешэф на 1, то NNO в 𝐄 – это sheafification 𝐅 и может быть показано, что он принимает вид…