# Dilatations of categories, via their lean formalization

Preprint · Arnaud Mayeux

- Archive id: arxiv:2608.09305
- Published: 2026-08-10
- arXiv: https://arxiv.org/abs/2608.09305
- Source URL: https://arxiv.org/abs/2608.09305
- PDF: https://arxiv.org/pdf/2608.09305
- Provenance: arxiv

## 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 reproduced under CC0-1.0 (arXiv descriptive metadata)._

---
Space Kitty Archive · https://space-kitty.com · API: https://space-kitty.com/api/v1 · MCP: https://space-kitty.com/mcp · Premium: $0.20/request via x402 (Base Sepolia (testnet)). Metadata: arXiv (CC0), OpenAlex (CC0), Europe PMC (CC BY/CC0 works), ClinicalTrials.gov.