теория категорий: identity

[109]

пришла в голову такая смешная категория: много объектов, и только identity morphisms. она как-нибудь называется по-специальному?

anyway, меня несколько настораживает использование равенства в теории категорий. любое введение начинается с "у нас есть только объекты и морфизмы, ака стрелки из одного объекта в другой, больше ничего". но очень быстро выясняется, что мы ещё оборудованы двумя операциями сравнения - одна для объектов, другая для морфизмов, которые работают как чёрный ящик - суём туда два морфизма, на выходе получаем true или false.

это необъявленное использование равенства появляется довольно быстро в любом введении в теорию категорий. вот, берём первое попавшееся: http://www.staff.science.uu.nl/~ooste110/syllabi/catsmoeder.pdf

строчка X = dom(f) and Y = cod(f) is okay, потому что это определение домена и кодомена, а не сравнение левой части с правой.

а вот в определении ассоциативности h(gf) = (hg)f уже не okay; at this point we are not equipped to test whether h(gf) = (hg)f или нет, мы не знаем, как проверить два по-разному сконструированных морфизма на равенство.

ну и дальше, id_Xg = g подразумевает возможность проверить, равны ли два по-разному сконструированных объекта, ибо только если они равны, исследуемый морфизм - это identity.

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

гуру, развейте мои сомнения.

Comments

[juan-gandhi.livejournal.com]

Дискретная категория называется. Важная вещь.

И ты прав насчет равенства. Там черти прячутся.

С одной стороны, равенство объектов несущественно (т.е. можно взять или Множества, или Скелет Множеств - типа пофиг); с другой стороны да, морфизмы сличаются на равенство.

Один добрый способ состоит в том, чтобы заявлять, что два морфизма равны если они вообще тождественно равны, т.е. просто являются одним и тем же объектом. (Не то что множества.)

[thedeemon.livejournal.com]

Да, этот момент меня тоже смущал сильно.
Вот тут хороший ответ, по-моему:
http://math.stackexchange.com/questions/1346155/how-should-i-think-about-morphism-equality

Т.е. часто мы имеем дело не с абстрактной категорией, а категорией чего-то, что уже само по себе имеет внутреннюю структуру и свойства, там уже может быть определено равенство (например, если это категория множеств и функций из множеств в множества). Еще, часто мы имеем дело с locally small категориями, где даже если объекты не образуют множества, то для двух конкретных объектов Х и У коллекция всех морфизмов из Х в У это множество, а во всяком множестве у нас уже есть равенство: хотим узнать равны ли морфизмы f и g, объединяем или пересекаем множества {f} и {g}, смотрим на число элементов в результате. Т.е. реюзаем то самое равенство, которое используется, когда идет речь о _множестве_ морфизмов из Х в У. В более общем же случае, когда у нас просто непонятная категория, и способа определить/вычислить равенство морфизмов нам снаружи не дадено, остается лишь работать с этими уравнениями синтаксически, опираться лишь на аксиомы самой ТК. Говорит нам аксиома, что id o f = f, вот это равенство и используем, не пытаясь проникнуть в его внутренний смысл, работаем чисто эквационально.

В применении к программированию, когда морфизмы это функции, как я понял, используется экстенсиональное их равеноство: (int x) => x+2 и (int x) => 1 + x + 1 суть равные морфизмы из Int в Int.

[109.livejournal.com]

а, внутренняя структура, понятно. то есть, как я и сказал, мы должны быть equipped with some way to test equality, просто это постоянно забывают упомянуть :)

про "непонятную категорию" непонятно :)

id o f = f - это же не аксиома, это определение identity (или, другими словами, test на identity), которым можно пользоваться только если мы знаем, как сравнивать объекты.

про использование множеств (без внутренней структуры) тоже непонятно. ну вот у нас есть два множества, { f(gh) } и { (fg)h }, чему равно их пересечение? нельзя сказать без знания внутренней структуры.

[thedeemon.livejournal.com]

Ну вот товарисч из ссылки сообщает, что необязательно мы должны быть equipped, можно на одних уравнениях ехать. Фишка в том, что то уравнение на id - это именно не тест, а аксиома. Определение категории (некоторые из) нам говорит, что нам дана волшебная функция, которая получает на вход произвольный объект категории и возвращает его id морфизм. И морфизм этот таков, что служит левой и правой единицей для композиции, т.е. выполнены такие-то равенства. Т.е. само определение id нам дарит эти равенства, как аксиомы. И дальше мы можем их использовать в уравнениях.
Подобно тому, как интерпретатор CPL использует эти уравнения для вычислений.

[109.livejournal.com]

ну да. мой пойнт заключается в том, что определение категории говорит нам, что у нас есть категория, если (среди прочих вещей) у нас для каждого объекта есть id morphism. теперь надо проверить, действительно ли у нас категория, для этого надо проверить, есть ли у нас id морфизмы. для этого надо проверить, выполняется ли равенство. и в этом смысле оно тест, а не аксиома.

а ты говоришь, что если уже известно, что это категория, то, значит, есть id морфизмы. duh! :)

[thedeemon.livejournal.com]

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