Глава 5. Сопряжения как универсальный язык двойственностей

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

Глава 14.4 предъявила одно сопряжение — $‘embed‘⊣‘forget‘$, корону P2. Эта глава поднимает взгляд: сопряжение — не разовая конструкция, а универсальный язык двойственностей. Один и тот же рисунок «левый$⊣$правый, единица, коединица, треугольники» повторяется по всему тому — от уровней до Галуа и геометрии-калибровки.

Мы делаем три вещи. Во-первых, выписываем общее сопряжение $F⊣G$ (не между уровнями, а между любыми категориями). Во-вторых, доказываем главное структурное следствие: правый сопряжённый сохраняет пределы (RAPL) — машинно для терминального случая, с честно обнажённой гипотезой естественности. В-третьих, разворачиваем каталог двойственностей тома и честно отмечаем, где мост есть сопряжение, а где — другой паттерн.

Ярусы главы (смешанные, честно). Общее $F⊣G$ и монада — stdlib/ (0 аксиом, в origin/main); RAPL — локальный слой src/category/ (0 аксиом, ожидает push); геом-калибровочная связь Галуа — процессный слой (наследует classic); Галуа полей — Часть XI (0 аксиом). Каждый якорь помечаем явно.

Общее сопряжение $F⊣G$

Сопряжение между категориями $C$ и $D$ — это пара функторов $F:C\to D$ (левый) и $G:D\to C$ (правый) вместе с единицей $\eta$ и коединицей $\epsilon$:

$${\eta }_c:c\to G(Fc),{\epsilon }_d:F(Gd)\to d,$$

подчинёнными двум треугольным тождествам. Машинно это запись Record Adjunction (adj_left $F$, adj_right $G$, adj_unit, adj_counit); тождества формализованы как triangle_left/triangle_right, их конъюнкция — is_adjunction. Тождественное сопряжение $C⊣C$ (оба функтора — тождество) служит конкретным свидетелем (id_adjunction, id_is_adjunction). ¹ Это алгебраический скелет двойственности: единица и коединица суть «почти-обратные» естественные переходы $1\Rightarrow GF$ и $FG\Rightarrow 1$, а треугольники следят за их когерентностью.

Честная граница записи. Record Adjunction несёт данные (единицу, коединицу) и треугольные тождества, но не несёт поля естественности единицы. Для большинства конкретных сопряжений естественность выполнена; но как поле записи её нет. Это станет важным уже в следующем разделе: глубокая теорема о пределах естественность требует — и мы предъявим её явной гипотезой, а не тихим допущением.

Что сохраняет правый сопряжённый: RAPL

Главное классическое структурное свойство сопряжений — слоган RAPL: «правые сопряжённые сохраняют пределы» (Right Adjoints Preserve Limits); двойственно, левые сохраняют копределы. В полном виде это теорема о произвольных пределах; мы доказываем её машинно для терминального объекта (предел пустой диаграммы):

$$\text{если }t\text{ терминален в }D,\text{то }Gt\text{ терминален в }C$$

(right_adjoint_preserves_terminal). В основе — лемма о биекции транспонирования:

$$G({\epsilon }_d\circ Fh)\circ {\eta }_c=h$$

(right_adjoint_transpose_roundtrip) — восьмишаговый диаграммный обход (функториальность $G$, ассоциативность, естественность $\eta$, треугольник, единицы). ²

Честно обнажённая гипотеза. Транспонирование становится биекцией лишь при естественности единицы — а её, как сказано, запись Adjunction не несёт. Поэтому мы вводим явный предикат unit_natural и добавляем его в посылки теоремы. Это не скрытая аксиома: гипотеза выполнима — для тождественного сопряжения она доказана (id_adjunction_unit_natural) и верна для любого сопряжения, чья единица есть настоящее естественное преобразование. Модель честной формализации: недостающее условие обнажается как посылка, а не протаскивается молча. (Полный RAPL для произвольных пределов — инкрементальная работа; терминальный случай схватывает суть.)

Монада — след сопряжения

У каждого сопряжения есть «тень» на одной стороне — монада $T=G\circ F$ (и двойственно комонада $F\circ G$). Монада — это паттерн вычисления: тип-конструктор с return и bind, подчинённый трём законам (левая/правая единица, ассоциативность). Машинно это Record Monad с инстансами Option/List/Result, композицией Клейсли (kleisli_assoc) и m_map. ³

Честная граница. Общая теорема «всякое сопряжение порождает монаду» как единый машинный результат у нас не оформлена (она требует естественности и треугольников, собранных в $\mu ,\eta$). Зато машинно проверены обе опоры по отдельности: (1) абстрактные законы монады (Monad.v, 0 аксиом); (2) конкретная монада сопряжения уровней — в процессном слое, наследующем classic, — $T=‘forget‘\circ ‘embed‘$, и она, в силу тугости 14.4, есть тождество (monad_is_identity), а двойственная комонада $‘embed‘\circ ‘forget‘$ изоморфна тождеству на забываемых. ⁴ Тривиальность этой монады — не бедность, а признак: единица-изоморфизм означает, что «круговой путь» уровня ничего не добавляет.

Каталог двойственностей тома

Один и тот же паттерн «$⊣$» встречается в томе трижды — в трёх разных кодировках. Сводим их в прозе (единый Coq-объект потребовал бы глубокой переунификации — кодировки гетерогенны).

(1) Уровни (Глава 14.4). $‘embed‘⊣‘forget‘$ — настоящее категорное сопряжение между $\text{Sys}(L)$ и $\text{Sys}(LSL)$, машинная форма P2; единица-изоморфизм, не эквивалентность (из-за P1). Ярус: 0 аксиом, origin/main.

(2) Галуа полей (Часть XI). Соответствие Галуа для $Q[\sqrt{2},\sqrt{3}]$ — антитонная связь Галуа: решётка подгрупп $\text{Gal}$ и решётка промежуточных полей соответствуют друг другу обращая включение (correspondence_inclusion_reversing), причём $[E:Q]=|\text{Gal}|=4$ (degree_equals_galois_order), а у $V_4$ ровно $5$ подгрупп (klein_four_subgroups). ⁵ Антитонная связь Галуа читается как сопряжение между порядком и обратным порядком — тот же скелет «$⊣$», обращающий направление; в формальном слое XI это конкретная таблица соответствия и correspondence_inclusion_reversing, а не теорема-объект полного poset-сопряжения.

(3) Геометрия$\leftrightarrow$калибровка (Часть XII, фаза 14A). Между упорядоченными геометриями («грубее$\le$тоньше») и калибровочными конфигурациями («тривиальнее$\le$возбуждённее») есть связь Галуа на порядках: $F\circ G\le \mathrm{id}$ доказано буквально (galois_lower_trivial: $F(G(gc))$ тривиальнее $gc$), а $\mathrm{id}\le G\circ F$ прочитывается через униформизацию геометрии (galois_upper); теорема geom_gauge_galois пакует компоненты (сохранение вершин, тривиализация связей, униформизация). Физический смысл: грубее геометрия$\to$тривиальнее калибровка; и обратно (galois_physical_meaning). ⁶ Важно: здесь строгое категорное сопряжение не проходит — его сознательно ослабили до связи Галуа на частичных порядках (это и есть честная конечно-процессная форма двойственности).

Что объединяет каталог. Кодировки гетерогенны: LevelAdjunction — точечное сопряжение с гипотезами; Галуа полей — решётки на nat; геом-калибровка — порядок $\le$ над ℚ. Они не сведены в один Rocq-объект Adjunction, и каталог честно остаётся прозаическим обобщением паттерна, а не единой машинной теоремой. Но паттерн один: левый$⊣$правый, единица, коединица, треугольники — язык, на котором том говорит о двойственностях.

Не всякий мост — сопряжение

Дисциплина языка требует обратного: уметь сказать, где сопряжения нет. Мост E/R/R$\to$калибровка — из таких. Там калибровочная группа есть группа автоморфизмов категории E/R/R: $\text{Aut}({\mathrm{ERR}}_N)$ имеет $N^2-1$ образующих, складывающихся в $SU(3)\times SU(2)\times U(1)$. Это функтор плюс группа автоморфизмов, а не сопряжение. ⁷ Вдобавок отождествление $\text{Aut}({\mathrm{ERR}}_N)\cong SU(N)$ — континуальный мост (требует топологию, которую P4 отдаёт процессным пределам), а не дискретная машинная теорема: доказана конечная структура (группа, счёт образующих), а группа Ли — концептуальный мост.

Урок методологический: категорный язык различает паттерны — сопряжение (уровни), связь Галуа (поля, геом-калибровка), функтор-автоморфизм (калибровка). Сваливать всё в «сопряжение» было бы overclaim; честная карта называет каждый паттерн своим именем. (Подробный разбор моста и его континуальной цены — в 14.7.)

Разбор E/R/R: сопряжение как E/R/R

Правила (L5). Треугольные тождества + естественность (там, где нужна, — честно обнажённая) + законы монады; для связей Галуа — в абстрактном чтении $F\circ G\le \mathrm{id}\le G\circ F$ (в файле раскрыто как тривиализация связей и униформизация геометрии). Эти правила конституируют двойственность как структуру, а не как метафору.

Роли (L4). Левый сопряжённый (свободно-подобный); правый (забывающий, предел-сохраняющий — RAPL); единица/коединица — переходы $1\Rightarrow GF$, $FG\Rightarrow 1$; монада — роль-след сопряжения; антитонная связь Галуа — роль-сопряжение на обратных порядках.

{

Элементы (L1$+$P4). Конкретные данные: id_adjunction; $T=‘forget‘\circ ‘embed‘=$тождество; $5$ подгрупп $V_4$ и $[E:Q]=4$; порядок $\le$ на геометриях/калибровках. Не поле текущей записи Adjunction: естественность единицы нужна как посылка/правило (обнажена как гипотеза unit_natural), а не как готовое поле записи. И $\text{Aut}({\mathrm{ERR}}_N)\cong SU(N)$ — континуальный предел (P4), не дискретный факт.}

Компонент	Что фиксирует	E/R/R-категория
треугольники + естественность + законы монады; $FG\le \mathrm{id}\le GF$	конституцию двойственности	Правило (L5)
левый$⊣$правый; единица/коединица; монада-след	статус функторов-партнёров	Роль (L4)
id_adjunction; $T=$тождество; $	V_4	$,$[E:ℚ]$;порядок$\le$

Диагностика P4. Континуальные стены проступают именно в двойственностях: $\text{Aut}\cong SU(N)$ требует топологии; строгое геом-калибровочное сопряжение не проходит и честно ослаблено до связи Галуа. P4 здесь не запрет, а указание масштаба: на конечно-процессном уровне двойственность жива как связь порядков; континуальная её форма — предел, не готовый объект.

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

Сопряжение предъявлено как язык: общее $F⊣G$ с единицей, коединицей и треугольниками (Adjunction.v); главное следствие — правый сопряжённый сохраняет пределы (RAPL, терминальный случай, машинно, с честно обнажённой естественностью); монада как след сопряжения (абстрактно — Monad.v; конкретно — тождественная монада уровней). Каталог тома собрал три двойственности (уровни / Галуа полей / геом-калибровка) под один паттерн и честно отметил, что мост E/R/R$\to$калибровка — не сопряжение, а функтор-автоморфизм.

Ярусы (честно). Общее сопряжение и монада — Adjunction.v (5 Qed) + Monad.v (20 Qed), 0 аксиом, origin/main. RAPL — RightAdjointPreservesLimits.v (3 Qed), 0 аксиом, но локальный слой src/category/ (90ebd74), ожидает push. Галуа полей — Часть XI (0 аксиом, origin/main). Геом-калибровка — ProcessGGGalois.v (15 Qed), процессный слой (числит classic), origin/main.

Дальше — Глава 14.6: процессы как универсальные конструкции (P4: пределы и копределы суть процессы) и топосный набор SetoidCat (конечные (ко)пределы, декартова замкнутость, предикатный классификатор подобъектов) — два прочтения универсальных конструкций, процессное и сетоидно-топосное.

---

---

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

Навигация: ← Глава 4. Функторы между уровнями и сопряжение · Глава 6. Процессы как универсальные конструкции; Setoid как топос →

Footnotes

1. src/stdlib/Adjunction.v (5 Qed, 0 Admitted, 0 аксиом; в origin/main): Record Adjunction (mkAdj), triangle_left/_right, is_adjunction, id_adjunction, id_adjunction_triangle_left/_right, id_is_adjunction, id_defect_zero. (Лемма adjunction_unique_up_to_iso в файле — placeholder тождественного случая, а не общая теорема единственности правого сопряжённого: последняя не формализована.) ↩

2. src/category/RightAdjointPreservesLimits.v (3 Qed, 0 Admitted, 0 аксиом; локальный слой src/category/, коммит 90ebd74, ожидает git push): unit_natural, id_adjunction_unit_natural, right_adjoint_ transpose_ roundtrip, right_adjoint_ preserves_ terminal. ↩

3. src/stdlib/Monad.v (20 Qed, 0 Admitted, 0 аксиом; в origin/main): Record Monad, m_left_id/m_right_id/m_assoc; OptionMonad, ListMonad, ResultMonad; kleisli_assoc, kleisli_id_left/_right, m_map_id. ↩

4. src/process/ProcessAdjunction.v (процессный слой, наследует classic; в origin/main): level_monad, monad_is_identity, monad_unit_is_iso; level_comonad, comonad_counit_is_iso. ↩

5. src/algebra/GaloisQ23.v, GaloisDegreeQ23.v, GaloisCorrespondence.v (Часть XI, 0 аксиом; в origin/main): fixed_by, base_fixed_by_all, correspondence_ inclusion_ reversing, degree_ equals_ galois_ order, klein_four_subgroups. ↩

6. src/process/ProcessGGGalois.v (15 Qed, 0 Admitted; процессный слой, импортирует Classical — наследует classic; в origin/main): geom_coarser, gauge_more_trivial, galois_lower_trivial, galois_upper, geom_gauge_galois, galois_physical_meaning. ↩

7. src/foundation/ERRGaugeFunctorSynthesis.v (9 Qed по грэпу; баннер «12»; 0 Admitted; в origin/main): distinction_is_category, gauge_is_automorphism, generators_match_sm, err_gauge_synthesis. ↩