Dilatations of categories, via their lean formalization

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.

Abstract: arXiv descriptive metadata (CC0). Thank you to arXiv for use of its open access interoperability. This service was not reviewed or approved by, nor does it necessarily express or reflect the policies or opinions of, arXiv.