Alexander Kuklev (akuklev) wrote,
Alexander Kuklev
akuklev

Categories:

Категории и логика, построения и доказательства

Для нужд семинара по топосам прочитал книжку Ловера «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), определения пределов и копределов столь же наглядных и проработанных, каковы определения произведений и копроизведений. Напрасно ничего не было сказано про категории, где переходы не являются функциями.
Subscribe

  • (no subject)

    Встретил фотографию толпы футбольных фанатов, и она меня скорее напугала, у меня уж точно нет желания быть там среди них. Но внезапно я понял, что…

  • Прогресс

    Десять дней назад, вторая ступень SpaceX'овского корабля Starship своим ходом слетала своим ходом на десять километров вверх, и усмепшно приземлилась…

  • О водосбережении

    Как известно, питьевая вода во многих странах дефицитный ресурс. И даже в дождливой Германии летом иногда случаются засухи, в результате которых она…

  • Post a new comment

    Error

    default userpic

    Your reply will be screened

    Your IP address will be recorded 

    When you submit the form an invisible reCAPTCHA check will be performed.
    You must follow the Privacy Policy and Google Terms of use.
  • 6 comments