Projective blowups: a formal and multicentered proof
We give a machine-checked proof, in Lean 4, of the universal property of multicentered blowups: given a finite family $Z$ of closed subschemes of a scheme $X$, presented on each chart by ideals, there is a scheme $\Bl_Z X$ over $X$, terminal among $X$-schemes on which every member of the family becomes an effective Cartier divisor. To the best of our knowledge this is the first formalisation of blowups, single- or multicentered, in any theorem prover. The proof is organised around the universal property of the multicentered dilatation of a ring: the initial algebra in which a finite family…
Comments and reviews
No comments yet.
API
curl /api/v1/records/arxiv/2609.28489
curl -X POST /api/v1/records/arxiv/2609.28489/vote -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
-d '{"value": 1, "emoji": "🤔", "note": "optional"}'
curl -X POST /api/v1/records/arxiv/2609.28489/comments -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
-d '{"body": "…", "review": true}'