Bổ đề Yoneda trong phạm trù đôi: Khi lý thuyết phạm trù vượt qua giới hạn của tập hợp

Bartosz Milewski vừa đăng bài viết mới trên blog cá nhân, tiếp tục chuỗi bài về lý thuyết phạm trù nâng cao. Lần này, ông tập trung vào một chủ đề khá hàn lâm nhưng có ý nghĩa nền tảng: làm thế nào để phát biểu Bổ đề Yoneda — một trong những kết quả quan trọng nhất của lý thuyết phạm trù — trong ngữ cảnh phạm trù đôi (double categories).

Điểm thú vị là bài viết không chỉ dừng ở toán học thuần túy, mà còn đặt nền móng cho một hiện thực hóa bằng Haskell ở phần tiếp theo.

Vấn đề: Nói về presheaf mà không được nhắc đến tập hợp

Tác giả mở đầu bằng một cách diễn đạt giàu hình ảnh: khi làm việc với phạm trù đôi, ta giống như đang chơi một trò chơi "hãy nói về tập hợp mà không được nhắc đến tập hợp". Thay vì nói về hom-set, ta nói về đơn vị nằm ngang (horizontal units). Đằng sau cách nói này là một trực giác: các mũi tên nằm ngang thực chất được hình dung như các profunctor, và đơn vị của phép hợp thành profunctor chính là một hom-functor.

Vấn đề nảy sinh khi ta muốn định nghĩa presheaf — vốn theo truyền thống là các functor nhận giá trị trong phạm trù Set. Nếu không được nhắc đến Set, ta mất luôn công cụ để phát biểu Bổ đề Yoneda. Đây chính là điểm mấu chốt mà Milewski muốn giải quyết.

"Đôi khi bạn chỉ cần nói về presheaf mà không được phép nhắc đến presheaf."

Ông chỉ ra rằng nhiều cấu trúc phạm trù tiêu chuẩn — như giới hạn có trọng số (weighted limits), mở rộng Kan, hay phạm trù phần tử (tabulations) — có thể được tổng quát hóa bằng profunctor. Nhưng riêng Bổ đề Yoneda thì cần một cách tiếp cận đặc biệt hơn.

Chiến lược: Định nghĩa mọi thứ bằng cấu trúc phổ quát

Ý tưởng cốt lõi của bài viết là: trong phạm trù đôi, các 0-cell đại diện cho các phạm trù, nhưng ta không có quyền truy cập trực tiếp vào các vật thể của chúng. Do đó, mọi định nghĩa phải được thực hiện thông qua cấu trúc phổ quát (universal constructions).

Cụ thể, tác giả cần xây dựng:

• Một vật thể 0-cell biểu diễn phạm trù presheaf
• Một mũi tên thẳng đứng (1-cell) đóng vai trò phép nhúng Yoneda (Yoneda embedding)

Ngay cả thao tác đơn giản nhất — áp dụng một presheaf lên một vật thể để thu được một tập hợp — cũng phải được định nghĩa "theo lô", như một mũi tên nằm ngang cụ thể.

Phân loại mũi tên: Từ functor đến profunctor và ngược lại

Milewski trình bày một quan sát quan trọng: có thể chuyển đổi qua lại giữa functor và profunctor theo hai cách chính tắc, tương ứng với companion và conjoint trong một proarrow equipment.

Một profunctor, khi được curry hóa, có thể được xem như một functor đi vào phạm trù presheaf. Tác giả ký hiệu phạm trù presheaf trên phạm trù A là:

Ký hiệu phạm trù presheaf

Phép tương đương này có thể được viết dưới dạng một biến đổi tự nhiên khả nghịch. Một chi tiết tinh tế mà tác giả nhấn mạnh: khi áp dụng một vật thể trong phạm trù presheaf lên một đối tượng khác, thực chất ta đang sử dụng counit của adjunction curry hóa — tức evaluation (pro-)functor.

Phép nhúng Yoneda và tính dày đặc

Câu hỏi tiếp theo: đâu là mũi tên phân loại cho mũi tên đơn vị (unit arrow) — mũi tên nằm ngang đơn giản nhất? Trong phạm trù Set, mũi tên đơn vị chính là hom-profunctor, và mũi tên phân loại của nó chính là functor Yoneda.

Khi so sánh 2-cell định nghĩa sự phân loại này với định nghĩa của phép nhúng Yoneda, ta nhận ra một điều thú vị: trong một proarrow equipment, evaluation profunctor chính là companion của functor Yoneda.

Phép nhúng Yoneda như một companion

Tác giả cũng muốn phép nhúng Yoneda có tính dày đặc (dense) — đây là tổng quát hóa của khẩu hiệu nổi tiếng "mọi presheaf đều là colimit của các representable". Tính chất này được biểu diễn qua mở rộng Kan trái.

Adjunction: Nửa còn lại của Bổ đề Yoneda

Phần hấp dẫn nhất của bài viết có lẽ là khi tác giả phân tích adjunction giữa companion và conjoint. Trong trường hợp của mũi tên Yoneda, adjunction này đọc là:

Adjunction của companion và conjoint

Tác giả chỉ ra rằng counit của companion cung cấp một nửa của Bổ đề Yoneda. Trong phạm trù Set, đây chính là kết quả quen thuộc. Tuy nhiên, trong một equipment tùy ý, nửa còn lại — chiều từ phải sang trái — không tự động đúng.

Để có được một Bổ đề Yoneda đầy đủ, ta cần thêm điều kiện rằng unit của adjunction phải là một đẳng cấu. Trong Set, đây chính là cách chứng minh kinh điển rằng phép nhúng Yoneda là đầy đủ và trung thành (full and faithful).

Điều kiện cho cấu trúc Yoneda

Kết hợp hai điều kiện:

1. Unit của adjunction là đẳng cấu
2. Functor Yoneda có tính dày đặc

...ta thu được những equipment được gọi là có cấu trúc Yoneda (Yoneda structure). Đây là những equipment sở hữu các vật thể presheaf và các phép nhúng Yoneda hoạt động tốt.

Milewski kết thúc bằng lời cảm ơn John Baez vì những góp ý xây dựng, đồng thời hứa hẹn phần tiếp theo sẽ trình bày một hiện thực hóa đồ chơi bằng Haskell.

Ý nghĩa với giới lập trình viên

Với những ai quan tâm đến lý thuyết phạm trù ứng dụng trong lập trình hàm, bài viết này là một bước tiến quan trọng. Bổ đề Yoneda vốn đã xuất hiện trong các thư viện Haskell dưới dạng forall r. (a -> r) -> f r, nhưng việc hiểu nó trong bối cảnh phạm trù đôi mở ra hướng tổng quát hóa sâu sắc hơn — nơi các khái niệm như profunctor, optics, và lens đều có thể được nhìn nhận lại.

Đây là kiểu bài viết đòi hỏi nền tảng toán học vững chắc, nhưng lại có ích trực tiếp cho những kỹ sư đang làm việc với các abstraction phức tạp trong ngôn ngữ lập trình hàm.

Người đọc có thể theo dõi toàn bộ bài viết gốc tại blog của Bartosz Milewski và thảo luận trên Hacker News.