Сопряжённые функторы: универсальные оптимизации

Когда программист пишет curry/uncurry в Haskell или замечает, что ∃ и ∀ - это сопряжённые операции в логике, перед ним одна из самых универсальных конструкций в математике. Сопряжения формализуют идею «оптимального решения»: левый сопряжённый строит самый простой объект, правый - самый богатый. Это объединяет линейную алгебру, теорию групп, топологию и функциональное программирование.

• Curry-Howard-Lambek: сопряжения как семантика λ-исчисления и логических систем
• Galois connections в абстрактной интерпретации (static analysis, компиляторы)
• State/Reader монады в Haskell: прямое следствие сопряжений (S×−) ⊣ (S→−)

Предварительные знания

• ∞-Categories: Morphisms Between Morphisms

Сопряжение: определение и интуиция

Дэниел Кан ввёл сопряжённые функторы в 1958 году; к 1971 году Маклейн писал, что сопряжения встречаются «12 раз до завтрака» в математике - от свободных групп до двойственности Стоуна. **Сопряжение** F ⊣ G (F левый сопряжённый G, G правый сопряжённый F) - это пара функторов F: C → D, G: D → C с естественным изоморфизмом: Hom_D(F(A), B) ≅ Hom_C(A, G(B)) для всех A ∈ C, B ∈ D. Сопряжения - «наиболее частая конструкция в математике» (Маклейн): они появляются везде, где есть «свободный/забывчивый» или «оптимальный» способ перехода между структурами.

**«Сопряжения везде»:** Маклейн говорил, что сопряжения - «наиболее фундаментальная концепция» теории категорий. Свободное/забывчивое (алгебра), curry/uncurry (λ-исчисление), ∃/∀ (логика), прямой/обратный образ (геометрия), индукция/ограничение (теория представлений) - всё это сопряжения.

Единица и коединица сопряжения

Сопряжение F ⊣ G эквивалентно заданию пары натуральных преобразований: **единицы** η: Id_C → GF и **коединицы** ε: FG → Id_D, удовлетворяющих тождествам треугольников. Это даёт третье (эквивалентное) определение сопряжения и позволяет явно конструировать взаимное соответствие морфизмов.

**Треугольники = согласованность:** Тождества треугольников - не просто технические условия, а глубокое утверждение: «если вложить через η и потом оценить через ε, получим тождество». Они гарантируют, что соответствие Hom_D(FA,B) ≅ Hom_C(A,GB) действительно является взаимно обратным.

Каждое сопряжение порождает монаду

Из каждого сопряжения F ⊣ G возникает монада T = G ∘ F на C с единицей η: Id → GF и умножением μ = G(ε_F): GF GF → GF. Обратно, каждая монада возникает из некоторого сопряжения (двумя канническими способами: через Kleisli и через Эйленберга - Мура). Это объясняет глубинную связь сопряжений и монад.

**Теорема о сопряжённых функторах (RAPL):** Правые сопряжённые всегда сохраняют пределы; левые - копределы. Это объясняет, почему забывчивый функтор Grp → Set сохраняет произведения (G₁ × G₂ как множество = U(G₁) × U(G₂)), и почему свободный функтор сохраняет копроизведения.

Ключевые идеи

• F ⊣ G: Hom(FA, B) ≅ Hom(A, GB) - натуральный изоморфизм, не просто биекция
• Единица η: Id→GF и коединица ε: FG→Id с тождествами треугольников
• Правые сопряжённые сохраняют пределы; левые - копределы (RAPL/LAPC)
• Каждое сопряжение порождает монаду T=GF; каждая монада из сопряжения (Kleisli или Эйленберг - Мур)

Связанные темы

Сопряжения - связующая нить между монадами, пределами и теорией топосов.

• Монады — Каждое сопряжение F⊣G порождает монаду GF; это главная связь двух концепций
• Пределы и копределы — Правые сопряжённые сохраняют пределы - ключевая теорема; пределы характеризуют через сопряжения
• Теория топосов — Геометрические морфизмы топосов = пары сопряжённых функторов f*⊣f_*

Вопросы для размышления

• Почему curry и uncurry образуют сопряжение, а не просто взаимно обратные функции? В чём разница?
• Как квантификаторы ∃ и ∀ являются левым и правым сопряжёнными обратного образа? Проверьте на примере конкретного предиката.
• Нарисуйте все три способа смотреть на State-монаду: как на (T, η, μ), как на Kleisli-категорию и как возникающую из сопряжения. Убедитесь, что все три описания согласованы.

Связанные уроки

• ml-07
• plt-09-dependent-types