AI 中文总结
本文在Lean 4证明助手的Mathlib库上形式化范畴扩张的构造及主要定理，建立数学命题与Lean声明的对应表，为范畴扩张理论提供形式化基础。
AI 中文摘要
给定范畴$\boldsymbol{\textit{C}}$和一个中心，即由态射$d_i$及其上余域上的筛$N_i$组成的对集合，$\boldsymbol{\textit{C}}$的扩张是新范畴$\boldsymbol{\textit{C}}'$，其中每个$n \in N_i$均可通过$d_i$唯一且函子地分解。本文在Lean 4证明助手的Mathlib库基础上，通过完整构造及主要定理的形式化，提出范畴扩张理论，附录整理了数学命题与形式化它们的Lean声明之间的系统对照表。
英文摘要
Given a category $\calC$ and a center, that is a collection of pairs $(d_i, N_i)$ consisting of a morphism $d_i$ and a sieve $N_i$ over its codomain, the dilatation of $\calC$ is a new category $\calC'$ in which every $n \in N_i$ factors, uniquely and functorially, through $d_i$. This paper presents the theory of dilatations of categories through a full formalization of the construction and its main theorems in the Lean~4 proof assistant, on top of the Mathlib library. An appendix collects a systematic dictionary between the mathematical statements and the Lean declarations that formalize them.
