![[personal profile]](https://www.dreamwidth.org/img/silk/identity/user.png){kind=small}
Для нужд семинара по топосам прочитал книжку Ловера «Conceptual Mathematics: A First Introduction to Category Theory». Книжка прекрасная, она показывает, как можно сделать обзор теории категорий и классно рассказать о топосах, пользуясь только элементарными, доступными любому продвиннутому старшекласнику примерами: конечными множествами, графами, натуральными числами и (буквально пару раз, для иллюстративных примеров) областями ≤ 3-мерного эвклидового пространства. С другой стороны, книжка в некотором смысле сырая, мне бы хотелось рассматривать её как задел для будущего курса на эту тему.
Технические детали полностью опускаются при соблюдении эталонной точности и строгости. Доказательства везде исключительно в форме понятных картинок с пояснительным текстом. После определения категорий (class of objects and collection of composeable transitions between them) и парочки простых примеров объясняется, зачем категории придумали, какая идея за ними стоит: “.. by objectifying certain concepts as transitions in a category, the combining of concepts becomes composition of transitions! Then we can condense a complicated argument into simple calculations using the associative law. Several hundred years ago, Hooke, Leibniz, and other great scientists foresaw the possibility of a “philosophical algebra” which would have such features.”
Conceptual understanding of facts, structures, and theorems mostly comes after their discovery, so categories often play the rôle of mathematical bookkeeping: writing things nicely afterwards and revealing the “big picture”.
А релевантные концепции можно сформулировать на языке переходов между объектами, потому что наблюдаемые свойства объектов проявляются только в их взаимоотношениях с другими объектами. Авторы периодически подчёркивают, что категории это open world theory. Про точки/подобъекты одного объекта можно говорить о реальном их равенстве или вложенности. Для разных объектов говорить о равенстве невозможно, можно говорить только об изоморфизме, т.е. о том, что “со стороны они неотличимы”, а если изоморфизм единственный, то “могут быть однозначно идентифицированы”; что подобъект данного объекта A это не просто объект B, но объект B с конкретно выбранным вложением i: B ↪ A.
Показывается, как из категории “базовых объектов” изготавливаются категории “объектов с дополнительной структурой”, что внутренняя структура объектов конкретных категорий выражается на языке генераторов и соотношений, и что в качестве базовой категории можно брать не только категорию множеств, но и другие категории. Изучено, какими свойствами должны обладать категории базовых объектов, чтобы на них можно было смоделировать всё что угодно — такие категории называются топосами. На конкретных примерах здоровски показывают, как в разных топосах могут выглядить шкалы истинности и работать оператор отрицания.
Классно в самом общем контексте доказывается диагональный аргумент Кантора и в качестве его следствия теорема Гёделя о неполноте. К сожалению, обсуждение теоремы Гёделя очень куцое. И нету того, что я счёл бы кульминацией такого курса: антиГёделя, т.е. теоремы об семантической адекватности категорных моделей: “The deductive logical calculus is sound and complete for models in topoi. Specifically, for any logical theory T, a T-sentence is T-provable iff it is true in every T-model.”
Чего бы я ещё добавил в такой курс кроме этой теоремы (на момент написания книжки кажется ещё даже не доказанной)? Если глобально, то полноценный рассказ о лямбда-исчислении (в т.ч. типизированном, с зависимыми типами), теориях, соответствиях Карри-Говарда и теории множеств/топосе NBG, как минимально-рестриктивной конечно-аксиоматизированной рефлексии теории типов, избегающей парадокса Рассела.
Ну и есть ряд мелких вещей, которые напрашивались, но почему-то были опущены: факторобъекты, категории отношений (comma categories), определения пределов и копределов столь же наглядных и проработанных, каковы определения произведений и копроизведений. Напрасно ничего не было сказано про категории, где переходы не являются функциями.
Технические детали полностью опускаются при соблюдении эталонной точности и строгости. Доказательства везде исключительно в форме понятных картинок с пояснительным текстом. После определения категорий (class of objects and collection of composeable transitions between them) и парочки простых примеров объясняется, зачем категории придумали, какая идея за ними стоит: “.. by objectifying certain concepts as transitions in a category, the combining of concepts becomes composition of transitions! Then we can condense a complicated argument into simple calculations using the associative law. Several hundred years ago, Hooke, Leibniz, and other great scientists foresaw the possibility of a “philosophical algebra” which would have such features.”
Conceptual understanding of facts, structures, and theorems mostly comes after their discovery, so categories often play the rôle of mathematical bookkeeping: writing things nicely afterwards and revealing the “big picture”.
А релевантные концепции можно сформулировать на языке переходов между объектами, потому что наблюдаемые свойства объектов проявляются только в их взаимоотношениях с другими объектами. Авторы периодически подчёркивают, что категории это open world theory. Про точки/подобъекты одного объекта можно говорить о реальном их равенстве или вложенности. Для разных объектов говорить о равенстве невозможно, можно говорить только об изоморфизме, т.е. о том, что “со стороны они неотличимы”, а если изоморфизм единственный, то “могут быть однозначно идентифицированы”; что подобъект данного объекта A это не просто объект B, но объект B с конкретно выбранным вложением i: B ↪ A.
Показывается, как из категории “базовых объектов” изготавливаются категории “объектов с дополнительной структурой”, что внутренняя структура объектов конкретных категорий выражается на языке генераторов и соотношений, и что в качестве базовой категории можно брать не только категорию множеств, но и другие категории. Изучено, какими свойствами должны обладать категории базовых объектов, чтобы на них можно было смоделировать всё что угодно — такие категории называются топосами. На конкретных примерах здоровски показывают, как в разных топосах могут выглядить шкалы истинности и работать оператор отрицания.
Классно в самом общем контексте доказывается диагональный аргумент Кантора и в качестве его следствия теорема Гёделя о неполноте. К сожалению, обсуждение теоремы Гёделя очень куцое. И нету того, что я счёл бы кульминацией такого курса: антиГёделя, т.е. теоремы об семантической адекватности категорных моделей: “The deductive logical calculus is sound and complete for models in topoi. Specifically, for any logical theory T, a T-sentence is T-provable iff it is true in every T-model.”
Чего бы я ещё добавил в такой курс кроме этой теоремы (на момент написания книжки кажется ещё даже не доказанной)? Если глобально, то полноценный рассказ о лямбда-исчислении (в т.ч. типизированном, с зависимыми типами), теориях, соответствиях Карри-Говарда и теории множеств/топосе NBG, как минимально-рестриктивной конечно-аксиоматизированной рефлексии теории типов, избегающей парадокса Рассела.
Ну и есть ряд мелких вещей, которые напрашивались, но почему-то были опущены: факторобъекты, категории отношений (comma categories), определения пределов и копределов столь же наглядных и проработанных, каковы определения произведений и копроизведений. Напрасно ничего не было сказано про категории, где переходы не являются функциями.
