Papers With

← All papers
First page of Dilatations of categories, via their lean formalization

Dilatations of categories, via their lean formalization

Arnaud Mayeux

cs.LO Aug 10, 2026 · v1 math.CT
formalization mathlib category-theory
Read PDF arXiv abstract Code
TL;DR
Formalizes the theory of dilatations of categories, including the construction and its main theorems, in Lean 4 on top of Mathlib.
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.
Problem

Dilatations of categories generalize both localization and dilatations of rings via a center: a family of morphisms paired with sieves over their codomains. The theory had only informal published exposition.

Approach

The dilatation is built in Lean 4 as a quotient of a category generated from the localization quiver, reusing Mathlib's sieves and Gabriel–Zisman localization machinery rather than formalizing fraction sequences directly. Centers are encoded as a Lean structure with indexed families. A canonical functor and universal property are established, and comparison functors for restriction, sieve shrinking, and staged dilatations are derived by specializing the universal property. An appendix pairs each mathematical statement with its Lean declaration.

Results

A full formalization of the construction and its main theorems is provided, including corrections and clarifications produced during formalization, intended also as informal/formal training material for AI systems.