Unbiasing symmetric monoidal categories in Lean

1. 문제 제기 (Problem)

• 편향된 정의의 한계: 기존의 대칭 모노이드 범주 정의는 이항 텐서 곱 ($\otimes$), 단위원 (unit), 그리고 결합자 (associator), 단위원자 (unitor), 브레이딩 (braiding) 등의 구조를 기반으로 합니다. 이는 낮은 차수 (low-arity) 의 데이터만 필요로 하여 정의는 간단하지만, 임의의 유한 개수 (higher arities) 에 대한 텐서 곱을 다룰 때는 복잡해집니다.
• 실용적 필요성: 대수학이나 위상수학에서 유한 집합에 대한 합이나 곱과 같은 연산은 순서가 고정되지 않은 임의의 유한 집합 위에서 정의되어야 합니다. 예를 들어, 유한 군 $G$의 표현론에서 $\sum_{\rho \in \text{Irr}(G)} (\dim \rho)^2 = |G|$와 같은 식은 순서에 무관한 합을 요구합니다.
• 고차 범주론 (Higher Category Theory) 과의 연결: 대칭 모노이드 범주는 $(\infty, 1)$-범주 이론에서 중요한 역할을 합니다. Lurie 의 $\infty$-operads 나 Cranch 의 Lawvere 대칭 모노이드 $(\infty, 1)$-범주와 같은 모델들은 본질적으로 편향 제거된 (unbiased) 형태, 즉 모든 차수의 텐서 곱을 포함하는 구조로 정의됩니다. 기존 Lean/Mathlib 의 편향된 정의는 이러한 고차 범주론적 관점과 연결하는 데 장벽이 됩니다.
• 현재 상태: Mathlib 에는 모노이드 범주의 일관성 정리 (coherence theorem) 가 형식화되어 있지만, 대칭 모노이드 범주의 편향 제거 과정 자체는 형식화되어 있지 않았습니다.

2. 방법론 (Methodology)

저자는 Mac Lane 의 일관성 정리를 기반으로 하여, 대칭 모노이드 범주를 스팬 (spans) 의 (2,1)-범주에서 Cat-값의 의사함수 (pseudofunctor) 로 확장하는 접근법을 취했습니다.

A. 대칭 리스트 (Symmetric Lists) 와 일관성 정리

• 대칭 리스트의 정의: Piceghello 의 HoTT(Homotopy Type Theory) 기반 연구를 Lean/Mathlib(비-HoTT 환경) 에 맞게 재구성했습니다. 대칭 리스트는 생성자와 관계로 정의된 범주 $SList(J)$로, 객체는$J$의 리스트이고, 사상은 교환 (swap) 과 리스트 접미 (cons) 연산으로 생성됩니다.
• 코크터 군 (Coxeter Groups) 과의 대응: 대칭 리스트의 사상들은 $A_\infty$ 타입의 코크터 군 (즉, 무한 대칭군) 의 원소로 레이블링될 수 있음을 증명했습니다. 이는 Mac Lane 의 일관성 정리를 구체화하여, 두 텐서 곱 사이의 모든 "캐논ical" 사상이 유일함을 보여줍니다.
  • 주요 결과 (Theorem 2.8): 대칭 리스트의 두 사상이 같을 필요충분조건은 그들이 $A_\infty$에서 같은 레이블 (치환) 을 가지는 것입니다.
• 자유 대칭 모노이드 범주: 대칭 리스트 범주 $SList(J)$가 집합$J$ 위의 자유 대칭 모노이드 범주와 동치임을 증명했습니다 (Theorem 2.10).

B. 스펜 (Span) 범주와 의사함수 구성

• 스팬의 Pith: 범주 $C$의 스펜 (spans) 으로 이루어진 이차 범주 (bicategory) 의 'pith' (가역적인 2-사상만 남긴 부분) 를 다룹니다.
• Pith-Beck-Chevalley 시스템: 편향 제거된 대칭 모노이드 범주를 구성하기 위해, 스펜 범주에서 타겟 범주로 가는 의사함수를 정의하는 새로운 구조인 Pith-Beck-Chevalley 시스템을 도입했습니다. 이는 두 개의 의사함수 (공변적 $U$와 반변적 $V$) 와 카르테시안 사각형 (pullback square) 에 대한 기저 변경 (base change) 동형사상으로 구성됩니다.
• Kleisli 이차 범주: 대칭 모노이드 범주의 보편적 성질을 인코딩하기 위해 **대칭 리스트의 Kleisli 이차 범주 ($K_{SList}$)**를 정의했습니다. 이는 대칭 모노이드 범주를 $K_{SList}^{op}$에서 Cat 으로 가는 의사함수로 해석할 수 있게 합니다.

C. 편향 제거 과정의 구체화

1. 보편적 공식의 추상화: 대칭 모노이드 범주 $C$에서의 연산을 $K_{SList}$에서의 보편적 공식으로 추상화합니다.
2. 이중성 (Duality) 활용: 대칭 리스트의 벡터에 대한 이중성 (transpose) 연산을 정의하고, 이를 스펜의 전치 (transpose) 연산과 연결합니다.
3. 선형성 (Linearity) 과 다중집합: 대칭 리스트가 '선형 (linear, 중복 요소 없음)'일 때 사상이 유일함을 이용합니다. 이를 통해 스펜 범주에서 $K_{SList}$로 가는 유일한 의사함수 $\Lambda$를 구성할 수 있었습니다.
4. 최종 구성: $\Lambda: \text{Pith}(\text{Span}(\text{Fin})) \to K_{SList}^{op}$와 $C_K: K_{SList}^{op} \to \text{Cat}$의 합성으로 편향 제거된 대칭 모노이드 범주 $C^\otimes$를 정의합니다.

3. 주요 기여 및 결과 (Key Contributions & Results)

• Theorem 1.1 (주요 정리): 임의의 대칭 모노이드 범주 $\mathcal{C}$에 대해, 유한 집합의 스펜 (2,1)-범주의 pith 에서 Cat 으로 가는 의사함수 $C^\otimes$가 존재함을 증명했습니다.
  • 이 함수는 유한 집합 $J$를 $J$개의 객체의 곱 범주 $\mathcal{C}^J$로 보냅니다.
  • 스펜 $A \xleftarrow{f} B \xrightarrow{g} J$는 $g_! f^*$ (여기서 $f^*$는 전사, $g_!$는 텐서 곱에 의한 합) 로 매핑됩니다.
  • 이는 대칭 모노이드 범주가 Lawvere 대칭 모노이드 $(\infty, 1)$-범주의 ordinary-categorical 버전임을 보여줍니다.
• 형식화된 일관성 정리 (Theorem 1.3): 집합 $J$ 위의 자유 대칭 모노이드 범주가 $J$ 위의 유한 집합과 전단사 (bijections) 로 이루어진 범주 $\text{Core}(\text{Fin}/J)$와 동치임을 형식화했습니다. 이는 Piceghello 의 작업을 Lean 환경에 성공적으로 이식하고, 사상과 치환 (permutation) 사이의 일대일 대응을 완전히 증명했습니다.
• Lean/Mathlib 구현: 약 12.5k 줄의 코드로 이루어진 전체 형식화 작업을 수행했습니다. 이는 대칭 모노이드 범주의 편향 제거를 다룬 **첫 번째 기계화 증명 (mechanized proof)**입니다.
• 새로운 인프라 구축:
  • 스펜 이차 범주 (bicategory of spans) 의 형식화.
  • Pith-Beck-Chevalley 시스템 및 Kleisli 이차 범주에 대한 새로운 구조 정의.
  • 대칭 리스트의 사상과 치환군 사이의 정밀한 대응 관계 (Corollary 2.9).

4. 의의 및 향후 과제 (Significance & Future Work)

• 이론적 의의: 대칭 모노이드 범주의 편향 제거 과정을 엄밀하게 형식화함으로써, 고차 범주론 (higher category theory) 과 기존 범주론 사이의 간극을 메웠습니다. 이는 Lurie 의 $\infty$-operads 등과의 비교 정리를 증명하는 데 필수적인 기초를 제공합니다.
• 실용적 의의 (Mathlib):
  • 자유 가환 모노이드 객체: 대칭 모노이드 범주 내의 자유 가환 모노이드 객체 (예: 대칭 텐서 거듭제곱 $Sym^n(c)$) 를 정의하고 조작할 수 있는 기반을 마련했습니다.
  • 고차 연산: 임의의 유한 개수에 대한 텐서 곱 연산을 자연스럽게 다룰 수 있게 되어, 복잡한 대수적 구조의 형식화가 가능해집니다.
• 향후 작업:
  • 편향 제거된 구조를 이용한 구체적인 응용 (예: 대칭 텐서 거듭제곱, 내부 가환 모노이드 객체의 편향 제거) 형식화.
  • 구성된 함수 $\Lambda$가 국소적으로 동치 (local equivalence) 임을 증명하여, 편향 제거된 대칭 모노이드 범주와 Cranch 의 Lawvere 관점 사이의 완전한 동치를 확립.
  • Mathlib 에 이차 범주론 (bicategory theory) 의 핵심 인프라 (biequivalence, product 등) 를 추가하여 더 복잡한 고차 구조 형식화 지원.

요약

이 논문은 Lean 4 를 사용하여 대칭 모노이드 범주의 편향 제거 (unbiasing) 문제를 해결한 선구적인 작업입니다. Mac Lane 의 일관성 정리를 대칭 리스트 (symmetric lists) 와 코크터 군을 통해 정밀하게 형식화하고, 이를 스펜 범주와 Kleisli 이차 범주를 연결하는 의사함수 구성으로 이어냄으로써, 임의의 차수 (arbitrary arity) 에 대한 텐서 곱을 체계적으로 다룰 수 있는 프레임워크를 Mathlib 에 구축했습니다. 이는 추상 대수학의 고차 범주론적 일반화를 위한 필수적인 발걸음입니다.