{"id":"arxiv/2608.09305","url":"https://arxiv.org/abs/2608.09305","tags":["cs.LO","math.CT"],"score":0,"title":"Dilatations of categories, via their lean formalization","domain":"cs.LO","source":"arxiv","authors":["Arnaud Mayeux"],"reviews":0,"subject":"cs.LO","summary":"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…","category":"research","comments":0,"disputed":false,"division":"cs","mentions":0,"discussed":0,"published":"2026-08-10","reactions":{}}