Formalizing multi-graded Brenner-Schröer Proj schemes and dilatations of rings in Lean4

기술 요약: Lean4에서의 다중 등급 Brenner-Schröer Proj 스킴 및 환의 딜라테이션(Dilatations) 형식화

문제 정의
본 논문은 Lean4 정리 증명기 내에서 다중 등급 대수 기하학의 고급 구조들을 형식화하는 문제를 다룬다. 고전적인 대수 기하학은 대개 자연수($\mathbb{N}$) 또는 정수($\mathbb{Z}$)로 등급이 매겨진 환에 의존하지만, 현대의 발전된 이론들—예를 들어 리 이론(Lie theory), 기하적 표현론, 그리고 최소 모델 프로그램 등—은 더 일반적인 모노이드 또는 군으로 등급이 매겨진 환을 요구한다. 특히 저자들은 Brenner–Schröer Proj 구성을 다루며, 이는 고전적인 Proj 구성을 다중 등급 환경으로 일반화한 것이다. 또한, 국소화(localization) 및 블로우업(blowup)과 관련된 연산인 환의 딜라테이션(dilatation) 이론을 다룬다. 과제는 타입 이론적 프레임워크(Lean4) 내에서 등급이 매겨진 환 $A$와 그 직합 분해 $\bigoplus_{i \in \iota} A_i$ 사이의 구분을 엄격하게 관리하면서도, 공학적 사용성을 해치지 않는 방식으로 이러한 구조들을 구현하는 것이다.

방법론
저자들은 이러한 개념들을 Lean4에서 형식화하기 위해 기존 문헌(특히 [9]의 처리를 따름)과 일치하는 대수적 접근 방식을 채택한다. 방법론은 다음과 같다:

1. 등급 구조를 위한 일반적 설정: 형식화 과정은 등급 모노이드 $\iota$가 임의의 아벨 군인 등급 환 및 모듈을 정의한다. 타입 이론적 제약을 처리하기 위해, 저자들은 환 $A$와 그 등급 성분 $A_i$를 구분하며, 환과 그 직합 분해 사이를 전환할 수 있는 능력을 유지하면서 성분들을 부분군으로 취급하기 위해 SetLike 구조를 활용한다.
2. 동차 국소화와 "포션(Potions)": 핵심적인 기술적 혁신은 동차 국소화 $A(S)$의 차수가 0인 부분으로 정의되는 "포션"($\vartheta(S)$)의 정의이다. 표준적인 국소화와 달리, 포션은 국소화된 환의 부분환으로 정의되지 않고, 동일한 차수를 가진 동차 원소 $a, b$ ($b \in S$)에 대한 트리플 $(i, a, b)$의 몫(quotient)으로 정의된다. 이 구조는 귀납법을 용이하게 하고 분자와 분모에 접근하는 것을 돕는다.
3. 관련성 및 양질의 포션 성분: 저자들은 "관련된(relevant)" 동차 부모노이드의 개념을 형식화하는데, 여기서 부모노이드 내 원소들의 차수에 의해 생성된 부분군이 등급 군 내에서 유한 지수(또는 토션 몫)를 갖는 것을 의미한다. 저자들은 "양질의 포션 성분(good potion ingredients)"을 관련되어 있으면서 동시에 유한 생성되는 부모노이드로 정의한다.
4. 글루잉(Gluing) 및 Proj 구성: Proj 스킴은 양질의 포션 성분들의 가족과 연관된 아핀 스킴 $\text{Spec}(\vartheta(S_i))$들을 글루잉하여 구성된다. 글루잉 데이터는 포션 텐서 곱 사이의 동형 관계(예: $\vartheta(ST) \otimes_{\vartheta(S)} \vartheta(SR) \cong \vartheta(RST)$)에 의존하며, 이는 "포션 생성자(potion generators)"를 통해 확립된다.
5. 딜라테이션(Dilatations): 본 논문은 멀티센터(여러 아이디얼과 원소들의 집합)에 대한 환의 딜라테이션을 형식화한다. 이는 기호적 분수 $m/a^\nu$의 동치류를 정의하는 것을 포함하며, 딜라테이션을 특징짓는 보편 성질(universal property)을 증명하는 과정을 포함한다.

주요 기여 및 결과
본 논문은 Lean4 내의 정의, 보조 정리, 그리고 정리들의 포괄적인 라이브러리를 제시한다:

• 다중 등급 Proj의 형식화: 저자들은 Brenner–Schröer Proj 구성을 완전히 구현하였다. 여기에는 동차 국소화의 정의, 포션의 이론, 그리고 Proj 스킴을 형성하기 위한 아핀 스킴의 글루잉이 포함된다.
• 포션 생성자 및 동형 관계: 중요한 기여 중 하나는 "포션 생성자"의 형식화이며, 이를 통해 관련된 $S$와 유한 생성된 $T$에 대하여 사상 $\text{Spec}(\vartheta(ST)) \to \text{Spec}(\vartheta(S))$가 열린 침투(open immersion)임을 증명할 수 있다. 또한 글루잉 구성을 위해 필요한 코사이클 조건(cocycle conditions)을 확립한다.
• 함자성(Functoriality): Proj 구성이 등급 환의 범주에서 스킴의 범주로 가는 반변 함자(contravariant functor)임을 보여준다. 저자들은 대상 가족의 이미지가 타겟 가족와 정의적으로 동일하지 않은 타입 이론적 미묘함을 다루기 위해, 함자성을 확립하고자 특정 사상(projHomOfLE)을 사용하는 과정을 주의 깊게 다루었다.
• 딜라테이션: 본 논문은 환 딜라테이션의 정의를 형식화하고 그 보편 성질을 증명한다: 중심 원소들의 이미지가 영인자가 아니고 대응하는 아이디얼들의 이미지를 생성하는 임의의 환 준동형 사상 $\chi: A \to B$에 대하여, 딜라테이션으로부터 $B$로의 유일한 사상이 존재한다.
• 확장된 가족의 동형성: 기존 성분의 곱을 포함함으로써 양질의 포션 성분 가족을 확장하는 것이 동형인 Proj 스킴을 결과로 가져온다는 것을 증명하며, 이를 통해 생성 가족의 선택에 대한 구성의 견고성을 보장한다.

의의
본 논문은 주로 고급 대수 기하학의 형식화를 위한 기초적인 단계로서의 중요성을 주장한다. 이는 다음의 역할을 수행한다:

1. 문서화: 형식화의 근간이 되는 정의, 설계 선택, 주요 결과들에 대한 상세한 기록으로서, 향후 개발자들을 안내하기 위한 것이다.
2. 토대: 다중 등급 구조나 딜라테이션을 필요로 하는 프로젝트를 포함하여, 향후 확장될 수 있는 형식화된 대수 기하학을 위한 재사용 가능한 라이브러리이다.
3. 검증: Brenner–Schröer 구성과 딜라테이션 이론의 정확성을 증명기 내에서 검증함으로써, 문헌의 대수적 정의를 엄격하게 준수하고 있음을 보여주는 완전한 형식적 구현이다.

저자들은 고급 기하적 구조의 형성화를 지원하기 위해 해당 코드가 공개적으로 사용 가능하다는 점을 명시하였다. 저자들은 대수 기하학의 미해결 난제를 해결했다고 주장하는 것이 아니라, 기존의 복잡한 이론들을 기계가 확인 가능한 형식으로 성공적으로 변환했음을 밝히고 있다.