а вот ещё рант

[juan_gandhi]

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

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

Comments

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

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