Глава 2. Функторы, естественные преобразования, лемма Йонеды

Где стоит глава

Глава 14.1 установила категорию как метасистему. Эта глава поднимается на следующий этаж: функторы — структура-сохраняющие отображения между категориями (морфизмы категорий); естественные преобразования — морфизмы между функторами; и, как кульминация, — лемма Йонеды и полнота-верность вложения Йонеды.

Это самая сильная новая глава Части XIV: лемма Йонеды и полно-верное вложение здесь не «классическое чтение», а машинно доказанные, без аксиом результаты. Их содержательный итог — точная форма тезиса, зашитого уже в сетоидном равенстве из 14.1:

Объект полностью определяется своими ролями — системой морфизмов из него и в него.

Это категорная форма P3 (мост к 14.3). Базовый Functor.v закрыт без аксиом; новые результаты слоя src/category/ заявлены 0-аксиомными по локальному build — до синхронизации с основной веткой это пункт чек-листа воспроизводимости.

Функтор как структурное соответствие

Функтор $F:\mathcal{C}\to \mathcal{D}$ — пара отображений: на объектах $F_{\mathrm{obj}}$ и на стрелках $F_{\mathrm{mor}}:{\text{Hom}}_{\mathcal{C}}(a,b)\to {\text{Hom}}_{\mathcal{D}}(Fa,Fb)$, с сохранением структуры: $F(\mathrm{id})=\mathrm{id}$ и $F(g\circ f)=F(g)\circ F(f)$.

В Rocq это запись с тремя законами.¹ Помимо сохранения тождества и композиции, поле fmor_compat требует уважения к сетоидному равенству морфизмов (cat_mor_eq, из 14.1) — функтор переносит не «голые стрелки», а стрелки с точностью до их равенства.

Ко- и контравариантность. Ковариантный функтор сохраняет направление стрелок; контравариантный обращает его — формально это функтор ${\mathcal{C}}^{\mathrm{op}}\to \mathcal{D}$ (через opposite_cat из 14.1). Эта тонкость станет существенной для вложения Йонеды (§14.2.7).

E/R/R-чтение. Функтор — это роль-перенос: он переводит элементы, роли и правила категории $\mathcal{C}$ в $\mathcal{D}$, сохраняя конституцию (тождество$\to$тождество, композиция$\to$композиция). Машинно проверено, что функтор сохраняет изоморфизмы (fmor_preserves_iso): роль «обратимость» переносится. Тождественный и композиция функторов (id_functor, compose_functor) ассоциативны на объектах (compose_functor_assoc).

Процессное чтение (мост к 14.6). В ToS есть и процессная сторона функториальности: производные функторы $R^{n}F$ как процесс приближений с убыванием поправки.²

Естественные преобразования и категория функторов $[\mathcal{C},\mathcal{D}]$

Естественное преобразование $\eta :F\Rightarrow G$ (между функторами $F,G:\mathcal{C}\to \mathcal{D}$) — семейство стрелок ${\eta }_a:Fa\to Ga$, согласованное с действием на морфизмах: для любого $f:a\to b$ квадрат коммутирует, ${\eta }_b\circ F(f)=G(f)\circ {\eta }_a$. Это правило когерентности (L5): семейство компонент действует «одинаково» по всей категории.

Машинно: Record NatTrans (nt_comp, nt_natural); тождественное преобразование id_nat_trans и вертикальная композиция vert_comp_nat_trans (та же Functor.v).

Категория функторов построена. Функторы $\mathcal{C}\to \mathcal{D}$ сами образуют категорию $[\mathcal{C},\mathcal{D}]$: объекты — функторы, морфизмы — естественные преобразования, композиция — вертикальная, равенство морфизмов — покомпонентное. Эта категория построена машинно, и все её законы выводятся покомпонентно из законов $\mathcal{D}$.³

Естественный изоморфизм: обратное естественно

Естественный изоморфизм — это в точности изоморфизм в категории функторов $[\mathcal{C},\mathcal{D}]$. Поэтому рефлексивность, симметрия и транзитивность достаются даром из общих свойств изоморфизма (§14.1); каждая компонента естественного изоморфизма — изоморфизм (а значит, моно и эпи).⁴

Содержательная теорема главы — natural_ inverse_ is_ natural:

Если естественное преобразование поточечно обратимо, то обратные компоненты автоматически естественны.

То есть «обратное к естественному изоморфизму естественно» доказывается, а не постулируется. С точки зрения L5/P4 это важно: естественность обратного — не дополнительное предположение, а вынужденное правило, вытекающее из естественности прямого преобразования и обратимости компонент (диаграммный обход, 0 аксиом). Правило конституирует объект (обратный изоморфизм), не позволяя ему быть «неестественным».

Представимый функтор и лемма Йонеды

Представимый функтор. Зафиксируем объект $x$. Функтор $\text{Hom}(x,-):\mathcal{C}\to \text{SetoidCat}$ посылает объект $a$ в hom-сетоид (носитель ${\text{Hom}}_{\mathcal{C}}(x,a)=‘ca{t}_{m}or‘xa$, равенство — сетоидное cat_mor_eq), а морфизм $f$ — в пост-композицию $g\mapsto f\circ g$. Функторные законы следуют из совместимости композиции, левой единицы и ассоциативности $\mathcal{C}$. Здесь окупается выбор \SetoidCat{} из 14.1: именно сетоидное равенство hom-множеств делает $\text{Hom}(x,-)$ функтором.⁵

Лемма Йонеды. Для любого функтора $F:\mathcal{C}\to \text{SetoidCat}$ и объекта $x$ естественные преобразования $\text{Hom}(x,-)\Rightarrow F$ находятся в биекции с элементами $F(x)$:

$$\text{Nat}(\text{Hom}(x,-),F)\cong F(x).$$

Биекция машинно доказана в обе стороны:

• $Y:\alpha \mapsto {\alpha }_x({\mathrm{id}}_x)$ (вычислить семейство на тождестве) — yoneda_to;
• $Y^{-1}:u\mapsto (a\mapsto (g\mapsto F(g)(u)))$ — yoneda_from;
• $Y\circ Y^{-1}=\mathrm{id}$ (через $F(\mathrm{id})=\mathrm{id}$) — yoneda_to_from; $Y^{-1}\circ Y=\mathrm{id}$ (через естественность $\alpha$) — yoneda_from_to; единственность — yoneda_unique.

Что говорит лемма (E/R/R / P4). Естественное семейство полностью определяется одним семенем — значением ${\alpha }_x({\mathrm{id}}_x)\in F(x)$; квадрат естественности есть правило восстановления $g\mapsto F(g)(u)$ всего семейства из этого семени. Поэтому «$\text{Nat}(\text{Hom}(x,-),F)$» — не завершённое множество всех преобразований (мощность), а конечное правило реконструкции. Это снимает обычную загадку «как одно значение знает всё естественное семейство»: естественность есть закон, элемент — семя.

Вложение Йонеды: объект определяется ролями

Морфизм $h:y\to x$ индуцирует естественное преобразование $\text{Hom}(x,-)\Rightarrow \text{Hom}(y,-)$ предкомпозицией ($g\mapsto g\circ h$). Машинно доказано, что это сопоставление полно и верно:

$$‘ca{t}_{m}or‘yx=\text{Hom}(y,x)\cong \text{Nat}(\text{Hom}(x,-),\text{Hom}(y,-)),$$

то есть верность (различные морфизмы дают различные преобразования) и полнота (каждое преобразование происходит из морфизма) — прямое следствие леммы Йонеды при $F:=\text{Hom}(y,-)$. Слева стоит именно $\text{Hom}(y,x)$: это контравариантность вложения — объект $x$ уходит в $\text{Hom}(x,-)$, а стрелка $h:y\to x$ даёт преобразование $\text{Hom}(x,-)\Rightarrow \text{Hom}(y,-)$ (в коде — yoneda_faithful, yoneda_full над cat_mor $yx$).⁶ Это и есть точная форма центрального тезиса:

объект полностью определён своей системой морфизмов — категорная форма P3 (тождество объекта — через его роли, не через «внутреннюю субстанцию»).

Честная стена (важно). Полнота и верность доказаны содержательно — как биекция hom-множества и множества естественных преобразований. Но собрать вложение Йонеды в единый Functor-объект ${\mathcal{C}}^{\mathrm{op}}\to [\mathcal{C},\text{SetoidCat}]$ не удаётся: запись Category мономорфна по вселенным, а $[\mathcal{C},\text{SetoidCat}]$ строго выше по вселенной, чем $\mathcal{C}$ (объекты \SetoidCat{} уже подняли уровень) — упаковка требует обратного неравенства. Это классическое «категория предпучков велика» — P4-граница размера, а не пробел в доказательстве: содержание вложения (полнота+верность) от этого большого объекта не зависит. Поэтому мы не утверждаем «вложение построено как функтор»; стену размера выносим в карту границ 14.7.

Разбор E/R/R: функтор, естественность, представление

Правила (L5). Сохранение тождества и композиции (конституция функтора); квадрат естественности (когерентность семейства); биекция Йонеды (правило восстановления семейства из семени и правило «объект$\leftrightarrow$его представимый функтор»).

Роли (L4). Функтор — роль-перенос (структуры $\mathcal{C}$ в $\mathcal{D}$); естественное преобразование — роль-семейство (когерентный набор компонент); $\text{Hom}(x,-)$ — роль «зондирование из $x$»; ${\alpha }_x({\mathrm{id}}_x)$ — роль-семя; вложение Йонеды — роль «представить объект его морфизмами».

{

Элементы (L1$+$P4). Конкретные данные: компоненты ${\eta }_a$, морфизмы $g:x\to a$, элементы $u\in F(x)$. Не элемент в смысле завершённой мощности: «множество всех естественных преобразований» (в рабочем слое это hom-сетоид категории $[\mathcal{C},\text{SetoidCat}]$ / правило восстановления, а не мощностная тотальность); и единый большой Functor-объект $[\mathcal{C},\text{SetoidCat}]$ как объект над $\mathcal{C}$ (стена размера).}

Компонент	Что фиксирует	E/R/R-категория
сохранение id/композиции; квадрат естественности; биекция Йонеды	конституцию переноса, когерентности и представления	Правило (L5)
функтор$=$перенос; естеств.\ преобр.$=$семейство; \Hom(x,-)$${}={}зонд; \alpha_x(\mathrm{id}_x)$${}={}семя	статус переносов и семейств	Роль (L4)
${\eta }_a$, $g:x\to a$, $u\in F(x)$	вычислимые носители	Элемент (L1$+$P4)

Что снимает разбор. Лемма Йонеды часто звучит мистически («объект знает всё о себе через стрелки»). ToS читает её как правило: естественность форсирует восстановление семейства из одного семени, а вложение делает «объект$=$его роли» точной биекцией. Загадки нет — есть закон (L5) и его семя (L1). А честная стена вселенных показывает, где сам категорный язык встречает P4: завершённую «категорию всех предпучков» как объект собрать нельзя.

Что глава подготовила

Установлены функторы (роль-перенос, сохраняют изоморфизмы), естественные преобразования и машинно построенная категория функторов $[\mathcal{C},\mathcal{D}]$; доказано, что обратное к естественному изоморфизму естественно; и, как кульминация, — лемма Йонеды и полно-верное вложение Йонеды (по локальному build — 0 аксиом, Print Assumptions$=$«Closed under the global context»; после синхронизации с main статус фиксируется). Содержательный итог: объект определяется своими ролями — категорная форма P3; честная стена: завершённую категорию предпучков как объект собрать нельзя (размер, P4).

Дальше — Глава 14.3: категория систем $\mathrm{Sys}(L)$, где тот же тезис получает свою изначальную, доонтологическую форму — P3_strictly_stronger_than_iso: изоморфные системы не обязаны быть лейбницево равны. Вложение Йонеды этой главы — абстрактная тень того же P3.

---

---

Часть: Часть XIV. Категория систем · Том: «Математика»

Навигация: ← Глава 1. Категории как метасистемы · Глава 3. Категория систем Sys(L) →

Footnotes

1. src/stdlib/Functor.v (18 Qed, 0 аксиом; в origin/main): Record Functor (fobj, fmor, fmor_compat, fmor_id, fmor_comp); id_functor, compose_functor, compose_functor_assoc; примеры ListFunctor, OptionFunctor, const_functor; fmor_preserves_iso (функтор сохраняет изоморфизмы). ↩

2. src/stdlib/ D1_DerivedFunctor.v (20 Qed; в origin/main): $R^{n}F$ как уровни процесса, каскад поправок $1/2^n$. ↩

3. src/category/ FunctorCategory.v (4 Qed, 0 аксиом): nt_eq (покомпонентное равенство), FunctorCat $\mathcal{C}\mathcal{D}$ как Category; мост FunctorCat_ iso_ componentwise (изоморфизм в $[\mathcal{C},\mathcal{D}]$ = поточечный изоморфизм). Оговорка о воспроизводимости (как в 14.1): слой src/category/ (13 файлов, 49 Qed, 0 аксиом, Print Assumptions$=$«Closed under the global context», commit 90ebd74) собран и проверен локально; синхронизация с основной веткой — пункт чек-листа. ↩

4. src/category/NaturalIsomorphism.v (7 Qed, 0 аксиом, тот же локальный слой): NaturalIso как is_iso в FunctorCat; nat_iso_id/nat_iso_sym/ nat_iso_trans; nat_iso_components (поточечный изоморфизм); компоненты моно/эпи. ↩

5. src/category/YonedaLemma.v (3 Qed, 0 аксиом, локальный слой): hom_setoid, representable ($\text{Hom}(x,-):\mathcal{C}\to \text{SetoidCat}$); yoneda_to, yoneda_from; yoneda_to_from, yoneda_from_to, yoneda_unique. ↩

6. src/category/YonedaEmbedding.v (3 Qed, 0 аксиом, локальный слой): yoneda_embed_mor (предкомпозиция), yoneda_faithful, yoneda_full. ↩