KV
g >>> id == id
Если нет равенства морфизмов, как записать такую аксиому?
Если нет равенства морфизмов, как записать такую аксиому?
Size: a a a
2020 February 01
A
Элементы класса это обычно множества в теории множеств, так что на немалых категориях тоже есть равенство
A
Просто возникают проблемки с такими вещами, как "категория всех категорий" или "категория функторов между парой категорий"
A
Вообще, в произвольной логической теории равенство это просто такой специальный символ (предикат), от которого требуют "рефлексивность" (объект равен самому себе), транзитивность (a = b, b = c => a = c), симметричность (a = b <=> b = a) и согласованность с остальными предикатами и операциями: то есть, например, если f = g и h = k, то f . g должно быть равно h . k
A
По сути, когда мы говорим о конкретной модели этой теории, то мы должны определить, что мы понимаем под этим равенством (задать интерпретацию), чтобы эти аксиомы выполнялись
A
То есть можно определить теорию категорий как логическую теорию, а не надстройку над (расширенной) теорией множеств, но когда мы будем говорить о конкретной категории, нужно будет сказать, что мы понимаем под равенством
A
Обычно этого не делают, а используют обычное теоретико-множественное равенство
VY
Спасибо
VY
Т.е. морфизмы равны, когда этот "один и тот же морфизм" и ничего больше мудрить не надо, так? %)
KV
Т.е. морфизмы равны, когда этот "один и тот же морфизм" и ничего больше мудрить не надо, так? %)
Мудрить надо по ситуации
KV
Можно рассматривать enriched категории с изоморфизмом морфизмов. Не знаю, где это может понадобиться, но вдруг
KV
Опять же, в высших категориях изоморфизмы вместо равенства
VY
Да, это вроде как более корректно звучит (имхо)... натуральные изоморфизмы морфизмов
VY
То есть можно определить теорию категорий как логическую теорию, а не надстройку над (расширенной) теорией множеств, но когда мы будем говорить о конкретной категории, нужно будет сказать, что мы понимаем под равенством
Ну да, вот так я это понимаю теперь... Т.е. равенство это вот просто символ с 3 св-вами, перечисленными выше и оно просто есть. Но как только мы укажем на конкретную категорию, то нужно будет объяснить что оно значит. Всем большое спасибо за объяснения!
DK
объясните прикладное значение теории категорий, пожалуйста
KV
объясните прикладное значение теории категорий, пожалуйста
Прямые приложения — это ongoing research, а так-то это вообще внутренний инструмент точных наук
DK
спасибо, кажется, я сильно далек от этого
A
Прямые приложения — это ongoing research, а так-то это вообще внутренний инструмент точных наук
Так ведь и в программировании всё чаще используется
KV
Так ведь и в программировании всё чаще используется
Не знаю, не знаю. То, что в программировании, это скорее либо результаты научных работ с использованием категорий, которые могли бы быть получены и без них, либо какие-то конструкции по навеянным мотивам, типа монад в хаскелле
KV
Ни первое, ни второе, приложением не поворачивается язык назвать