기술 요약: Lean에서의 추상 심플리셜 복합체 및 스텔라 세분화의 형식화

문제 정의

심플리셜 복합체(simplicial complexes) 이론은 대수적 및 조합론적 위상수학의 기초이며, 호몰로지(homology)와 속(genus)과 같은 불변량을 계산하고, 이산 모스 이론(discrete Morse theory) 및 붕괴 알고리즘(collapse algorithms)을 통해 호모토피 유형을 연구하기 위한 주요 도구 역할을 한다. 고전적인 정의들은 종종 유클리드 공간 내의 기하학적 임베딩(바리센트릭 좌표 및 아핀 독립성을 사용하는)에 의존하는데, 이러한 접근 방식은 부가적인 데이터를 도입하여 형식적 계산을 복잡하게 만든다.

저자들은 Lean 증명 보조기 생태계에서 발견되는 격차를 지적한다. 즉, mathlib에는 심플리셜 복합체와 관련된 다양한 형식화가 포함되어 있으나, 이들 간의 상호 연결이 부족하며, **스텔라 세분화(stellar subdivisions)**에 대한 기존의 형식화가 존재하지 않는다. 또한, 다른 증명 보조기(Rocq, ACL2)의 기존 형식화들은 알렉산더(Alexander)와 파크너(Pachner)의 다양체 삼각측량에 관한 구조적 정리와 같은 조합론적 토대를 제공하기보다는, 특정 계산 응용(예: 지속 호몰로지, 알렉산더 쌍대성)에 치중되어 있다. 본 논문은 심플리셜 세분화, 링크(link), 조인(join)과 관련된 항등식의 엄밀한 검증을 지원하면서도, 기존 라이브러리 내용과의 호환성과 계산 가능성을 유지하는 Lean 4 기반의 순수 조합론적 프레임워크의 필요성을 다룬다.

방법론

저자들은 **추상 심플리셜 복합체(Abstract Simplicial Complexes)**를 (어떠한 주변 기하 공간과도 독립적인) 부분집합 관계에 대해 닫혀 있는 유한 집합(면, faces)들의 집합으로 정의함으로써 순수 조합론적 프레임워크를 채택한다. 이 접근 방식은 mathlib의 SimplicialComplex 구조에서 발견되는 기하학적 조건(아핀 독립성, 볼록 껍질 교차 등)을 제거하여, 오버헤드를 줄이고 타입 시그니처를 단순화한다.

주요 방법론적 선택은 다음과 같다:

• 타입 캐스팅 및 코어션(Type-Casting and Coercions): 조인(join)과 같이 정점 타입을 변경하는 연산을 처리하기 위해, 저자들은 정점 집합에 대한 단사 사상(injective maps)을 나타내는 SimplicialCoe 구조를 정의한다. 이를 통해 주변 타입에 대한 전역적인 전단사 함수 없이도 "손실 없는" 재라벨링이 가능하다.
• 조인을 위한 이산 합집합(Disjoint Unions for Joins): 정점 집합이 서로 다르다는 가정을 하지 않고 두 복합체의 조인($K \star L$)을 정의하기 위해, 저자들은 면을 인덱싱하는 곱 타입 $E \times k$ ($k$는 비자명 반환, non-trivial semiring)를 활용하여 정점 집합의 서로소인 복사본들을 효과적으로 생성한다.
• 스텔라 세분화(Stellar Subdivisions): 면 $s$의 세분화 $\sigma_s K$는 $s$의 스타(star)의 내부를 제거하고, 이를 $s$의 경계($\partial s$), $s$의 링크($Lk(K, s)$), 그리고 새로운 바리센터 정점$x$의 조인으로 대체함으로써 조합론적으로 정의된다.
• 형식적 검증: 모든 정의와 정리는 Lean 4로 구현되었다. 저자들은 mathlib와의 향후 통합을 용이하게 하기 위해 계산 가능성을 우선시하고 가정을 최소화하였다.

주요 기여

본 논문은 모든 증명 보조기 중 최초로 스텔라 세분화를 형식화하였다. 구체적인 기여는 다음과 같다:

1. 추상 심플리셜 복합체의 형식화:

   • 핵심 구조인 AbstractSimplicialComplex의 정의와 이를 기하학적 SimplicialComplex 인스턴스로의 변환 및 역변환.
   • 모피즘(SimplicialMap), 동형 사상(SimplicialIso), 그리고 코어션(SimplicialCoe)의 형식화.
   • 합집합, 교집합, 부분 복합체(subcomplexes), 차원 계산 등의 표준 연산 구현.

2. 부분 복합체 및 연산의 형식화:

   • 링크($Lk(K, s)$), **면의 경계**($\partial s$), **스타**($St(K, s)$), 스타 컴플리먼트(star complements), 콘(cones), 그리고 조인($K \star L$)에 대한 엄밀한 정의 및 성질 증명.
   • 조인에 대한 분배 법칙, 결합 법칙, 교환 법칙(동형/코어션 관점에서의) 증명.
   • 이러한 연산들이 동형 사상 및 코어션과 어떻게 상호작용하는지를 보여주는 항등식 확립.

3. 스텔라 세분화의 형식화:

   • 스텔라 세분화 $\sigma_s K$와 스텔라 용접(stellar weld)(역 연산)의 정의.
   • 스텔라 동치($K \cong_{st} L$)를 스텔라 이동(stellar moves)의 추이적 폐쇄(transitive closure)로 정의.
   • 스텔라 동치가 단사 타입 캐스팅 하에서도 보존됨을 입증하여(정리 3.2), 해당 동치 관계가 정점 라벨링의 변화에 견고함을 보장함.

4. 새로운 정리 및 항등식:

   • 스텔라 세분화와 링크 사이의 상호작용을 설명하는 항등식 도출. 특히, 정리 3.9는 세분화된 면의 링크에 있는 면 $t$에 대하여, 세분된 복합체 내 $t$의 링크가 원래 링크의 스텔라 세분화임을 입립한다: $Lk(\sigma_s K, t) = \sigma_{s \setminus t}(Lk(K, t))$.
   • 저자들은 링크와 세분화의 "반교환성(anticommutativity)"에 관한 이 특정 항등식을 포함한 여러 결과들이 표준 문헌에는 참조가 없으며, 형식화 과정 중에 도출되었음을 언급한다.

결과

본 형식화는 삼각측단 다양체 연구에서 흔히 사용되는 일련의 항등식들을 성공적으로 검증하였다:

• 링크 보존: 면 $t$가 세분된 스타 외부에 있는 경우, 그 링크는 변하지 않는다 ($Lk(\sigma_s K, t) = Lk(K, t)$).
• 조인 호환성: 스텔라 세분화는 특정 방식으로 조인에 대해 분배된다, 예: $(\sigma_s K) \star L = \sigma_{s \sqcup \emptyset}(K \star L)$.
• 동치 보존: 스텔라 동치는 심플리셜 동형 사상 및 단사 타입 캐스팅 하에서 보존된다(대상 타입이 새로운 바리센터 라벨을 위한 충분한 "공간"을 가진 경우).
• 코드 규모: 현재 프로젝트는 정의, 유틸리티 렘마, 증명을 포함하여 약 14,000 라인의 Lean 코드로 구성되어 있다.

의의 및 주장

저자들은 본 연구를 알렉산더(Alexander) 및 파크너(Pachner)의 정리를 형식화하기 위한 기초적인 단계로 위치시킨다. 이 정리들은 다양체의 삼각측량들이 서로 동형일 필요충분조건이 일련의 스텔라(또는 비스텔라) 이동에 의해 관련되어 있다는 것을 기술한다.

• 최초의 사례: 본 논문은 모든 증명 보조기 중 스텔라 세분화를 형식화한 최초의 사례임을 주장한다.
• 이론과 계산의 가교: 조합론적 프레임워크를 채택함으로써, 본 연구는 심플리셜 복합체 이론을 계산적 기법 및 알고리즘 응용(예: 위상적 데이터 분석 및 Regina와 같은 소프트웨어)에 더 적합하게 만드는 것을 목표로 한다.
• 민속적 지식(Folklore)의 목록화: 저자들은 많은 조합론적 위상수학의 기술적 항등식들이 증명의 번거로움 때문에 "민속적 지식" 상태로 남아 있다고 주장한다. 이 형식화는 이러한 결과들을 목록화하고 검증하여 논리적 공백을 메우는 역할을 한다.
• 제한된 범위: 저자들은 이것이 "초기 작업"임을 명시한다. 파크너의 정리를 아직 형식화했다고 주장하는 것이 아니라, 이를 수행하는 데 필요한 필수 인프라(세분화, 링크, 조인 및 동치 관계)를 제공했다는 것이다. 또한, 조합론적 측면을 분리해냈으나, 이를 mathlib의 기하학적 SimplicialComplex 정의와 완전히 통합하고 모든 싱글톤이 면인 전체 복합체(total complexes)의 복잡성을 다루기 위해서는 향후 작업이 필요함을 인정한다.

이 연구는 계산 가능성과 mathlib와의 호환성을 우선시하는 설계 철학을 강조하며, Lean 생태계 내에서 향후 조합론적 위상수학의 발전을 위한 유선형의 기초를 구축하는 것을 목표로 한다.