Local uniformization

The question

Local uniformization in positive characteristic. Let $k$ be a field of characteristic $p>0$, let $F$ be a finitely generated field extension of $k$, and let $\mathcal{O}$ be a valuation ring of $F$ containing $k$. Then $\mathcal{O}$ admits local uniformization over $k$.

This is open from dimension four on: it is known when the transcendence degree of $F\mid k$ is at most three, see local_uniformization_of_trdeg_le_three.

Let $F$ be a finitely generated field extension of a field $k$ and let $\mathcal{O}$ be a valuation ring of $F$ containing $k$. Local uniformization asks for an affine model of $F\mid k$ on which the centre of $\mathcal{O}$ is a regular point: a finitely generated $k$-subalgebra $A\subseteq \mathcal{O}$ with fraction field $F$ such that $A_{\mathfrak{p}}$ is regular, where $\mathfrak{p}={\mathfrak{m}}_{\mathcal{O}}\cap A$ is the centre.

This is the local form of resolution of singularities, one valuation at a time. Zariski introduced it and proved it in characteristic zero, and deduced resolution of singularities in dimension at most three from it. In positive characteristic it is known in dimension at most three, and open from dimension four on. A place is Abhyankar when the rational rank of its value group and the transcendence degree of its residue field over $k$ add up to the transcendence degree of $F\mid k$; an Abhyankar place whose residue field is separable over $k$ is uniformized in any dimension [KK2005].

The form asked here is the weak one: some affine model of $F\mid k$ works. The proofs give the strong form, where the model may moreover be required to contain a prescribed finite subset of $\mathcal{O}$, and that is the form that patches into a resolution of singularities.

The conclusion here asks that the centre be a regular point, not a smooth one. Over a perfect field the two agree; over an imperfect field regularity is the right condition, since already $k(a^{1/p})\mid k$ for $a\in k\setminus k^p$ has no model that is smooth over $k$.

For a field extension, Algebra.EssFiniteType k F says that $F$ is finitely generated as a field over $k$, and Algebra.trdeg k F is the transcendence degree, the dimension of a model. The centre ValuationSubring.centerOn and the predicate ValuationSubring.HasLocalUniformization are defined in FormalConjecturesForMathlib.RingTheory.Valuation.LocalUniformization.

Formal statement (Lean 4)

From Formal Conjectures, module FormalConjectures.Wikipedia.LocalUniformization.

theorem local_uniformization (k F : Type*) [Field k] [Field F] [Algebra k F]
    [Algebra.EssFiniteType k F] (p : ℕ) [Fact p.Prime] [CharP k p] (𝒪 : ValuationSubring F)
    (hk : ∀ x : k, algebraMap k F x ∈ 𝒪) :
    𝒪.HasLocalUniformization k

What counts as progress

• A Lean proof of the pinned statement (or of its negation, for a yes/no question) — checked by the Lean kernel against the upstream statement; a curator confirms before the problem is marked resolved.
• Partial results: special cases, weaker bounds, reductions — as verified claims.
• Computations and numerical evidence with published code (reproducible).
• Literature: the problem may have been solved or partly solved already. Report it as a literature claim.
• A precise flaw in the formal statement (a misformalisation) — report it upstream too.

References

• Wikipedia
• [Zar1940] O. Zariski, [Local uniformization on algebraic varieties](https://doi.org/10.2307/1968864), Ann. of Math. 41 (1940), 852--896.
• [Abh1956] S. Abhyankar, [Local uniformization on algebraic surfaces over ground fields of characteristic $p\ne 0$](https://doi.org/10.2307/1970014), Ann. of Math. 63 (1956), 491--526.
• [Abh1966] 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$.
• [Cut2009] S. D. Cutkosky, [Resolution of singularities for 3-folds in positive characteristic](https://doi.org/10.1353/ajm.0.0036), Amer. J. Math. 131 (2009), 59--127; a simplification of [Abh1966], also over an algebraically closed field.
• [CP2008] V. Cossart and O. Piltant, [Resolution of singularities of threefolds in positive characteristic I](https://doi.org/10.1016/j.jalgebra.2008.03.032), J. Algebra 320 (2008), 1051--1082.
• [CP2009] V. Cossart and O. Piltant, [Resolution of singularities of threefolds in positive characteristic II](https://doi.org/10.1016/j.jalgebra.2008.11.030), J. Algebra 321 (2009), 1836--1976; quasi-projective threefolds over a field $k$ with $[k:k^p]<\infty$, in every positive characteristic.
• [CP2019] V. Cossart and O. Piltant, [Resolution of singularities of arithmetical threefolds](https://doi.org/10.1016/j.jalgebra.2019.02.017), J. Algebra 529 (2019), 268--535.
• [KK2005] H. Knaf and F.-V. Kuhlmann, [Abhyankar places admit local uniformization in any characteristic](https://doi.org/10.1016/j.ansens.2005.09.001), Ann. Sci. École Norm. Sup. 38 (2005), 833--846; the hypotheses are that the place is Abhyankar and that its residue field is separable over the ground field.
• [KK2009] H. Knaf and F.-V. Kuhlmann, [Every place admits local uniformization in a finite extension of the function field](https://doi.org/10.1016/j.aim.2008.12.009), Adv. Math. 221 (2009), 428--453.
• [Tem2013] M. Temkin, [Inseparable local uniformization](https://doi.org/10.1016/j.jalgebra.2012.09.023), J. Algebra 373 (2013), 65--119.

Source and licence

Imported from Formal Conjectures (Wikipedia), commit 2f91d251c07f. Statements and descriptions © The Formal Conjectures Authors, Apache License 2.0; reformatted for this page.