LocalUniformization.lean`

Explanation legend Lean4 Domain Explanation Language (L4DEL)

L4DEL explanations are a separate layer. They do not change the Lean source. Intuition is explanatory prose; numbered items are a reading path; sources link the wording back to evidence.

L4DEL: Lean4 Domain Explanation Language

Annotation provenance. This overlay contains 10 curated AI-written annotations and 7190 mechanical source-derived annotations. They have not been human-reviewed as explanations; treat them as unverified and not mathematical authority. Retained generation history: The 71 original curated annotations were produced in a Claude Sonnet 5.5 session at medium effort; Claude Opus 5.5 is recorded in that session as the advisor model, not the direct author. The bulk source-derived expansion was generated mechanically from pinned source comments by tooling developed in a GPT-5.6 Sol session at ultra reasoning; GPT-5.6 Sol did not originate the quoted source prose. On 2026-10-17 the mechanically generated source-comment annotations of the Formal Conjectures, Carleson, FLT, PFR, CompFiles, Mathematics in Lean and Theorem Proving in Lean overlays were regenerated by the same generator after three corrections made in a Claude Sonnet 5.5 session: titles no longer cut a sentence inside mathematics or end on a dangling word, workflow markers are removed from the quoted prose, and declaration names follow the scanner's namespace resolution. The boilerplate step line was dropped, and comments that were only a row of dashes no longer yield annotations. No new prose was written and no human review is claimed.

Credit: The upstream authors and contributors retain credit for the project and mathematics. lean4-explainer only renders their pinned source and adds the separately disclosed explanation layer.

Project sources: Pinned project documentation, Formal Conjectures paper, arXiv v1

5 declarations, 4 contain sorry, 0 declared as axioms

Local uniformization

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.

References:

Wikipedia
[Zar1940] O. Zariski, Local uniformization on algebraic varieties, Ann. of Math. 41 (1940), 852--896.
[Abh1956] S. Abhyankar, Local uniformization on algebraic surfaces over ground fields of characteristic $p \neq 0$, 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, 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, J. Algebra 320 (2008), 1051--1082.
[CP2009] V. Cossart and O. Piltant, Resolution of singularities of threefolds in positive characteristic II, 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, J. Algebra 529 (2019), 268--535.
[KK2005] H. Knaf and F.-V. Kuhlmann, Abhyankar places admit local uniformization in any characteristic, 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, Adv. Math. 221 (2009), 428--453.
[Tem2013] M. Temkin, Inseparable local uniformization, J. Algebra 373 (2013), 65--119.

Imports (1)

FormalConjecturesUtil

theorem LocalUniformization.hasLocalUniformization_top The trivial valuation subring of a function field is uniformized by any affine model, since its centre is the generic point line 93 source
Source documentation
The trivial valuation subring of a function field is uniformized by any affine model, since its centre is the generic point.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, Algebra, Subalgebra, Algebra.FiniteType, Subtype, Membership.mem, IsFractionRing, ValuationSubring.HasLocalUniformization, Top.top, ValuationSubring
Proof uses: ValuationSubring.mem_top, Exists.intro, Exists, And, IsRegularLocalRing, Localization.AtPrime, ValuationSubring.centerOn, Ideal.primeCompl, And.intro, Eq, Ideal, Bot.bot, Eq.mpr, Ideal.comap, RingHom, RingHom.codRestrict, AlgHom.toRingHom, Subalgebra.val, IsLocalRing.maximalIdeal, id and 21 more
78 instances, coercions and auxiliary constants left out.

Tactic trace: 14 steps
Open to load the checked before-and-after goal states.
```
theorem hasLocalUniformization_top {F : Type*} [Field F] {k : Type*} [Field k] [Algebra k F]
    (A : Subalgebra k F) [Algebra.FiniteType k A] [IsFractionRing A F] :
    (⊤ : ValuationSubring F).HasLocalUniformization k := by
…
```
theorem LocalUniformization.local_uniformization Local uniformization in positive characteristic sorry line 123 source
Source documentation
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.

depends on sorry what this means
Statement uses: Field, Algebra, Algebra.EssFiniteType, Nat, Fact, Nat.Prime, CharP, ValuationSubring, Membership.mem, RingHom, Algebra.algebraMap, ValuationSubring.HasLocalUniformization
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat
31 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
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 := by
…
```
theorem LocalUniformization.local_uniformization_of_charZero Zariski's local uniformization theorem sorry line 135 source
Source documentation
Zariski's local uniformization theorem. Every valuation ring of a finitely generated field extension $F \mid k$ that contains a field $k$ of characteristic zero admits local uniformization over $k$. This is the main theorem of [Zar1940].

depends on sorry what this means
Statement uses: Field, Algebra, Algebra.EssFiniteType, CharZero, ValuationSubring, Membership.mem, RingHom, Algebra.algebraMap, ValuationSubring.HasLocalUniformization
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Nat
31 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem local_uniformization_of_charZero (k F : Type*) [Field k] [Field F] [Algebra k F]
    [Algebra.EssFiniteType k F] [CharZero k] (𝒪 : ValuationSubring F)
    (hk : ∀ x : k, algebraMap k F x ∈ 𝒪) :
    𝒪.HasLocalUniformization k := by
…
```
theorem LocalUniformization.local_uniformization_of_trdeg_le_three Local uniformization holds in transcendence degree at most three over any field sorry line 153 source
Source documentation
Local uniformization holds in transcendence degree at most three over any field. In characteristic zero this is [Zar1940]. In positive characteristic, surfaces are [Abh1956]; threefolds over an algebraically closed field of characteristic $p > 5$ are [Abh1966], simplified in [Cut2009]; and the remaining characteristics $2, 3, 5$ are [CP2008] and [CP2009], for quasi-projective threefolds over a field $k$ with $[k : k^p] < \infty$. It follows in the generality stated here from [CP2019], Theorem 1.1, which resolves the singularities of every reduced separated Noetherian quasi-excellent scheme of dimension at most three in any characteristic: the centre of $\mathcal{O}$ on a resolution of a proper model of $F \mid k$ is a regular point.

depends on sorry what this means
Statement uses: Field, Algebra, Algebra.EssFiniteType, ValuationSubring, Membership.mem, RingHom, Algebra.algebraMap, LE.le, Cardinal, Algebra.trdeg, OfNat.ofNat, Nat, ValuationSubring.HasLocalUniformization
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
34 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem local_uniformization_of_trdeg_le_three (k F : Type*) [Field k] [Field F] [Algebra k F]
    [Algebra.EssFiniteType k F] (𝒪 : ValuationSubring F)
    (hk : ∀ x : k, algebraMap k F x ∈ 𝒪) (hF : Algebra.trdeg k F ≤ 3) :
    𝒪.HasLocalUniformization k := by
…
```
theorem LocalUniformization.local_uniformization_after_finite_extension Local uniformization after a finite extension sorry line 166 source
Source documentation
Local uniformization after a finite extension. Every valuation ring of a finitely generated field extension $F \mid k$ that contains $k$ admits local uniformization over $k$ after a finite extension $E$ of $F$, in any characteristic. This is the main theorem of [KK2009]. Compare [Tem2013], where the extension of $F$ is purely inseparable but the ground field is extended too.

depends on sorry what this means
Statement uses: Field, Algebra, Algebra.EssFiniteType, ValuationSubring, Membership.mem, RingHom, Algebra.algebraMap, Exists, IntermediateField, AlgebraicClosure, FiniteDimensional, Subtype, And, Eq, ValuationSubring.comap, ValuationSubring.HasLocalUniformization
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Nat
59 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem local_uniformization_after_finite_extension (k F : Type*) [Field k] [Field F]
    [Algebra k F] [Algebra.EssFiniteType k F] (𝒪 : ValuationSubring F)
    (hk : ∀ x : k, algebraMap k F x ∈ 𝒪) :
    ∃ (E : IntermediateField F (AlgebraicClosure F)) (_ : FiniteDimensional F E)
      (𝒪' : ValuationSubring E),
      𝒪'.comap (algebraMap F E) = 𝒪 ∧ 𝒪'.HasLocalUniformization k := by
…
```