Resolution of singularities by smooth and Hironaka-permissible blowups

### What is the conjecture

Let $k$ be a perfect field of characteristic $p > 0$ and let $X$ be an integral scheme, separated
and of finite type over $k$. Issue #5403 asks for *some* proper birational morphism onto $X$ from a
scheme smooth over $k$. One can ask for more: that the resolution be built out of blowups.

Call a closed subscheme $Z \subset X$ a *smooth center* if $Z$ is smooth over $k$ and contained in
the singular locus of $X$. Call it *Hironaka-permissible* if in addition $X$ is normally flat along
$Z$, that is, every graded piece $I^n / I^{n+1}$ of the conormal algebra of $Z$ in $X$ is a flat
$\mathcal{O}_Z$-module.

**Conjecture (smooth centers).** Every such $X$ admits a resolution of singularities $Y \to X$ that
is a finite composition of blowups, each in a center that is smooth over $k$ and contained in the
singular locus of the scheme being blown up.

**Conjecture (permissible centers).** The same, with every center Hironaka-permissible.

Both are open in positive characteristic, and they are genuinely different problems: normal
flatness is a real restriction on the center, not an automatic consequence of smoothness. Cossart
and Piltant record in Remark 1.4 that the morphism produced by their dimension three theorem is
*not* constructed as a composition of Hironaka-permissible blowing ups, and that the permissible
problem "remains widely open even in dimension three". So the dimension three resolution theorem
already formalised in `ResolutionOfSingularities.lean` settles neither statement.

In characteristic zero both are theorems. Włodarczyk, Theorem 8.1.1, produces a sequence of blowups
whose centers are smooth, are normally flat (part (c)), and by part (b) lie in $\mathrm{Sing}(Y_i)$
until $Y_i$ becomes smooth, after which the remaining centers only arrange the exceptional divisor.
Truncating the sequence at the first smooth stage gives both characteristic zero statements.

**Sources:**
- H. Hironaka, *Resolution of singularities of an algebraic variety over a field of characteristic
zero: I, II*, Ann. of Math. 79 (1964), 109-203 and 205-326,
https://doi.org/10.2307/1970486 and https://doi.org/10.2307/1970547
- J. Włodarczyk, *Singular implicit and inverse function theorems. Strong resolution with normally
flat centers*, https://arxiv.org/abs/1510.03480, Theorem 8.1.1(a)-(c)
- V. Cossart, O. Piltant, *Resolution of singularities of arithmetical threefolds*, J. Algebra 529
(2019), 268-535, https://doi.org/10.1016/j.jalgebra.2019.02.017, Theorem 1.1 and Remark 1.4
- H. Hauser, *On the problem of resolution of singularities in positive characteristic (or: a proof
we are still waiting for)*, Bull. Amer. Math. Soc. 47 (2010), 1-30,
https://doi.org/10.1090/S0273-0979-09-01274-9
- The Stacks Project, [tag 01WQ](https://stacks.math.columbia.edu/tag/01WQ) (effective Cartier
divisors), [tag 0806](https://stacks.math.columbia.edu/tag/0806) (universal property of blowing
up) and [tag 062Z](https://stacks.math.columbia.edu/tag/062Z) (the conormal algebra and the
normal cone)

### Prerequisites needed

Mathlib has neither blowups nor effective Cartier divisors, and no notion of normal flatness, so
these have to be supplied. They can be stated without constructing a blowup: characterise a blowup
by the universal property of [Stacks, tag 0806], as a morphism whose inverse-image ideal is
effective Cartier and which is terminal among such morphisms. Mathlib does provide
`AlgebraicGeometry.Scheme.IdealSheafData` with `comap`, `support` and `subschemeι`, and
`Scheme.Hom.smoothLocus`, which is enough to express the centers.

### [AMS categories](https://github.com/google-deepmind/formal-conjectures/labels?q=ams-)

* ams-14

### Choose either option

- [x] I plan on adding this conjecture to the repository
- [ ] This issue is up for grabs: I would like to see this conjecture added by somebody else

Start with ResolutionOfSingularities.lean and inspect AlgebraicGeometry.Scheme.IdealSheafData and Scheme.Hom.smoothLocus. Review the universal-property references at Stacks tags 0806, 01WQ, and 062Z, then determine how the smooth-center and Hironaka-permissible-center statements can be expressed. Done means the conjecture is added to the repository with the required notions supplied.

Written by the indexing model from the issue text.