а вот ещё рант

[juan_gandhi]

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

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

Comments

[huzhepidarasa.livejournal.com]

А как надо?

[ivan-gandhi.livejournal.com]

Ну он же для локально малых категорий только определён.

[huzhepidarasa.livejournal.com]

It's a "bring your own set theory" party. Когда существует какой-никакой Hom, оно и хорошо.

[ivan-gandhi.livejournal.com]

Может, и хорошо - а на что оно?

[migmit.livejournal.com]

Я поддерживаю Джонстона в деле освобождения теории категорий от тёмных деталей теории множеств.

[ivan-gandhi.livejournal.com]

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

[migmit.livejournal.com]

Наверное, это потому, что не такие уж они и истины.

[sober-space.livejournal.com]

Я когда начал читать вполне себе алгебраиста Касселя то был потрясён как он использует Hom ))

Он его буквально изнасиловал. Левая часть хома могла быть в категории алгебр, другая в категории множеств. Ну и т.д. и т.п. ))))

[ivan-gandhi.livejournal.com]

О, как это? Можно уточнить ссылку?

[sober-space.livejournal.com]

Ну вот (http://books.google.ru/books?id=S1KE_pToY98C&lpg=PP1&hl=ru&pg=PA7#v=onepage&q&f=false). Нет, ну там всё вполне корректно, конечно, но мне было непривычно.

[ivan-gandhi.livejournal.com]

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

[sober-space.livejournal.com]

Ну я же и говорю... непривычно...

[dimpas.livejournal.com]

ну да, вот Борис Гребенщиков (учившийся на матфаке ЛГУ в свое време) в какой-то песне даже поет "Hom, ho–hom"...

:-)

[ivan-gandhi.livejournal.com]

Он учился на примате, и там тогда ничему такому не учили, не знаю, как сейчас.

[marina_p]

Я пишу Hom, и вообще это во всех книжках так пишется. А что не так?

[ivan-gandhi.livejournal.com]

Для каких категорий?

[marina_p]

Да вроде для любых. Но реально везде же конкретные категории возникают.

[ivan-gandhi.livejournal.com]

Для любых же его не существует. Локально малые - одно, замкнутые моноидальные другое - а вообще - нету.

[cadadr.livejournal.com]

Ничего не понял. Все пишут Hom_C (A,B), а чем является этот Hom — отдельный вопрос.

[ivan-gandhi.livejournal.com]

И никто не сомневается в его существовании, да?

Hom_Cat(Set, Cat)

[cadadr.livejournal.com]

Если не понятно с Hom_C (A,B), значит и с самой категорией не всё понятно.

[ivan-gandhi.livejournal.com]

В смысле что она не локально малая? И чо? Ну нету Hom - это всё, что я хотел сказать.

[cadadr.livejournal.com]

Hom_C может быть и без локальной малости — ну пусть это не множество, а класс, супер-класс, супер-супер-класс, сепулька, и т. п. Не всегда задумываются, что это, т.е. не заботятся о всяких теоретико-множественных тонкостях. Но написать "Hom_C" ничего не мешает.

[ivan-gandhi.livejournal.com]

Вопрос - what's the codomain category of this functor?

[cadadr.livejournal.com]

Этот вопрос уже отдельный. Всё же одно дело когда пишут "Hom_C (A,B)", и ничего особенного под этим не подразумевают (ну какая-то сепулька стрелок из A в B), а другое дело — "Hom_C (A,−)" или там "Hom_C (−,B)".

[anhinga-anhinga.livejournal.com]

А в чём состоят глубокие причины того, что "последовательность" sets, proper classes, ... нельзя продолжать туда, где троеточие?

Мне казалось, что просто надо декларировать, что мы считаем это законным, и все дела, но, может быть, там есть какие-то более глубокие проблемы?

[anhinga-anhinga.livejournal.com]

А здесь, кажется, Hom просто надо объявить классом, а не множеством. Или при неаккуратном обращении легко получить противоречие?

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

Множества - вещь специфическая. Зависит от аксиоматики. Которая в данном случае и вовсе не нужна.

[anhinga-anhinga.livejournal.com]

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

[ivan-gandhi.livejournal.com]

Да я прежде всего в качестве источника знаний имею в виду "Теорию Топосов" Джонстона.

[anhinga-anhinga.livejournal.com]

А, отлично. Этой книжкой я часто пользуюсь, я посмотрю, как там это сделано.

[anhinga-anhinga.livejournal.com]

Но из этого ничего не вышло, потому что на странице 22 (русский перевод 1986-го года) написано, что предполагается, что читатель знаком с понятием сопряженных функторов, а между страницей 67, где вводится понятие внутреннего функтора, и страницей 71, где начинают говорить о конкретных случаях, когда внутренние функторы сопряжены, не видно никакого объяснения того, что означает понятие сопряженности для внутренних функторов (что, вообще говоря, нехорошо со стороны автора, или переводчика, или читателя (меня) -- я не знаю точно, кто из нас троих виноват в том, что я этого не вижу :-) ).

[ivan-gandhi.livejournal.com]

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

[migmit.livejournal.com]

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

[cadadr.livejournal.com]

Ну вот то, что в принципе используется:
http://ncatlab.org/nlab/show/Grothendieck+universe

[ivan-gandhi.livejournal.com]

Это в смысле оказывается, что ВОТ ЭТА ВОТ теория множеств на самом деле единственно правильная? Любопытно, ознакомимся. Не ZFC?

[cadadr.livejournal.com]

Почему правильная? Просто используется, когда возникают технические вопросы. Где-то в Séminaire de Géométrie Algébrique такое было написано.

[ivan-gandhi.livejournal.com]

Ну нет.

Этак мы всякую категорию в множества запишем, в том числе и Set_ZFC.

Да в конце концов, Hom_Cat(1, Set) - это что вообще? Множество тоже? Любопытно, любопытно.

[huzhepidarasa.livejournal.com]

Cat вроде бы категория (глобально) малых категорий, Set в нее не входит.

[huzhepidarasa.livejournal.com]

А вообще нам, долбокодерам, слишком большие множества неинтересны (количество битов во Вселенной конечно). Нам, максимум, нужно взять N, к нему применить Powerset счетное число раз, все это запихать в мешок — и бац, вот вам множество «всех» множеств.