Лемма Ёнеды

«Объект полностью определяется своими связями» - это звучит как философия, но лемма Ёнеды делает из этого точную теорему. Она объясняет Church encoding в лямбда-исчислении, parametricity в системах типов, представляющие объекты в алгебраической геометрии. Это одна из самых «полезных» теорем в математике - и при этом одна из самых простых в формулировке.

• **Church encoding**: натуральные числа как функции `type Nat = <R>(f: (r: R) => R, z: R) => R` - это ровно вложение Ёнеды для натуральных чисел как монойда
• **Parametricity**: теорема Рейнольдса о параметрических типах - прямое следствие леммы Ёнеды. Полиморфная функция `id: <A>(a: A) => A` единственна - это Ёнеда
• **Алгебраическая геометрия**: схемы Гротендика определяются через их точки-морфизмы из других схем. «Представляемость функторов точек» - центральная задача модульной теории

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

• Adjoint Functors

Yoneda

Лемма Ёнеды - возможно, самый глубокий результат теории категорий. Её можно сформулировать так: **объект полностью определяется тем, как в него отображаются другие объекты**. Или двойственно: как он отображается в другие. Это категорное воплощение принципа «друзья объекта определяют его самого».

**Лемма Ёнеды**: для любой локально малой категории C, любого объекта A ∈ C и любого функтора F: C → Set существует естественная биекция: Nat(Hom(A, -), F) ≅ F(A). Здесь Nat - множество всех естественных преобразований. Биекция отправляет α: Hom(A,-) ⇒ F в элемент α_A(id_A) ∈ F(A).

Неформально: чтобы задать естественное преобразование из Hom(A,-) в F, достаточно выбрать один элемент F(A). Всё остальное определяется автоматически. Это удивительно: из одного «стартового» элемента вся бесконечная семья морфизмов α_B восстанавливается единственным образом.

Representable

Функтор F: C → Set называется **представимым**, если он изоморфен Hom(A,-) для некоторого A ∈ C. Представимые функторы - это «функторы, которые «помнят» объект». Лемма Ёнеды говорит: объект A полностью определяется функтором Hom(A,-). Это значит, что категорию C можно «вложить» в категорию функторов, не теряя информации.

Функтор F: C → Set **представим**, если существует объект A ∈ C и изоморфизм Nat(Hom(A,-), F) ≅ F(A), причём сам F ≅ Hom(A,-). Объект A называется **представляющим объектом** для F. Пара (A, u) где u ∈ F(A) - **универсальный элемент** - единственно определяет представление.

**Примеры представимых функторов**: в Top функтор «связные компоненты» π₀: Top → Set представим кругом S¹... нет: π₀ представим двухточечным пространством {0,1} - морфизмы {0,1} → X соответствуют парам точек из разных компонент. Функтор «фундаментальная группа» π₁: Top* → Grp - не представим в Top, но представим в категории H-пространств.

Presheaf

**Пресноп** (presheaf) на категории C - это контравариантный функтор F: C^{op} → Set, то есть функтор из противокатегории в Set. Пресноп «приписывает» каждому объекту множество «секций», а каждому морфизму - операцию «ограничения». Категория всех преснопов на C обозначается Ĉ = Set^{C^{op}} и является ключевым объектом теории категорий.

**Пресноп** на C - функтор F: C^{op} → Set. Для объекта U - множество F(U) «секций над U». Для морфизма f: V → U - функция ограничения F(f): F(U) → F(V). Категория Ĉ = [C^{op}, Set] называется **категорией преснопов** на C. Она обладает всеми пределами и копределами.

Важнейший пример: **топологические снопы**. Пресноп на открытых множествах топологического пространства X - это «локальные данные», определённые на каждом открытом U, с операциями ограничения. Если данные «склеиваются» согласованно, пресноп является **снопом** (sheaf). Снопы - основа современной алгебраической геометрии (Гротендик).

Embedding

Лемма Ёнеды немедленно даёт **вложение Ёнеды**: полный и точный функтор y: C → Ĉ = [C^{op}, Set], отправляющий A в пресноп Hom(-, A). Это означает: любая категория C вкладывается в более богатую категорию преснопов, не теряя информации. В Ĉ существуют все пределы и копределы - даже если в C их нет.

**Вложение Ёнеды** y: C → [C^{op}, Set] определено как y(A) = Hom_C(-, A). Это вложение **полное и точное** (fully faithful): Hom_C(A, B) ≅ Nat(y(A), y(B)). Следствие: A ≅ B в C тогда и только тогда, когда y(A) ≅ y(B) в Ĉ. Объект определяется своими «входящими стрелками».

**Практическое следствие**: для проверки изоморфизма A ≅ B достаточно проверить, что для всех X функции Hom(X, A) → Hom(X, B) являются биекциями, естественными по X. Это называется «принципом Ёнеды» - объект определяется своими «точками» из всех других объектов. В программировании это принцип «parametricity»: тип определяется своим поведением для произвольных аргументов.

**Теорема о плотности**: любой пресноп F: C^{op} → Set является колимитом представимых преснопов. Это категорная аналогия теоремы о том, что любая функция - предел (или колимит) дельта-функций. Вложение Ёнеды - «базис» в категории преснопов.

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

• **Лемма Ёнеды**: Nat(Hom(A,-), F) ≅ F(A) - естественное преобразование из Hom(A,-) определяется одним элементом
• **Представимый функтор** F ≅ Hom(A,-) - функтор, «помнящий» объект A; пара (A, u) с u ∈ F(A) единственна с точностью до изоморфизма
• **Пресноп** - контравариантный функтор C^{op} → Set; категория преснопов Ĉ полна и кополна
• **Вложение Ёнеды** y: C ↪ [C^{op}, Set] полное и точное: объект определяется своими входящими стрелками

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

Лемма Ёнеды связана с большинством конструкций теории категорий:

• Топосы — Топос - это категория преснопов с дополнительными аксиомами. Лемма Ёнеды - основа внутренней логики топоса
• Сопряжённые функторы — Представимые функторы тесно связаны с сопряжениями: правый сопряжённый представим через Hom

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

• Church encoding натуральных чисел: `type Nat = <R>(s: (r: R) => R, z: R) => R`. Покажите, что это вложение Ёнеды для натуральных чисел, рассматриваемых как моноид (ℕ, +, 0).
• Функтор F: C → Set называется «копредставимым» (corepresentable), если F ≅ Hom(-,A). Как это связано с вложением Ёнеды? Постройте двойственную версию леммы.
• Почему полнота и точность вложения y означает, что «объект определяется своими стрелками»? Сформулируйте это как конкретное утверждение об изоморфизмах.

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

• aa-03-homomorphisms
• plt-11-typeclasses