Dilatations of categories, via their lean formalization
2026-08-10 • Logic in Computer Science
Logic in Computer Science
AI summaryⓘ
The authors study a mathematical construction called 'dilatation' that changes a category by forcing certain arrows (morphisms) to factor through specified special arrows in a unique way. They fully formalize this construction and its main results using the Lean 4 proof assistant and the Mathlib library, ensuring that the whole theory is rigorously checked by computer. Their work also includes a detailed guide linking the mathematical ideas to the formal code.
category theorycategorymorphismsievedilatationfactorizationLean 4proof assistantformalizationMathlib
Authors
Arnaud Mayeux
Abstract
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.