The blow-up of a configuration has trivial direct image of the structure sheaf

Let $S$ be a surface, $p$ a configuration of $r$ points, $B$ an integral scheme and $\pi:B\to S$ a quasi-compact blow-up of the centre ideal. Then $\mathcal O_S\to\pi_*\mathcal O_B$ is an isomorphism.

Notation. IsBlowup I π says that $I$ pulls back to an invertible ideal along $\pi$ and that $\pi$ is universal with this property. A Surface is an integral scheme smooth of relative dimension 2 over $\operatorname{Spec}\mathbb C$ with a closed immersion into some complex projective space over $\mathbb C$. Configuration S r is the set of $r$-tuples of complex points with distinct images, with the Zariski topology induced from the product.

Formalization Note The statement is verbatim from OpenAI's Lean development, with Definitions files of this development imported in place of the upstream modules; these are supporting code for the statement.