а вот ещё рант
Jul. 2nd, 2012 08:41 pm![[personal profile]](https://www.dreamwidth.org/img/silk/identity/user.png){kind=small}
juan_gandhiЕсли категорщик пишет слово
А ведь сплошь и рядом.
Hom, то он вызывает у меня большие подозрения. Если какой другой математик или программист пишет слово Hom, то он вызывает у меня большое сочувствие, unless они имеют в виду какую-нибудь конкретную замкнутую моноидальную категорию.А ведь сплошь и рядом.
![[identity profile]](https://www.dreamwidth.org/img/silk/identity/openid.png){kind=small}
no subject
Date: 2012-07-03 11:19 pm (UTC)Хорошо бы привыкнуть, что нет такой универсальной теории множеств, из которой выводится всё.
Например, в ZFC нет никаких классов.
Ну хорошо, предположим на минутку, что мы объявили Hom классом.
Так в какую категорию этот функтор? Нет такой категории - "классы". Нет. Как вы определите морфизмы на классах? Уж не через декартово ли произведение?
no subject
Date: 2012-07-04 02:39 am (UTC)no subject
Date: 2012-07-04 05:17 am (UTC)А соответствие - когда каждому объекту... и каждому морфизму...
no subject
Date: 2012-07-04 05:59 am (UTC)no subject
Date: 2012-07-04 03:59 am (UTC)А в ZFC можно определить категорию Set? Или понятие локально малой категории? Или эти понятия предполагают, что классы есть?
(Ну и, конечно, если всерьёз отнестись к тому, что нет универсальной теории множеств, вообще бывает теория категорий в топосе, и, как вообще говоря, во всех этих "синтетических ситуациях", необязательно считать, что где-то там под всем этим лежит "хорошая" теория множеств. Особенно это популярно у конструктивистов, которые и в ZFC не верят, зато у них есть такие топосы, в которых мир конструктивен. Но, наверняка, они все любят Hom, поскольку любят лямбда-исчисление.)
> Нет такой категории - "классы".
Принято считать, что нет; но если начать строить башню sets, proper classes, ..., то, кажется, ничто не препятствует тому, чтобы её определить...
no subject
Date: 2012-07-04 05:16 am (UTC)Ну и для локально малой классы ж не требуются. Просто если есть множество Hom(A,B) - то локально малая.
Определить категорию "классы" как-то мне непонятно как - ведь там же нужны морфизмы какие-то, а что у классов за морфизмы?
no subject
Date: 2012-07-04 06:06 am (UTC)В какой-нибудь мета-теории это должно быть правильно; интересно, кто-нибудь написал это аккуратно...
> Просто если есть множество Hom(A,B) - то локально малая.
В ZFC никакой другой определить нельзя, насколько я понимаю... Поэтому никакого нетривиального смысле в этом понятии, вроде, не остаётся...
> а что у классов за морфизмы?
"Функции", но только "большие" (бинарные отношения, но являющиеся классами, а не множествами); например, "большая функция", ставящая в соответствие любому множеству другое множество (это если из класса Set в класс Set).
no subject
Date: 2012-07-04 06:16 am (UTC)То есть, в ZFC вообще, похоже, явно описываются только малые категории; хотя аксиомазировать "в стиле ZFC" можно и конкретные отдельно взятые большие категории (например, Set).
no subject
Date: 2012-07-04 06:12 am (UTC)Например, декартово произведение -- морфизм из класса пар множеств в класс множеств.
no subject
Date: 2012-07-04 09:22 am (UTC)no subject
Date: 2012-07-04 09:20 am (UTC)> любят лямбда-исчисление
Во-первых, лямбда-исчисление строится на экспоненте, без нужды в Hom'ах.
Во-вторых, есть понятие internal Hom.
no subject
Date: 2012-07-04 12:52 pm (UTC)Да, но экспонента определяется, как правый сопряжённый функтор к функтору декартова умножения на объект, то есть требуют, чтобы была естественная биекция между hom(a x b, c) и hom(a, c^b).
> Во-вторых, есть понятие internal Hom.
Я это и говорю (в несколько другом контексте, где вся теория категорий внутренняя).
no subject
Date: 2012-07-04 01:26 pm (UTC)Это я к тому, что "конструктивистам, которые любят лямбду" (а попросту, функциональщикам), думать за Hom'ы не нужно совсем. Хотя и в функциональщине всегда все интуитивно понимают экспоненту, как внутренний Hom.
no subject
Date: 2012-07-04 01:43 pm (UTC)В точности. Поэтому (сейчас неохота тратить время, чтобы проверять, но мне кажется, что) так, наверное будет, и когда люди работают внутри всяких "realisability toposes" и тому подобных конструктивных описаниях.
no subject
Date: 2012-07-04 03:02 pm (UTC)no subject
Date: 2012-07-04 03:09 pm (UTC)no subject
Date: 2012-07-04 03:26 pm (UTC)no subject
Date: 2012-07-05 02:18 pm (UTC)Есть естественные преобразования: i from id to GoF, j from FoG to id, такие, что выполняются некоторые равенства:
http://ncatlab.org/nlab/show/triangle+identities
(примерно четвертое сверху определение здесь:
http://ncatlab.org/nlab/show/right+adjoint
)
***
А, я только теперь заметил, что это дано, как главное определение в этой заметке:
http://ncatlab.org/nlab/show/adjoint+functor
(Оказывается, ещё можно говорить, что это "adjunction in the 2-category Cat")
no subject
Date: 2012-07-04 10:11 pm (UTC)no subject
Date: 2012-07-04 10:36 pm (UTC)no subject
Date: 2012-07-04 10:45 pm (UTC)Но, главное, как написать правила, чтобы там не использовались бы кванторы по hom-set'ам? Среди всех формализаций, на которые я сейчас смотрю, я ничего не вижу в таком стиле...
no subject
Date: 2012-07-04 11:30 pm (UTC)no subject
Date: 2012-07-05 04:34 am (UTC)(no subject)
From:(no subject)
From:(no subject)
From:(no subject)
From:(no subject)
From:no subject
Date: 2012-07-05 01:52 am (UTC)no subject
Date: 2012-07-04 07:21 am (UTC)