Delooping presented groups in homotopy type theory

Champin, Mimram, Oleon 의 논문 "Delooping Presented Groups in Homotopy Type Theory"에 대한 상세한 기술적 요약입니다.

1. 문제 제기

호모토피 타입 이론 (HoTT) 에서 군 (group) 은 두 가지 방식으로 표현될 수 있습니다:

1. 외부적 (External): 공리를 만족하는 곱셈, 단위, 역원 연산을 갖춘 집합으로서.
2. 내부적 (Internal): 점화된 연결된 군집 (pointed connected groupoid) $A$의 루프 공간 ($\Omega A$)으로서. 타입 $A$는 군의 델루핑 (delooping) ($BG$) 이라고 불립니다.

어떤 군이든 델루핑이 존재한다는 것은 알려져 있지만, 임의의 군 $G$에 대한 표준적인 구성들은 종종 계산하거나 귀납적으로 추론하기 어려운 복잡한 타입을 초래합니다. 구체적으로:

• 토르소 (torsor) 구성 (G-집합 사용) 은 전체 군의 작용을 고려해야 하므로 방대한 타입을 요구합니다.
• 고차 귀납 타입 (HIT) 구성 (Eilenberg-MacLane 공간) 은 일반적으로 $G$의 각 원소에 대해 하나의 루프와 각 원소 쌍에 대해 하나의 경로 (곱셈 표) 를 필요로 하여, 방대한 수의 생성자 (constructors) 를 초래합니다.

저자들은 표현된 (presented) 군 (즉, 생성자와 관계식으로 정의된 군) 의 경우, 델루핑에 대한 더 단순하고 계산적으로 효율적인 구성을 개발하고자 합니다. 그들은 결과 타입의 크기를 전체 군 구조가 아닌 표현의 조합론적 복잡도에 맞추어 줄이려 합니다.

2. 방법론

이 논문은 HoTT 의 합성 기하학을 활용하며, 다음을 사용합니다:

• 고차 귀납 타입 (HITs): 점, 경로, 고차 경로를 가진 공간을 정의하기 위해.
• 절단 (Truncation): 군집 성질 (고차 호모토피 군의 절단) 을 강제하기 위해.
• 폴리그래프 (Polygraphs): 생성자와 관계를 체계적으로 관리하기 위해 HoTT 에 적응된 재작성 이론적 구조.
• 그로텐디크 쌍대성과 평탄화 보조정리 (Grothendieck Duality and Flattening Lemma): 섬유 열 (fiber sequences) 과 전체 공간 (total spaces) 을 연결하여 핵과 연결 성분을 계산할 수 있게 하기 위해.
• 형식화: 모든 결과는 cubical Agda 증명 보조기에서 형식화되었습니다.

3. 주요 기여 및 결과

A. 생성된 토르소를 통한 단순화된 델루핑 (3 절 및 4 절)

저자들은 고전적인 토르소 구성을 정교화합니다. 전체 군 $G$의 작용을 가진 모든 $G$-집합의 타입을 사용하는 대신, 생성 집합 $X$의 작용을 가진 $X$-집합을 도입합니다.

• 정리 15: $G$가 집합 $X$에 의해 생성되면, 주 $X$-집합 (주 $G$-토르소에서 유도됨) 의 연결 성분은 $G$의 델루핑입니다.
• 의의: 이 구성은 전체 군이 아닌 생성자들의 작용만 요구합니다.
  • 예시: 순환군 $\mathbb{Z}$의 경우, 표준적인 델루핑은 원 $S^1$입니다. 저자들은 엔드모피즘 타입 ($\Sigma (A:U). (A \to A)$) 에서 후속 함수 (successor function) 의 연결 성분이 $\mathbb{Z}$의 델루핑임을 보입니다. 이는 UniMath 과 같은 맥락에서 HIT 의 필요성을 피하고 추론을 단순화합니다.

B. 고차 귀납 타입을 통한 단순화된 델루핑 (5 절)

저자들은 $\langle X \mid R \rangle$로 표현된 군 $G$에 대한 새로운 HIT 구성을 제안합니다.

• **구성 ($BP$):** 군 원소당 하나의 루프 대신, 타입$BP$는 다음을 가집니다:
  • 한 점 $\star$.
  • 각 생성자 $x \in X$에 대한 하나의 루프 gen.
  • 각 관계식 $r \in R$에 대한 하나의 2-경로 rel.
  • 군집 절단 (groupoid truncation).
• 정리 24: $BP$는 표현된 군$[P]$의 델루핑입니다.
• 장점: 이는 모든 $|G|$개의 원소에 대한 루프를 요구하는 표준 $K(G, 1)$에 비해 생성자의 수를 획기적으로 줄입니다. 이는 타입 이론적 정의를 표준 조합론적 군론과 일치시켜, 전통적인 군론적 논증 (예: 티에츠 변환) 을 모방하는 귀납적 증명을 용이하게 합니다.

C. 2-폴리그래프와 내부적 추론 (6 절)

이러한 HIT 들의 조작을 형식화하기 위해, 저자들은 HoTT 내에서 2-폴리그래프를 도입합니다.

• 정의: 0-셀 (점), 1-셀 (생성자), 2-셀 (관계식) 로 구성된 구조.
• 표현된 타입: 그들은 2-폴리그래프에 의해 생성된 타입을 특정 HIT 로 정의합니다.
• 티에츠 변환: 그들은 표현된 타입을 보존하면서 폴리그래프를 수정 (생성자나 관계식의 추가/제거) 하는 연산 (T0, T1, T2) 을 정의합니다.
• 정리 29: 티에츠 동치인 2-폴리그래프는 동일한 타입을 표현합니다.
• 의의: 이는 HoTT 내에서 군 표현의 내부적 조작을 가능하게 하여, 근본적인 호모토피 타입을 변경하지 않고도 표현을 계산적으로 편리한 형태 (예: Knuth-Bendix 완성을 통한 수렴 표현) 로 변환할 수 있게 합니다.

D. 케일리 그래프와 복합체 (7 절)

저자들은 케일리 그래프와 복합체에 대한 새로운 호모토피적 해석을 제공합니다.

• 케일리 그래프를 핵으로: 그들은 표현에 의해 유도된 사상 $B\gamma^*: BX^* \to BG$의 핵이 케일리 그래프 $C(X, G)$임을 증명합니다 (정리 35).
  • $BX^*$는 생성자 위의 자유군의 델루핑입니다.
  • 섬유 열 $C(X, G) \to BX^* \to BG$는 군의 관계식을 인코딩합니다.
• 케일리 복합체: 그들은 이를 2 차원으로 확장하여, 2-스켈레톤 $B_2P$의 델루핑의 2-스켈레톤인 $B_2P$에서 $BG$로 가는 사상의 핵으로서 **케일리 복합체**$CP$를 정의합니다.
• 정리 40 및 43: 케일리 복합체는 타입 $B_2P$의 보편 피복 (universal covering) 입니다.
• 의의: 이는 고전적인 군론적 기하학적 객체 (케일리 그래프/복합체) 와 델루핑의 호모토피적 구조 사이의 직접적인 연결을 확립하여, 자유군과 표현된 군 사이의 "결함"을 측정합니다.

4. 의의 및 영향

• 계산적 효율성: 제안된 구성은 훨씬 적은 수의 생성자를 가진 타입을 산출하여, Agda 와 같은 증명 보조기에서의 계산과 자동화된 추론을 더 용이하게 합니다.
• 대수와 위상수학의 연결: 이 논문은 생성자, 관계식, 티에츠 변환, 케일리 그래프와 같은 고전적인 군론적 개념들을 HoTT 의 합성 언어로 성공적으로 번역하여, 전통적인 대수적 증명과 유사한 "내부적" 증명을 가능하게 합니다.
• 메타이론적 추론: 2-폴리그래프를 사용하여 저자들은 HIT 들의 구조 자체에 대해 추론할 수 있는 프레임워크를 제공하며, 호모토피 타입을 보존하는 변환을 가능하게 합니다.
• 미래 작업의 기초: 이 논문은 $n$-폴리그래프와 고차 케일리 복합체를 정의하기 위한 기초를 마련하며, 이는 HoTT 에서 군에 대한 자동화된 일관성 증명과 효율적인 코호몰로지 계산을 이끌 수 있습니다.

요약하자면, 이 작업은 군 표현의 특정 구조를 활용하여 타입의 정의와 이에 대한 추론을 모두 단순화하는, HoTT 에서 군 델루핑의 "작은" 그리고 "조합론적" 모델을 구성하기 위한 도구 세트를 제공합니다.