Глава 4. Функторы между уровнями и сопряжение

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

Главы 14.1–14.3 работали внутри одного уровня: категория как метасистема (14.1), функторы и вложение Йонеды (14.2), категория систем $\text{Sys}(L)$ с ядром P3 (14.3). Эта глава делает шаг, ради которого вся иерархия и затевалась, — она строит функторы между уровнями и показывает, что их связь есть точное категорное сопряжение. Это корона Части XIV: принцип P2 (Дополнительность) получает машинную форму.

Две стрелки соединяют соседние уровни. Вложение

$$‘embed‘:\text{Sys}(L)⟶\text{Sys}(LSL)$$

поднимает систему на следующий уровень; забывание

$$‘forget‘:\text{Sys}(LSL)\rightharpoonup \text{Sys}(L)$$

опускает её обратно — но частично (значок $\rightharpoonup$). Главный результат:

$‘embed‘⊣‘forget‘$ — сопряжение, и это и есть P2 (Дополнительность): два дополнительных взгляда на одну структуру, ни один из которых сам по себе не полон.

Якоря сопряжения — LevelFunctors.v, LevelAdjunction.v и (для имени P2) ProcessAdjunction.v — все в основной ветке (origin/main): можно ссылаться уверенно, как в 14.3. Общая рамка «эквивалентность категорий» опирается на новый локальный слой src/category/ (помечаем отдельно).

Иерархия уровней: отношение $\ll$

Стрелки embed/forget движутся вдоль хребта ToS — строгого порядка на уровнях. Тип Level порождён двумя конструкторами (дно L1 и переход к следующему LS), а отношение $w\ll L$ («уровень $w$ ниже $L$») есть фундированный строгий порядок. ¹ Нам понадобятся ровно четыре его свойства: транзитивность ($w\ll L\ll LSL\Rightarrow w\ll LSL$), факт $L\ll LSL$ (каждый уровень ниже следующего), иррефлексивность $\neg (L\ll L)$ — это и есть P1 (запрет самопринадлежности в форме «уровень не ниже самого себя»), — и разрешимость сравнения. Иррефлексивность окажется тем самым местом, где forget наталкивается на обструкцию.

embed: уровень вкладывается в следующий

Вложение системы $S$ с уровня $L$ на $LSL$ оставляет те же элементы, тот же критерий и того же свидетеля $w$; меняется лишь доказательство его законности: было $w\ll L$, стало $w\ll LSL$ — через транзитивность и $L\ll LSL$. На элементах ничего не происходит:

$$‘ElemOf‘(LSL)(‘embed‘S)=‘ElemOf‘LS$$

дефиниционно (embed_obj_elem_eq, level_bridge); морфизм вкладывается той же функцией на элементах (embed_preserves_structure).

Это полноценный функтор — EmbedFunctor $L:\text{Sys}(L)\to \text{Sys}(LSL)$: он сохраняет тождество и композицию, верен (embed_faithful), сохраняет вложения, сюръекции и изоморфизмы (embed_ preserves_ embedding, embed_ preserves_ surjection, embed_ preserves_ iso), а пустую систему переводит в инициальную (embed_ empty_ is_ initial). ² Содержательное прочтение прямое: нижний уровень сидит в верхнем без искажения — элементы, критерий и сеть морфизмов переносятся один в один. Уровень-структура «невидима снизу»: с точки зрения элементов $S$ и $‘embed‘S$ неотличимы.

forget: частичное забывание уровня

Обратный ход опускает систему с $LSL$ на $L$, и здесь возникает асимметрия. Система с $LSL$ забываема (is_forgettable), если её свидетель строго ниже $L$:

$$‘i{s}_{f}orgettable‘LT:=(\text{свидетель }T)\ll L.$$

Только при этой гипотезе можно построить forget_obj $LT{H}_f:\text{Sys}(L)$ — законность свидетеля на новом уровне даёт сама гипотеза $H_f$.

Обструкция P1. Не всякая система с $LSL$ забываема. Возьмём систему, чей свидетель равен $L$ (witness_L_system): забыть её значило бы получить $L\ll L$, что запрещено иррефлексивностью — P1. Поэтому (witness_L_not_forgettable)

$$‘P{1}_{o}bstruct{s}_{t}ota{l}_{f}orget‘:\exists T,\neg ‘i{s}_{f}orgettable‘LT.$$

Сама забываемость разрешима (is_forgettable_dec): для каждой системы можно вычислить, опускается она или нет.

Почему forget не упаковывается в Functor. Раз forget определён лишь на части объектов (нужна гипотеза $H_f$), он не образует instance Rocq-структуры Functor (та требует тотального fobj на всех объектах). Это не лень формализации, а честная конституция: сопряжение записано как набор standalone-лемм с явными гипотезами forgettability, а не как пара функторов. ³ Тем не менее все свойства сопряжения — хом-биекция, естественность, единица, коединица, треугольники — доказаны поточечно (следующий раздел). forget_mor верен на своей области определения и сохраняет вложения (forget_faithful, forget_ preserves_ embedding).

Сопряжение $‘embed‘⊣‘forget‘$ — это P2

Сердце главы. Между уровнями есть естественная биекция хом-множеств:

$${\text{Hom}}_{\text{Sys}(LSL)}(‘embed‘S,T)\cong {\text{Hom}}_{\text{Sys}(L)}(S,‘forget‘T),$$

слева направо — adj_forward, справа налево — adj_backward; обе стороны взаимно обратны (level_adjunction) и естественны по $S$ и по $T$ (adj_natural_S, adj_natural_T, adj_naturality_square). По определению сопряжения это значит: embed — левый сопряжённый, forget — правый. ⁴

Единица и коединица. Единица ${\eta }_S:S\to ‘forget‘(‘embed‘S)$ — это изоморфизм (adjunction_unit_is_iso); более того, $‘forget‘(‘embed‘S)=S$ лейбницево (forget_embed_roundtrip). Коединица ${\epsilon }_T:‘embed‘(‘forget‘T)\to T$ — изоморфизм для забываемых $T$ (adjunction_ counit_ is_ iso_ for_ forgettable). Оба треугольных тождества выполнены (triangle_identity_1, triangle_identity_2). Поскольку единица — изоморфизм, сопряжение «тугое»; категорно это означает, что embed вполне верен (fully faithful). Машинно явно доказана верность (embed_faithful), а полнота следует из изоморфности единицы (forget_ embed_ adjunction_ tight) — это согласуется с тем, что мы уже знали про embed напрямую. ⁵

Почему это P2 (Дополнительность). P2 утверждает, что у системы есть дополнительные аспекты, не специфицируемые одновременно. Категорно это и есть пара сопряжённых: embed добавляет уровень-структуру, forget её снимает — два дополнительных взгляда на одну структуру, ни один из которых сам по себе не есть полная картина. Этот тезис собран машинно: P2_categorical/P2_holds (сопряжение на каждом уровне), P2_unit_is_iso, P2_counit_is_iso_forgettable, и обобщающая P2_grand_summary. ⁶

Это не эквивалентность. Из обструкции P1 следует, что forget не тотален, а значит сопряжение не есть эквивалентность категорий (complementarity_not_equivalence): среди систем уровня $LSL$ есть незабываемые, до которых снизу не дотянуться. В этом и состоит асимметрия дополнительности (complementarity_asymmetry): вверх-и-вниз возвращает исходное ($‘forget‘\circ ‘embed‘=\mathrm{id}$), но вниз-и-вверх покрывает лишь забываемую часть.

Эквивалентность категорий: одинаковость с точностью до роли

Сопряжение уровней — частный (и «тугой») случай. Общее понятие «две категории суть одно и то же с точностью до роли» есть эквивалентность. Мы строим её как ToS-структуру: CatEquiv $CD$ несёт два функтора $F:C\to D$, $G:D\to C$ и естественные изоморфизмы ${\mathrm{id}}_C\cong G\circ F$, $F\circ G\cong {\mathrm{id}}_D$. Обратные к единице и коединице несутся как данные (а не как существование внутри Prop), поэтому симметрия $D\simeq C$ — чистая перестановка полей (equiv_sym). ⁷ Единица и коединица оказываются естественными изоморфизмами (ce_unit_is_nat_iso, ce_counit_is_nat_iso), а оба функтора — существенно сюръективны (equiv_F_ess_surjective, equiv_G_ess_surjective): каждый объект цели изоморфен образу некоторого объекта источника. Рефлексивность даёт тождественная эквивалентность $C\simeq C$ (id_equiv), где все четыре естественных преобразования суть тождества. ⁸

Эхо P3. Эквивалентность слабее изоморфизма категорий: не требуется $G\circ F=\mathrm{id}$ «в точности», а лишь $G\circ F\cong \mathrm{id}$. Это прямой категорный отголосок P3 из 14.3: «одинаковость» естественно мерить с точностью до изоморфизма, а не до лейбницева равенства.

Контраст с уровнями. Сопряжение $‘embed‘⊣‘forget‘$ даже туже, чем нужно для эквивалентности (единица — изоморфизм всегда, коединица — изоморфизм на забываемой части), — и всё же эквивалентностью не является: embed не существенно сюръективен (незабываемые системы P1). Значит $\text{Sys}(L)$ сидит в $\text{Sys}(LSL)$ как полная роль-подчасть с частичным возвратом (forget) на забываемых объектах, но не исчерпывает её. Эквивалентность же — верный масштаб «одинаковости с точностью до роли» для целых категорий, и им мы будем мерить двойственности тома в 14.5.

Разбор E/R/R: межуровневая структура как E/R/R

Правила (L5). Функторные законы embed (сохранение тождества/композиции) + законы сопряжения (треугольники, естественность по обоим аргументам) + дополнительность P2 ($‘embed‘⊣‘forget‘$) + обструкция P1 (forget частичен: $\neg L\ll L$). Эквивалентность задаёт правило «одинаковость с точностью до роли» (эхо P3).

Роли (L4). embed — левый сопряжённый (свободно-подобное вложение); forget — правый (забывающий, частичный); единица — роль «нижнее сидит в верхнем» (iso); коединица — роль «восстановить забываемое»; эквивалентность — роль «то же с точностью до роли».

{

Элементы (L1$+$P4). Конкретные данные: ElemOf, переносимые embed один в один (level_bridge); свидетель $w\ll L$ — вычислимый «ключ», открывающий забывание; система witness_L_system ($w=L$) — конкретный свидетель невозможности тотального forget. Не элемент межуровневой наблюдаемости: тотальность forget — P1 прямо запрещает её (нельзя опустить всё с $LSL$ на $L$).}

Компонент	Что фиксирует	E/R/R-категория
функторные законы embed + треугольники/естественность + P2 + P1-обструкция	конституцию межуровневой связи	Правило (L5)
embed$=$левый сопр.; forget$=$правый (частичный); $\eta ,\epsilon$ как роли	статус стрелок между уровнями	Роль (L4)
ElemOf; свидетель $w\ll L$; witness_L_system	вычислимые носители и «ключ» забывания	Элемент (L1$+$P4)

Диагностика P4. Почему forget частичен? Потому что иерархия обоснована: нет $L\ll L$, шаг вниз не всегда возможен — уровень-под-собой должен реально существовать. Это не дефект, а та же конечная актуальность, что в 14.3 не позволяла поставить пустую/единичную систему на дно: «опустить уровень» осмысленно лишь там, где есть куда опускать.

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

Построены функторы между уровнями: embed — полноценный верный функтор $\text{Sys}(L)\to \text{Sys}(LSL)$, сохраняющий вложения/сюръекции/изоморфизмы; forget — частичное забывание, ограниченное обструкцией P1 (P1_obstructs_total_forget, разрешимо). Их связь — сопряжение $‘embed‘⊣‘forget‘$ с биекцией хом-множеств, единицей-изоморфизмом (откуда embed вполне верен) и коединицей-изоморфизмом на забываемых; это машинная форма принципа P2 (Дополнительность). Сопряжение не эквивалентность — ровно из-за P1. Общую рамку «одинаковость с точностью до роли» даёт CatEquiv (симметрия, рефлексивность, существенная сюръективность), категорное эхо P3.

Ярусы (честно). Ядро сопряжения — LevelFunctors.v (30 лемм) + LevelAdjunction.v (25 Qed) — 0 аксиом, в origin/main. Имя P2 и монада/комонада — ProcessAdjunction.v (синтетический слой, числит classic), тоже в origin/main. Рамка эквивалентности — EquivalenceOfCategories.v (7 Qed) + IdentityEquivalence.v (2 Qed) — 0 аксиом, но локальный слой src/category/ (коммит 90ebd74), ожидает git push.

Дальше — Глава 14.5: сопряжения $F⊣G$ как универсальный язык двойственностей; правый сопряжённый сохраняет пределы (RAPL, терминальный случай — машинно); и каталог сопряжений тома (уровни здесь / Галуа из Части XI / геометрия-калибровка из Части XII) как сквозная нить.

---

---

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

Навигация: ← Глава 3. Категория систем Sys(L) · Глава 5. Сопряжения как универсальный язык двойственностей →

Footnotes

1. src/TheoryOfSystems_Core_ERR.v: Level (L1, LS), level_lt (обозначение $\ll$), level_lt_trans (транзитивность), level_lt_LS ($L\ll LSL$), level_lt_irrefl ($\neg L\ll L$ — это P1), level_lt_dec (разрешимость). Замечание: речь о системной иерархии Level, а не об ординалах (foundation/Ordinal.v) или геометрических уровнях DOF (foundation/LevelStructure.v) — это разные понятия «уровня». ↩

2. src/LevelFunctors.v (30 доказанных лемм, 0 Admitted, 0 аксиом; в origin/main; из них 3 закрыты Defined. — embed_is_forgettable, embed_2_forgettable_to_LS/_to_L, — остальные Qed.): embed_obj, embed_mor, EmbedFunctor, embed_obj_elem_eq, embed_faithful, embed_preserves_iso, embed_empty_is_initial и др. ↩

3. Ключевая ремарка src/LevelAdjunction.v (строки 11–14): «Since forget is partial (requires is_forgettable), we cannot form a proper Functor instance for it. Instead, we prove all adjunction properties as standalone lemmas with explicit forgettability hypotheses.» ↩

4. Направление фиксируется самой биекцией. Сопряжение $F⊣G$ (где $F$ левый, $G$ правый) есть ${\text{Hom}}_D(Fc,d)\cong {\text{Hom}}_C(c,Gd)$; сопоставляя, $F=‘embed‘$, $G=‘forget‘$. Это форма «свободный $⊣$ забывающий»: embed свободно вкладывает, forget забывает уровень. То же подтверждают единица ${\eta }_S:S\to ‘forget‘(‘embed‘S)$ (вид $1\to GF$) и коединица ${\epsilon }_T:‘embed‘(‘forget‘T)\to T$ (вид $FG\to 1$). Каноническое машинное утверждение P2_categorical (ProcessAdjunction.v) формулирует ровно «Embed $⊣$ Forget». В старых шапках файлов (LevelAdjunction.v, ProcessAdjunction.v) может встречаться обратная словесная маркировка ролей — направление здесь фиксируется не баннером, а самой хом-биекцией: $\text{Hom}(‘embed‘S,T)\cong \text{Hom}(S,‘forget‘T)$, значит $‘embed‘⊣‘forget‘$. ↩

5. src/LevelAdjunction.v (25 Qed, 0 Admitted, 0 аксиом; в origin/main): adj_forward/adj_backward, level_adjunction, adj_natural_S/_T, adjunction_unit_component/_is_iso, adjunction_counit_component, triangle_identity_1/_2, embed_reflects_iso, forget_embed_adjunction_tight, adj_preserves_iso/adj_reflects_iso. ↩

6. src/process/ProcessAdjunction.v — синтетический P2-слой (0 Admitted; в origin/main). Файл лежит в процессном слое и импортирует Classical, поэтому наследует classic в ярусе — но переэкспортируемое ядро сопряжения суть те же 0-аксиомные леммы из LevelAdjunction.v. Здесь же — монада $‘forget‘\circ ‘embed‘$ (которая есть тождество, monad_is_identity) и комонада $‘embed‘\circ ‘forget‘$ (comonad_counit_is_iso). ↩

7. src/category/EquivalenceOfCategories.v (7 Qed, 0 Admitted, 0 аксиом; локальный слой src/category/, коммит 90ebd74, ожидает git push): Record CatEquiv, ce_unit_is_nat_iso, ce_counit_is_nat_iso, equiv_F_ess_surjective, equiv_G_ess_surjective, equiv_sym, equiv_F_preserves_iso; определения is_ess_surjective/is_faithful/is_full. В отличие от LevelFunctors.v/LevelAdjunction.v (в origin/main), этот раздел опирается на локальный слой src/category/ — до push его статус не смешиваем с подтверждённым origin/main. ↩

8. src/category/IdentityEquivalence.v (2 Qed, 0 аксиом; локальный слой): id_equiv, id_equiv_unit_components, id_equiv_ess_surjective. Вместе с equiv_sym это рефлексивность и симметрия $\simeq$; транзитивность (склейка эквивалентностей) оставлена на потом. ↩