Formalising the Bruhat-Tits Tree

1. 문제 제기 (Problem)

• 수학적 배경: 브루하트-티트 트리는 $p$-진수 체 $Q_p$나 더 일반적인 이산 값매김 체 (discrete valuation field) $K$ 위에서 정의되는 조합론적 객체로, $GL_2(K)$의 부분군 구조, 호몰로지, 그리고 표현론 (representation theory) 을 연구하는 데 필수적인 도구입니다. 특히, Ihara 의 정리 (torsion-free 부분군은 자유군임) 증명이나 드린펠드 상반평면 (Drinfeld's upper half plane) 과의 연결 고리 등에서 핵심적인 역할을 합니다.
• 형식화의 필요성: 수학 연구는 점차 복잡해지고 있으며, 오류가 없는 증명과 명확한 문서화가 요구됩니다. 저자들은 형식화 도구가 이러한 연구 과정을 지원하고 문서화를 개선할 수 있다는 점에 주목했습니다.
• 현재의 공백: 브루하트-티트 트리는 증명 보조기 (proof assistant) 에서 한 번도 형식화된 바가 없었습니다. 또한, 이 트리를 구성하는 데 필요한 카탄 분해 (Cartan decomposition) 역시 $GL_n(K)$에 대해 체계적으로 형식화되지 않은 상태였습니다.

2. 방법론 (Methodology)

이 프로젝트는 Lean 4와 그 방대한 수학 라이브러리인 mathlib4를 기반으로 진행되었습니다.

• 일반화된 설정: 구체적인 $Q_p$ 대신 임의의 이산 값매김 환 (discrete valuation ring) $R$과 그 분수체 $K$를 사용하여 더 일반적인 맥락에서 형식화를 수행했습니다. 완비성 (completeness) 은 트리의 구성 자체에는 필요하지 않으므로 가정하지 않았습니다.
• 카탄 분해 (Cartan Decomposition) 형식화:
  • $GL_n(K)$를 $GL_n(R)$의 이중 잉여류 (double cosets) 로 분해하는 정리를 증명했습니다.
  • 가우스 소거법 (Gaussian elimination) 유사 알고리즘을 사용하여 행렬을 대각화하는 과정을 형식화했습니다.
  • 행렬의 원소들을 값매김 (valuation) 을 기준으로 정렬하고, 행과 열을 교환하여 표준형으로 만드는 과정을 Lean 코드로 구현했습니다.
• 브루하트-티트 트리의 구성:
  • 정점 (Vertices): $K^2$ 내의 $R$-격자 (lattices) 를 동위 (homothety, 스칼라 배) 관계로 동치류로 분류하여 정의했습니다.
  • 거리 함수 (Distance): 두 격자 사이의 거리를 정의하기 위해, 두 격자의 기저를 관련짓는 정리 (Proposition 3.1) 를 카탄 분해를 통해 증명했습니다. 이를 통해 두 격자 $L, L'$ 사이의 거리를 $n-m$ (여기서 $\varpi^n e, \varpi^m f$가 기저가 됨) 으로 정의했습니다.
  • 그래프 구조: 거리가 1 인 정점들을 이웃으로 정의하여 단순 그래프를 구성하고, 이것이 실제로 트리 (연결되고 순환이 없음) 임을 증명했습니다.
• 격자의 관점 (Perspectives on Lattices): Lean 에서 격자를 표현할 때 발생하는 타입 문제 (격자 $M$의 원소와 $K^2$의 원소 간의 타입 불일치) 를 해결하기 위해 세 가지 관점을 비교하고, 기저 (basis) 를 사용하여 격자를 정의하는 관점을 채택하여 타입 변환 (casting) 없이 등식 유도 원칙을 사용할 수 있도록 최적화했습니다.
• 조화 코체인 (Harmonic Cohains) 검증:
  • 트리의 에지에 정의된 함수 (코체인) 에 대한 라플라시안 (Laplacian) 연산자를 정의하고, 이 연산자가 전사 (surjective) 임을 증명했습니다.
  • 이 과정에서 $SL_2(K)$의 작용이 정점의 짝수/홀수 패리티를 보존함을 이용했습니다.

3. 주요 기여 (Key Contributions)

1. 최초의 형식화: 브루하트-티트 트리와 관련된 이론을 증명 보조기에서 최초로 완전히 형식화했습니다. 약 8,000 줄의 Lean 코드가 작성되었으며, 이는 Graph, Lattice, Cartan 등 5 개의 폴더로 구조화되어 있습니다.
2. 카탄 분해의 형식화: $GL_n(K)$에 대한 카탄 분해 정리를 증명하고, 이를 mathlib 에 통합할 수 있는 수준의 API 로 개발했습니다. 이는 $p$-진수 표현론 연구에 중요한 기반이 됩니다.
3. 격자 이론의 확장: mathlib 에 격자 (lattice) 의 정의와 관련 정리들을 추가하여, 추후 다른 수론 연구에서 재사용할 수 있는 기반을 마련했습니다.
4. 조화 코체인에 대한 전사성 증명: 라플라시안 연산자의 전사성에 대한 직접적이고 초등적인 증명을 형식화했습니다. 이는 연구 중인 "리만 분석적 theta 코사이클 (rigid analytic theta cocycles)"의 구조를 이해하는 데 필수적인 단계였습니다.
5. 일반화 (Generalization): 형식화 과정에서 연구자들은 초기 가정을 $Z$에서 임의의 가환환 $A$와 $A$-모듈 $M$으로 일반화할 수 있음을 발견했습니다. Lean 의 유연성 덕분에 코드 수정이 용이했고, 이는 수학적 통찰로 이어졌습니다.

4. 결과 (Results)

• 정리 검증: 형식화된 코드를 통해 브루하트-티트 트리가 실제로 트리 (acyclic and connected) 임을 기계적으로 검증했습니다.
• 조화 코체인 정밀 검증: 저자 중 한 명이 진행 중인 연구 (Gebhard Böckle 및 O˘guz Gezmi¸s 와의 공동 작업) 의 핵심인 짧은 완전열 (short exact sequence) $0 \to \text{Har}(T, \mathbb{Z}) \to \text{Maps}(E(T), \mathbb{Z}) \xrightarrow{\Delta} \text{Maps}(V(T), \mathbb{Z}) \to 0$의 전사성 부분을 형식적으로 검증했습니다.
• 코드 효율성: 조화 코체인 전사성 증명 부분에서는 LaTeX 문서 140 줄에 대해 Lean 코드가 750 줄 미만으로, 다른 프로젝트에 비해 매우 높은 효율성을 보였습니다. 이는 Lean 이 복잡한 수학적 증명을 명확하게 표현하는 데 적합함을 시사합니다.

5. 의의 및 향후 전망 (Significance)

• 수론 연구의 새로운 패러다임: 이 프로젝트는 고등 수학 (대학원 수준) 의 복잡한 개념을 형식화하여 연구의 정확성을 높이고, 오류를 방지하는 새로운 가능성을 보여주었습니다.
• mathlib 통합: 작성된 코드는 mathlib4 에 통합될 예정이며, 이는 향후 $p$-진수 표현론, 대수적 수론, 그리고 드린펠드 상반평면과 관련된 연구들을 위한 표준적인 형식화 기반을 제공할 것입니다.
• 연구 도구로서의 Lean: 저자들은 형식화 과정에서 수학적 가정을 일반화하고 새로운 통찰을 얻는 경험을 했습니다. 이는 형식화 도구가 단순히 증명을 검증하는 것을 넘어, 수학적 발견을 촉진하는 도구로 활용될 수 있음을 보여줍니다.
• 한계와 과제: 현재 형식화는 격자 이론과 카탄 분해에 집중되어 있으며, 드린펠드 상반평면이나 리만 분석적 기하학 (rigid analytic geometry) 과 같은 더 깊은 이론은 아직 형식화되지 않았습니다. 향후 Shapiro 보조정리 등 군 코호몰로지 관련 이론의 형식화가 필요하면, 이 프로젝트의 결과물이 더 복잡한 연구 (예: $H^1(\Gamma, \dots)$ 구조 분석) 를 검증하는 데 활용될 수 있습니다.

결론적으로, 이 논문은 추상적인 대수적 수론 개념을 Lean 을 통해 구체화하고 검증한 성공적인 사례로, 형식적 수학 (formal mathematics) 이 현대 수학 연구의 핵심 도구로 자리 잡을 수 있음을 입증했습니다.