Написал учебник теории категорий

[george66]

Geen в сообщении #1209274 писал(а):

Это понятно. Правда, попутно возник ещё один вопрос - один протоморфизм может "породить" несколько морфизмов?

Да, может и там есть пример (для предпорядка есть не больше одной стрелки между любыми двумя объектами $A$ и $B$, можно все такие стрелки обозначать $(A,B)$ или $(A,*,B)$, здесь достаточно одного протоморфизма $*$)

-- 13.04.2017, 23:00 --

Geen в сообщении #1209274 писал(а):

Вроде бы не было упоминаний, что единица единственна;

Да, двусторонняя единица единственна, но нам это ни за чем не нужно. В определении категории сказано "каждому объекту $A$ сопоставлена некоторая стрелка $id_A$, которая является двусторонней единицей", везде дальше мы работаем именно с этой двусторонней единицей. Если бы даже двусторонних единиц могло быть несколько, мы имеем одну выбранную.

-- 13.04.2017, 23:08 --

Geen в сообщении #1209274 писал(а):

Вы главное не обижайтесь если вопросы окажутся глупыми

Математики стесняются спрашивать, это зря. Больше всех опечаток в книге нашёл один программист (если не считать меня самого)

[Geen]

arseniiv в сообщении #1209283 писал(а):

Тут должно пройти рассуждение как для моноидов и единственности их нейтрального элемента: $\mathrm{id}_A = \mathrm{id}_A\circ\mathrm{id}'_A = \mathrm{id}'_A$ для любого объекта.

george66 в сообщении #1209301 писал(а):

В определении категории сказано "каждому объекту $A$ сопоставлена некоторая стрелка $id_A$, которая является двусторонней единицей", везде дальше мы работаем именно с этой двусторонней единицей.

Прошу прощения, у меня в голове каша ещё пока из утверждений типов: "для любого A существует 1" и "существует процедура, которая для каждого A указывает (один) 1"...

-- 14.04.2017, 00:10 --

george66 в сообщении #1209301 писал(а):

Математики стесняются спрашивать, это зря.

Ну, я не математик.

-- 14.04.2017, 00:12 --

george66 в сообщении #1209252 писал(а):

Равенство стрелок - это просто равенство без всяких затей. Например, что понимается под равенством действительных чисел? Вот так же и со стрелками. Проблемы равенства нас на данном этапе не волнуют.

Вот тут я впервые задумался о нетривиальности "аксиомы ассоциативности"

-- 14.04.2017, 00:17 --

(Оффтоп)

warlock66613 в сообщении #1209297 писал(а):

класс тождественных морфизмов является подклассом класса всех морфизмов, а раз класс всех морфизмов является множеством, то и класс тождественных морфизмов является множеством

На всякий случай уточню - есть такая теорема? (что подкласс множества является множеством)

[george66]

Geen в сообщении #1209308 писал(а):

george66 в сообщении #1209252 писал(а):

Равенство стрелок - это просто равенство без всяких затей. Например, что понимается под равенством действительных чисел? Вот так же и со стрелками. Проблемы равенства нас на данном этапе не волнуют.

Вот тут я впервые задумался о нетривиальности "аксиомы ассоциативности"

С равенством связаны свои нетривиальные проблемы (как и со всем "простым", если глубже копнуть), но нас они пока не интересуют.

-- 14.04.2017, 01:40 --

Geen в сообщении #1209308 писал(а):

На всякий случай уточню - есть такая теорема? (что подкласс множества является множеством)[/off]

Да, в ZF есть (аксиома выделения).

[sergei1961]

Всё-таки книга, не пост. Хотелось бы автора по имени... Затрачен большой труд, хотелось бы знать, кому быть благодарным. Или всё равно нельзя?

[george66]

Имя моё Георгий (Георгиевич), а фамилия ничем не знаменита. Если бы у меня было много выдающихся трудов, я бы непременно похвастал. Теорию категорий я выучил сам (за отсутствием русскоязычных знатоков, кроме Минца, который был в Америке), сидя в библиотеке ГПНТБ и читая журналы, лет за десять разобрался. По мере научения пробовал на людях (на маленьком семинаре в МГУ), в конце концов осталось только записать. У нас некоторый кусочек теории категорий знали алгебраисты, но там нужен довольно специальный кусок (что такое декартово замкнутая категория, они не знали).

[Anton_Peplov]

Можно замечание от читателя?

Понятно, что в определении категории (с. 1) слова "совокупность" и "операция" понимаются в наивном интуитивном смысле, и это правильно, потому что начинать с формальной теории - жестокость. Но я (как, полагаю, и многие другие читатели) давно привык к формализации этих понятий в ZFC. И, например, увидев слово "операция" (операция композиции сопоставляет паре стрелок....), автоматически понимаю его как "функция двух переменных", а функцию - как упорядоченную тройку множеств. Ясно, что это неправильно, ведь все стрелки категории вообще не обязаны образовывать множество. Не будет ли полезным прямо перед определением категории черкнуть пару фраз, что, мол, "совокупности", "операции" и т.д. мы пока понимаем в наивном смысле, и теоретико-множественную их формализацию не надо вспоминать, добра не будет?

Кстати, можно ли при определении категории понимать эту "совокупность" как класс, а "операцию" как функцию двух переменных (подкласс декартова произведения классов, такой, что...) в NBG? Кажется, Кон в "Универсальной алгебре" так и делает, но у него там только локально малые категории...

[george66]

Anton_Peplov в сообщении #1210794 писал(а):

Кстати, можно ли при определении категории понимать эту "совокупность" как класс, а "операцию" как функцию двух переменных (подкласс декартова произведения классов, такой, что...) в NBG? Кажется, Кон в "Универсальной алгебре" так и делает, но у него там только локально малые категории...

В NBG можно. Но я старался не говорить о теории множеств по двум причинам:
1) воспринимаю её как давно покойную науку;
2) программистам всё равно, они слово "операция" и так понимают наивно.
Упоминал только в тех местах, где возникают серьёзные трудности, если не различать большое и малое.

[Anton_Peplov]

george66 в сообщении #1210883 писал(а):

В NBG можно.

Спасибо.

george66 в сообщении #1210883 писал(а):

программистам всё равно, они слово "операция" и так понимают наивно.

Программистам-то да, но ведь книжку будут читать и математики.

[kp9r4d]

Anton_Peplov
Я как понимаю (пусть george66 меня поправит, если это не так) единого консенсуса в формализации категорий не достигнуто, а подход делить на большие и малые категории не идеален, потому что всё равно не получится рассматривать вещи, вроде "категории всех категорий", а очень хочется иногда.

-- 19.04.2017, 21:58 --

Category theory and foundations

[Anton_Peplov]

А вот на эту тему интересная цЫтата есть.

Chanzaa в сообщении #1209425 писал(а):

Маклейн предложил формальный язык, содержащий логику первого порядка и несколько нелогических аксиом; аксиомы множеств в этот язык не входят. Этот язык называется "метакатегория". На этом языке (и его диалектах) можно дать чистое определение множеств, чистое определение групп и даже чистое определение категорий. Самые известные результаты здесь принадлежат Ловеру. Он предложил диалект метакатегории под названием ETAC (элементарную теорию абстрактной категории) и с его помощью сделал ETCC и ETCS - соответственно элементарную теорию категории всех категорий и элементарную теорию категории всех множеств, то есть метаязык для категорий и метаязык множеств, в которых не встречается слово "множество" и тем более "класс".

[george66]

Если формализовать, естественный подход -- "башня". Есть малые множества, это "множества уровня ноль", их совокупность будет "множеством уровня один", совокупность множеств уровня один будет "множеством уровня два" и так далее. В теории множеств это, кажется, называется "универсумы Гротендика", в современной теории типов просто "универсумы".

[kp9r4d]

george66
По структуре очень напоминает теорию типов, которая была изложена в "Principia Mathematica", там парадокс лжеца нельзя было сформулировать, потому что утверждения уровня $n+1$ могли содержать только ссылки на утверждения уровня $n$, ну и для каждого уровня, формально, нужно было формулировать все определения и утверждения занаво, потому что эта "лесенка" вынесена на метаязык. Ну только это не избавляет от тех же проблем, категорию всех категорий нельзя рассмотреть, ровно как и нельзя рассмотреть "категорию всех множеств на всех уровнях". Унивёрсумы Гротендика это, всё же, нечто другое.

Anton_Peplov
Metacategory это не формальный язык, а модель определенной теории первого порядка. ETAC позволяет рассуждать о категориях ровно столько, сколько формальные выводы из аксиом групп позволяют рассуждать о группах. То есть всё хорошо до тех пор, пока нам не нужен какой-то механизм образования групп/категорий и механизм насыщения групп/категорий доп. структурами. К тому же это никак не решает проблему 2-категорий всех категорий, о ней на ETAC говорить нельзя. Про ETCC доказано, что она не обладает достаточной выразительной силой, чтобы охарактеризовать метакатегорию всех категорий. ETCS это вообще аксиоматизация топоса $\mathbf{Set}$ (снова, я, конечно за то, чтобы говорить что множество - это объект категории $\mathbf{Set}$, а категория - это множество (которое объект категории $\mathbf{Set}$), но это, видимо, не то, что вы ищите). Всё это в приведённой ссылке есть, почитайте, там помимо строгих конструкций есть довольно популярные объяснения.

[george66]

kp9r4d в сообщении #1210911 писал(а):

По структуре очень напоминает теорию типов, которая была изложена в "Principia Mathematica", там парадокс лжеца нельзя было сформулировать, потому что утверждения уровня $n+1$ могли содержать только ссылки на утверждения уровня $n$, ну и для каждого уровня

Не совсем то же самое. Если мы к теории типов добавим "тип всех типов" $U$, элементами которого являются все типы, включая его самого, мы получим примерно такой же парадокс, как и с множеством всех множеств. Поэтому мы добавим "тип всех малых типов" и обозначим его $U_0$, сам он своим элементом не является, потому что "большой". Мы можем из него что-то строить, например $U_0\times U_0$ и $U_0^{U_0}$. Все эти типы (а также малые, которые раньше у нас были) являются элементами $U_1$. И так далее, вводится цепочка "универсумов" возрастающей величины $U_0, U_1, U_2\cdots$

-- 20.04.2017, 00:52 --

Anton_Peplov в сообщении #1210894 писал(а):

А вот на эту тему интересная цЫтата есть.

Chanzaa в сообщении #1209425 писал(а):

Маклейн предложил формальный язык, содержащий логику первого порядка и несколько нелогических аксиом; аксиомы множеств в этот язык не входят. Этот язык называется "метакатегория". На этом языке (и его диалектах) можно дать чистое определение множеств, чистое определение групп и даже чистое определение категорий. Самые известные результаты здесь принадлежат Ловеру. Он предложил диалект метакатегории под названием ETAC (элементарную теорию абстрактной категории) и с его помощью сделал ETCC и ETCS - соответственно элементарную теорию категории всех категорий и элементарную теорию категории всех множеств, то есть метаязык для категорий и метаязык множеств, в которых не встречается слово "множество" и тем более "класс".

Формализации от Маклейна не прижились (хотя Маклейн учился математической логике). У Маклейна вообще сочетается глубокое понимание с неумением хорошо подать.

[Anton_Peplov]

В общем, пока я вижу ситуацию так.

1. Чтобы говорить про $\operatorname{Set}$, NGB хватает.
2. Чтобы говорить про "категорию всех категорий" и еще что-то столь же крутое, NGB не хватает.
3. Формализации, которые позволяют говорить про это крутое, обсуждаются, но мне совсем не обязательно знакомиться с наработками на эту тему прямо сейчас.

[george66]

Да, NGB хватает для всего, что есть в учебнике.