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

[george66]

Вообще, немножко удивляет частое желание непременно формализовать до оснований. Единственный случай, когда обычному математику (не специалисту по основаниям) приходится что-то формализовать до оснований -- это если он решил проверить свои результаты пруфчекером. А в этом случае формализуют в современной теории типов, по техническим причинам она гораздо лучше подходит для пруфчекера.

[Anton_Peplov]

Это детская травма. Рассел как-то выгуливал свой парадокс без поводка и ошейника. Он нас сильно покусал, и с тех пор мы очень его боимся.

[arseniiv]

Мне почему-то желание убедиться в том, что у аксиом, скажем, $\mathbb R$ есть модели, кажется достаточно сходным с желанием «основать». Кто насколько далеко зайдёт. (У меня это притом тоже есть, и вообще я заинтересовался в своё время матлогикой по таким причинам.)

[warlock66613]

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

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

А нематематику — тем более. Так что это желание внематематическое. Но разве анафункторы, появившиеся, если я правильно понимаю, благодаря этому желанию, не красивы?

[Anton_Peplov]

Б. Рассел писал(а):

Я жаждал определенности, как иные жаждут религиозной веры.

Я его понимаю, надо сказать.

[george66]

Поставьте пруфчекер Agda
https://en.wikipedia.org/wiki/Agda_(pro ... g_language)
и попробуйте что-нибудь доказать. Это, грубо говоря, как Microsoft studio, только для построения математических доказательств, они же лямбда-термы, они же программы на языке Haskell (с некоторыми добавлениями). Доказательства строятся шаг за шагом, на каждом шаге программа проверяет правильность и подсказывает возможные ходы. Это отучит от теории множеств навсегда. Правда, это тоже фигня, зато современная.

[arseniiv]

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

они же программы на языке Haskell (с некоторыми добавлениями)

По моим поверхностным впечатлением, Agda никак нельзя назвать хаскелем с добавлениями, это довольно другой язык.

-- Вс апр 23, 2017 18:52:10 --

Зато она на нём сама написана.

[Anton_Peplov]

Я про протоморфизмы чего-то не понял. Итак, они отличаются от морфизмов только тем, что протоморфизм может иметь сколько угодно начал и концов. Затем мы берем упорядоченную тройку "объект $A$, объект $B$ и протоморфизм $\varphi$ такой, что одним из его начал является $A$ и одним из его концов является $B$" и называем эту тройку морфизмом $f: A \to B$.
В учебнике сказано, что такое построение категории "обычно используется на практике". Можно ли развернуть этот тезис, проиллюстрировать примерами? Пока никакой практики я в нем не вижу, вижу "почесать левой ногой правое ухо". В частности, не понимаю, что означает фраза

Цитата:

Именно так мы строили категорию Set, протоморфизмами в этом случае были теоретико-множественные функции

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

[george66]

Теоретико-множественная функция определяется как множество пар. Например, функция на натуральных числах, тождественно равная нулю, определяется как множество пар $(0,0), (1,0), (2,0)\ldots$ По ней можно восстановить область определения, но нельзя восстановить область значений (виден один 0), что написано в Примере 1.3

[Anton_Peplov]

Понятно. Мы с Вами привыкли к разным определениям функции. Вы определяете функцию как множество упорядоченных пар с определенными свойствами. Я - как упорядоченную тройку $(X, Y, \Gamma)$, где $\Gamma \subset X \times Y$ - то самое множество упорядоченных пар, которое в этом определении называется не функцией, а графиком функции. Каким из этих двух определений пользоваться - вопрос вкуса, но в математической литературе они встречаются со сравнимой частотой, и стоит иметь в виду, что читатель может исходить из второго определения.

[Anton_Peplov]

Рассмотрим диаграмму
$\xymatrix{X\ar[rd]_h\ar[rr]^f&&Y\ar[ld]^{g}\\&Z}$
где $f, g, h$ - некоторые морфизмы, о которых мы знаем только то, что нарисовано на диаграмме.
Правильно ли я понимаю, что мы не можем сказать, коммутативна эта диаграмма или нет? А чтобы сказать, что она коммутативна, надо удостовериться, что $h = g \circ f$ (что из изображенной диаграммы не следует)?

[george66]

Да, по умолчанию не предполагается, что диаграмма коммутативна.

[Anton_Peplov]

В связи с этим интересно, что в пособиях по набору формул в $\TeX$ соответствующий раздел неизменно называется "коммутативные диаграммы", как будто некоммутативных не бывает. Это сбивает с толку.

[Padawan]

Ни разу не видел, чтобы диаграмма была нарисована и при этом не была коммутативной.

[Anton_Peplov]

Почему? Некоммутативные диаграммы никому не нужны?