Local uniformization

### What is the conjecture

Let $k$ be a field, let $F$ be a finitely generated field extension of $k$, and let
$\mathcal{O}$ be a valuation ring of $F$ containing $k$ (a *place of $F \mid k$*). Then
$\mathcal{O}$ *admits local uniformization over $k$* if some affine model of $F \mid k$ inside
$\mathcal{O}$ is regular at the centre of $\mathcal{O}$: there is a finitely generated
$k$-subalgebra $A \subseteq \mathcal{O}$ with fraction field $F$ such that $A_\mathfrak{p}$ is a
regular local ring, where $\mathfrak{p} = \mathfrak{m}_\mathcal{O} \cap A$ is the centre.

**Conjecture.** If $k$ has characteristic $p > 0$, then every place of $F \mid k$ admits local
uniformization over $k$.

This is the local form of resolution of singularities, one valuation at a time. Zariski
introduced it, proved it in characteristic zero, and deduced resolution of singularities in
dimension at most three from it. In positive characteristic it is known when the transcendence
degree of $F \mid k$ is at most three, and is open from transcendence degree four on.

Two solved variants are worth stating alongside the conjecture. Knaf and Kuhlmann proved that
every place of an algebraic function field admits local uniformization after a *finite extension*
of the function field, in any characteristic. Temkin proved that the extension can be taken purely
inseparable, at the cost of also extending the ground field purely inseparably.

Asking that the centre be a regular point rather than a smooth one is what makes the statement
right over an imperfect ground field. Over a perfect field the two agree. This is the same issue
as in #5403, where perfectness of $k$ has to be assumed because the conclusion there is
smoothness.

**Sources:**
- https://en.wikipedia.org/wiki/Local_uniformization_theorem
- O. Zariski, *Local uniformization on algebraic varieties*, Ann. of Math. 41 (1940), 852-896,
https://doi.org/10.2307/1968864. The characteristic zero theorem.
- S. Abhyankar, *Local uniformization on algebraic surfaces over ground fields of characteristic
$p \neq 0$*, Ann. of Math. 63 (1956), 491-526, https://doi.org/10.2307/1970014.
- S. Abhyankar, *Resolution of singularities of embedded algebraic surfaces*, Monographs in Pure
and Applied Mathematics 24, Academic Press, 1966. Birational resolution of threefolds over an
algebraically closed field of characteristic $p > 5$.
- S. D. Cutkosky, *Resolution of singularities for 3-folds in positive characteristic*, Amer. J.
Math. 131 (2009), 59-127, https://doi.org/10.1353/ajm.0.0036. A simplification of Abhyankar's
threefold proof, also over an algebraically closed field.
- V. Cossart, O. Piltant, *Resolution of singularities of threefolds in positive characteristic
I*, J. Algebra 320 (2008), 1051-1082, https://doi.org/10.1016/j.jalgebra.2008.03.032, and
*II*, J. Algebra 321 (2009), 1836-1976, https://doi.org/10.1016/j.jalgebra.2008.11.030.
Quasi-projective threefolds over a field $k$ with $[k : k^p] < \infty$, in every positive
characteristic; this is where characteristics 2, 3 and 5 come from.
- 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 resolves every
reduced separated Noetherian quasi-excellent scheme of dimension at most three, in any
characteristic, with an everywhere regular source. This is what gives the transcendence degree
at most three case over an arbitrary ground field: take the centre of $\mathcal{O}$ on a
resolution of a proper model of $F \mid k$.
- H. Knaf, F.-V. Kuhlmann, *Abhyankar places admit local uniformization in any characteristic*,
Ann. Sci. École Norm. Sup. 38 (2005), 833-846, https://doi.org/10.1016/j.ansens.2005.09.001.
- H. Knaf, F.-V. Kuhlmann, *Every place admits local uniformization in a finite extension of the
function field*, Adv. Math. 221 (2009), 428-453, https://doi.org/10.1016/j.aim.2008.12.009.
- M. Temkin, *Inseparable local uniformization*, J. Algebra 373 (2013), 65-119,
https://doi.org/10.1016/j.jalgebra.2012.09.023.

### Prerequisites needed

None. Mathlib has `ValuationSubring`, `IsRegularLocalRing`, `IsRegularRing`, `Localization.AtPrime`,
`Algebra.EssFiniteType` (which for a field extension says exactly that it is finitely generated
as a field) and `Algebra.trdeg`, which is everything the statements need.

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

* ams-12
* ams-13
* 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 by reviewing the stated Mathlib prerequisites: ValuationSubring, IsRegularLocalRing, IsRegularRing, Localization.AtPrime, Algebra.EssFiniteType, and Algebra.trdeg. Formalize the local uniformization conjecture and ensure the resulting Lean statements compile; no repository file or test entry point is identified in the issue.

Written by the indexing model from the issue text.