Лемма Йонеды: формулировка, доказательство, вложение

Лемма Йонеды - одно из тех утверждений, которое звучит как технический пустяк, но на деле задаёт само мировоззрение теории категорий. Формально она утверждает, что для любого объекта $A$ категории $\mathcal{C}$ и любого функтора $F: \mathcal{C} \to \text{Set}$ существует естественная биекция между естественными преобразованиями представимого функтора $h_A = \text{Hom}_{\mathcal{C}}(A, -)$ в $F$ и элементами множества $F(A)$. Содержательно она говорит вот что: объект полностью определяется тем, как из него выходят стрелки в остальные объекты категории. Дальше разберём формулировку аккуратно, набросаем доказательство, поговорим о вложении Йонеды и посмотрим, где это всё всплывает на практике.

Контекст: представимые функторы

Представимый функтор - это ковариантный функтор вида $h_A = \text{Hom}_{\mathcal{C}}(A, -): \mathcal{C} \to \text{Set}$. Он отправляет объект $X \in \mathcal{C}$ в множество морфизмов $\text{Hom}(A, X)$, а стрелку $f: X \to Y$ - в отображение посткомпозиции $f_*: \text{Hom}(A, X) \to \text{Hom}(A, Y)$, $g \mapsto f \circ g$. Контравариантный вариант - $h^A = \text{Hom}_{\mathcal{C}}(-, A): \mathcal{C}^{op} \to \text{Set}$, он реагирует на стрелки предкомпозицией. Представимость функтора $F$ означает существование такого $A$, что $F \cong h_A$ (или $F \cong h^A$ в контравариантном случае). Лемма Йонеды описывает все естественные преобразования из представимого функтора в произвольный - и тем самым проясняет, как «выглядит» представимость изнутри.

Если хочется приложить лемму к своей задаче - выбери ситуацию ниже, и в чате аккуратно построим естественное преобразование, обратное к нему и дадим интерпретацию.

Точная формулировка

Пусть $\mathcal{C}$ - локально малая категория (множества $\text{Hom}(X, Y)$ - настоящие множества, не классы), $A \in \mathcal{C}$ - фиксированный объект, $F: \mathcal{C} \to \text{Set}$ - произвольный ковариантный функтор. Тогда отображение

$$\Phi: \text{Nat}(h_A, F) \to F(A), \qquad \eta \mapsto \eta_A(\text{id}_A)$$

является биекцией множеств. Более того, эта биекция естественна как по $A$, так и по $F$: то есть оба отображения - $\Phi$ и обратное к нему - согласованы со стрелками $A \to A'$ в $\mathcal{C}$ и с естественными преобразованиями $F \to F'$.

Контравариантная версия выглядит зеркально: для $h^A = \text{Hom}(-, A)$ и функтора $G: \mathcal{C}^{op} \to \text{Set}$ имеем $\text{Nat}(h^A, G) \cong G(A)$, биекция определяется тем же способом - значением преобразования на тождестве.

Набросок доказательства

Доказательство - упражнение в естественности. Построим явный обратный к $\Phi$.

Пусть $a \in F(A)$. Определим $\eta^a: h_A \to F$ покомпонентно: для $X \in \mathcal{C}$ и $f \in h_A(X) = \text{Hom}(A, X)$ положим

$$\eta^a_X(f) = F(f)(a) \in F(X).$$

Проверим естественность. Для стрелки $g: X \to Y$ нужно проверить коммутативность квадрата с $h_A(g) = g_*$ слева и $F(g)$ справа. Берём $f \in \text{Hom}(A, X)$:

$$F(g) \circ \eta^a_X(f) = F(g)(F(f)(a)) = F(g \circ f)(a),$$ $$\eta^a_Y \circ h_A(g)(f) = \eta^a_Y(g \circ f) = F(g \circ f)(a).$$

Равенство получается из функториальности $F$. Значит, $\eta^a$ действительно естественное преобразование.

Теперь обе композиции. С одной стороны, $\Phi(\eta^a) = \eta^a_A(\text{id}_A) = F(\text{id}_A)(a) = \text{id}_{F(A)}(a) = a$ - снова функториальность. С другой, для любого естественного $\eta: h_A \to F$ и любого $f: A \to X$ из квадрата естественности на стрелке $f$ получается $\eta_X(f) = \eta_X(f \circ \text{id}_A) = F(f)(\eta_A(\text{id}_A))$ - а это в точности $\eta^{\Phi(\eta)}_X(f)$. То есть $\eta$ восстанавливается своим значением на $\text{id}_A$.

Получили: $\Phi$ имеет двусторонний обратный, значит, биекция. Естественность по $A$ и $F$ - отдельные проверки тех же квадратов; они опираются ровно на функториальность участников и на определение естественного преобразования.

Вложение Йонеды и полная вложенность

Сопоставление $A \mapsto h_A$ продолжается до функтора

$$y: \mathcal{C} \to \text{Fun}(\mathcal{C}^{op}, \text{Set}), \qquad A \mapsto \text{Hom}_{\mathcal{C}}(-, A).$$

Здесь категория значений - функторы из $\mathcal{C}^{op}$ в $\text{Set}$, обычно её зовут категорией предпучков и обозначают $\widehat{\mathcal{C}} = [\mathcal{C}^{op}, \text{Set}]$. Стрелке $f: A \to B$ функтор $y$ сопоставляет естественное преобразование $h^A \to h^B$, действующее постcомпозицией с $f$.

Из леммы Йонеды немедленно следует, что $y$ - полное и точное вложение (fully faithful): отображение $\text{Hom}_{\mathcal{C}}(A, B) \to \text{Nat}(h^A, h^B)$ является биекцией. Левая часть - стрелки в $\mathcal{C}$, правая - естественные преобразования между представимыми предпучками. Следствие: $\mathcal{C}$ можно отождествить с её образом внутри $\widehat{\mathcal{C}}$. Любая категория сидит внутри своей категории предпучков как полная подкатегория - и это важный мост к топосам и алгебраической геометрии.

Главное следствие: объект восстанавливается из своего hom-функтора

Если $h_A \cong h_B$ как функторы (естественный изоморфизм), то $A \cong B$ как объекты в $\mathcal{C}$. Иначе говоря, объект задаётся с точностью до изоморфизма множеством своих «образующих» - морфизмов в него (или из него). Это объясняет, почему так много определений в математике формулируется через универсальные свойства: декартово произведение, факторгруппа, тензорное произведение, пределы и копределы. Все они говорят про объект не «что он такое», а «какие отображения в него (или из него) существуют», - и лемма Йонеды гарантирует, что этого описания достаточно.

Например, в категории групп объект $G$ восстанавливается из $\text{Hom}(-, G)$: гомоморфизмы в $G$ с естественным действием перекомпозиции - полная информация о $G$. То же в категории колец, модулей, топологических пространств. Эта же идея «работы через Hom» лежит в основе сопряжённых функторов, где биекция $\text{Hom}(FX, Y) \cong \text{Hom}(X, GY)$ полностью задаёт пару $F \dashv G$.

Приложение в алгебраической геометрии: представимые предпучки

В алгебраической геометрии Гротендика схему часто определяют функтором её точек: $S \mapsto \text{Hom}(S, X)$ - предпучок на категории схем. Схема $X$ называется представимой, если этот предпучок изоморфен $h_X$ для какого-то реального объекта-схемы. Лемма Йонеды позволяет говорить о геометрических объектах через их функциональные точки: проективное пространство, многообразие модулей, формальная схема - все они в первую очередь предпучки, и вопрос «существует ли соответствующий геометрический объект» - это вопрос о представимости. Условия представимости (Артин, Гротендик, Деламонт) - отдельная большая теория; они дают критерии, когда предпучок «приходит» от настоящей схемы.

Приложение в программировании: CPS и Free monads

В функциональном программировании лемма Йонеды появляется через типы. Для функтора $F$ значение типа $F\,A$ изоморфно $\forall R.\ (A \to R) \to F\,R$ - представление в стиле continuation-passing (CPS): «дай продолжение, я применю его к содержимому». Изоморфизм - буквально $F\,A \cong \text{Nat}(\text{Hom}(A, -), F)$. На практике CPS-форма даёт более эффективную композицию: свободные монады в виде Codensity monad обходят квадратичный взрыв при многократном связывании. Языки с продвинутыми системами типов - Haskell, Scala с cats - используют это активно.

Моноид $M$ как одноообъектная категория - это категория с единственным объектом и стрелками-элементами $M$. Функторы из неё в $\text{Set}$ - это $M$-множества. Лемма Йонеды говорит: для $M$-множества $X$ имеем $\text{Nat}(M, X) \cong X$ - $M$-эквивариантные отображения регулярного действия в любое - это просто элементы $X$. Дальше про действия групп и подсчёт орбит см. лемму Бернсайда.

Контравариантная и ковариантная версии

Контравариантная версия - про предпучки. Для $F: \mathcal{C}^{op} \to \text{Set}$ и $A \in \mathcal{C}$:

$$\text{Nat}(h^A, F) \cong F(A), \qquad \eta \mapsto \eta_A(\text{id}_A).$$

Это та форма, которая чаще встречается у геометров и алгебраистов: с ней удобнее работать в категории предпучков, в категориях пучков и в теории топосов. Ковариантная - с $h_A$ - чаще нужна в гомологической алгебре и в категориях модулей, где функторы $\text{Hom}(M, -)$ описывают расширения, проективные резольвенты, $\text{Ext}$-группы.

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

Частые ошибки

• Путать стороны. $h_A$ - ковариантный, его естественные преобразования в $F: \mathcal{C} \to \text{Set}$ соответствуют элементам $F(A)$. $h^A$ - контравариантный, и для него работает функтор на $\mathcal{C}^{op}$. Несоответствие даёт «доказательство», в котором стрелки идут не туда.
• Забывать про локальную малость. Если $\text{Hom}(X, Y)$ - не множество, а собственный класс, то $h_A$ не функтор в $\text{Set}$, и лемма в стандартной форме не применяется. В больших категориях (например, $\text{Set}$ как объект внутри собственной мета-теории) требуются обходы через универсумы Гротендика.
• Считать, что $\Phi$ строится «как-нибудь по индукции». Никакой индукции нет: вся биекция задаётся одной формулой $\eta \mapsto \eta_A(\text{id}_A)$.
• Думать, что лемма Йонеды только для категорий множеств. Цель функтора - обязательно $\text{Set}$, но саму категорию $\mathcal{C}$ можно брать любой локально малой; результат - про неё.
• Путать вложение Йонеды с эквивалентностью. $y$ полное и точное, но обычно не эссенциально сюръективное: большинство предпучков не представимы.

FAQ

В чём «естественность» биекции в формулировке леммы? Имеется в виду, что обе семьи биекций - по $A$ и по $F$ - коммутируют с морфизмами. Если взять $f: A \to A'$, то квадрат с биекциями для $A$ и $A'$ и индуцированными отображениями коммутирует; то же для естественного преобразования $F \to F'$.

Почему лемма так важна, если она «просто переписывает» естественные преобразования через значения? Потому что она превращает абстрактный объект (всё пространство $\text{Nat}(h_A, F)$) в конкретный (множество $F(A)$). Это техническое сокращение, которое снимает целые слои бухгалтерии в категорных рассуждениях.

Что значит «функтор представим»? Функтор $F: \mathcal{C} \to \text{Set}$ называется представимым, если $F \cong h_A$ для какого-то $A$. Объект $A$ называется представляющим объектом и определён с точностью до изоморфизма - это снова следствие самой леммы Йонеды через её главное следствие.

Коротко

Лемма Йонеды утверждает, что естественные преобразования $h_A \to F$ - это в точности элементы $F(A)$, и биекция между ними задаётся вычислением преобразования на тождественной стрелке. Из неё немедленно следует, что объект восстанавливается из своего hom-функтора, что вложение Йонеды $y: \mathcal{C} \to \widehat{\mathcal{C}}$ - полное и точное, и что универсальные свойства корректно определяют объекты. Содержательно - это про то, что в категориях имеют значение не объекты сами по себе, а сеть стрелок, в которую они вплетены.