теория категорий: 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

[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]

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