а вот ещё рант

[juan_gandhi]

Если категорщик пишет слово Hom, то он вызывает у меня большие подозрения. Если какой другой математик или программист пишет слово Hom, то он вызывает у меня большое сочувствие, unless они имеют в виду какую-нибудь конкретную замкнутую моноидальную категорию.

А ведь сплошь и рядом.

Comments

[ivan-gandhi.livejournal.com]

"Класс" - это понятие GB.

Хорошо бы привыкнуть, что нет такой универсальной теории множеств, из которой выводится всё.

Например, в ZFC нет никаких классов.

Ну хорошо, предположим на минутку, что мы объявили Hom классом.

Так в какую категорию этот функтор? Нет такой категории - "классы". Нет. Как вы определите морфизмы на классах? Уж не через декартово ли произведение?

[huzhepidarasa.livejournal.com]

Ну так и функтор, если задуматься, какое-то такое отображение. Не очень понятное. Не функция, а что?

[ivan-gandhi.livejournal.com]

Не функция. Функция в теории множество определена.

А соответствие - когда каждому объекту... и каждому морфизму...

[huzhepidarasa.livejournal.com]

Ну вот мы же не определяем, что такое соответствие. We know it when we see it.

[anhinga-anhinga.livejournal.com]

> Например, в ZFC нет никаких классов.

А в ZFC можно определить категорию Set? Или понятие локально малой категории? Или эти понятия предполагают, что классы есть?

(Ну и, конечно, если всерьёз отнестись к тому, что нет универсальной теории множеств, вообще бывает теория категорий в топосе, и, как вообще говоря, во всех этих "синтетических ситуациях", необязательно считать, что где-то там под всем этим лежит "хорошая" теория множеств. Особенно это популярно у конструктивистов, которые и в ZFC не верят, зато у них есть такие топосы, в которых мир конструктивен. Но, наверняка, они все любят Hom, поскольку любят лямбда-исчисление.)

> Нет такой категории - "классы".

Принято считать, что нет; но если начать строить башню sets, proper classes, ..., то, кажется, ничто не препятствует тому, чтобы её определить...

[ivan-gandhi.livejournal.com]

Хороший вопрос. Так ведь ZFC сама определяет категорию Set.

Ну и для локально малой классы ж не требуются. Просто если есть множество Hom(A,B) - то локально малая.

Определить категорию "классы" как-то мне непонятно как - ведь там же нужны морфизмы какие-то, а что у классов за морфизмы?

[anhinga-anhinga.livejournal.com]

> Так ведь ZFC сама определяет категорию Set.

В какой-нибудь мета-теории это должно быть правильно; интересно, кто-нибудь написал это аккуратно...

> Просто если есть множество Hom(A,B) - то локально малая.

В ZFC никакой другой определить нельзя, насколько я понимаю... Поэтому никакого нетривиального смысле в этом понятии, вроде, не остаётся...

> а что у классов за морфизмы?

"Функции", но только "большие" (бинарные отношения, но являющиеся классами, а не множествами); например, "большая функция", ставящая в соответствие любому множеству другое множество (это если из класса Set в класс Set).

[anhinga-anhinga.livejournal.com]

> В ZFC никакой другой определить нельзя, насколько я понимаю

То есть, в ZFC вообще, похоже, явно описываются только малые категории; хотя аксиомазировать "в стиле ZFC" можно и конкретные отдельно взятые большие категории (например, Set).

[anhinga-anhinga.livejournal.com]

> "Функции", но только "большие"

Например, декартово произведение -- морфизм из класса пар множеств в класс множеств.

[nivanych.livejournal.com]

"Классы" и их иерархия имеют некоторый категорный смысл при лютом предикативизме ;-)

[nivanych.livejournal.com]

> они все любят Hom, поскольку
> любят лямбда-исчисление

Во-первых, лямбда-исчисление строится на экспоненте, без нужды в Hom'ах.
Во-вторых, есть понятие internal Hom.

[anhinga-anhinga.livejournal.com]

> Во-первых, лямбда-исчисление строится на экспоненте, без нужды в Hom'ах.

Да, но экспонента определяется, как правый сопряжённый функтор к функтору декартова умножения на объект, то есть требуют, чтобы была естественная биекция между hom(a x b, c) и hom(a, c^b).

> Во-вторых, есть понятие internal Hom.

Я это и говорю (в несколько другом контексте, где вся теория категорий внутренняя).

[nivanych.livejournal.com]

> Да, но экспонента определяется

Это я к тому, что "конструктивистам, которые любят лямбду" (а попросту, функциональщикам), думать за Hom'ы не нужно совсем. Хотя и в функциональщине всегда все интуитивно понимают экспоненту, как внутренний Hom.

[anhinga-anhinga.livejournal.com]

> Хотя и в функциональщине всегда все интуитивно понимают экспоненту, как внутренний Hom.

В точности. Поэтому (сейчас неохота тратить время, чтобы проверять, но мне кажется, что) так, наверное будет, и когда люди работают внутри всяких "realisability toposes" и тому подобных конструктивных описаниях.

[ivan-gandhi.livejournal.com]

Это такое "малое" определение сопряженности, через естественную биекцию между hom.

[anhinga-anhinga.livejournal.com]

Я забыл, как устроено "настоящее" определение.

[anhinga-anhinga.livejournal.com]

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

[anhinga-anhinga.livejournal.com]

Напишу-ка я, в чём оно состоит, поскольку кажется, что оно имеет больше шансов оказаться "настоящим", чем то, что обсуждаем веткой ниже. Это определение в (крайне нелюбимом мной) "монадическом стиле":

Есть естественные преобразования: 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")

[ivan-gandhi.livejournal.com]

F(x) → y тогда и только тогда, когда x → G(y), с правилами.

[anhinga-anhinga.livejournal.com]

Что означает здесь стрелка? Существования морфизма между объектами?

[anhinga-anhinga.livejournal.com]

I mean, "существование"

Но, главное, как написать правила, чтобы там не использовались бы кванторы по hom-set'ам? Среди всех формализаций, на которые я сейчас смотрю, я ничего не вижу в таком стиле...

[ivan-gandhi.livejournal.com]

Да; слова примерно такие, что каждому морфизму слева "соответствует" морфизм справа, и наоборот.

[anhinga-anhinga.livejournal.com]

Но это, кажется, предполагает, что это с обоих сторон множества. Мне кажется, трудно написать, что это "взаимно однозначное соответствие" так, чтобы не пользоваться неявно тем, что это hom-sets...

[ivan-gandhi.livejournal.com]

Конкретный морфизм.

[migmit.livejournal.com]

Hom_C(A,B) - нифига не функтор.