ResolutionOfSingularities.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

7 declarations, 4 contain sorry, 0 declared as axioms

Resolution of singularities

A variety $X$ over a field $k$ admits a resolution of singularities if there is a smooth $k$-variety $Y$ and a proper birational morphism $Y \to X$. Hironaka proved that every variety over a field of characteristic zero admits one. In positive characteristic this is known over a perfect field in dimension at most three, and is open from dimension four on. Perfectness of $k$ cannot be dropped from the statement in this form: over an imperfect field it fails already in dimension zero, see exists_not_hasResolution_of_not_perfectField below. Over an arbitrary field one asks instead that $Y$ be regular.

References:

Wikipedia
[Hir1964] H. Hironaka, Resolution of singularities of an algebraic variety over a field of characteristic zero, I and II, Ann. of Math. 79 (1964), 109--203 and 205--326.
[Kol2007] J. Kollár, Resolution of singularities -- Seattle lecture, Theorem 36.
[Hau2010] 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.
[Lip1978] J. Lipman, Desingularization of two-dimensional schemes, Ann. of Math. 107 (1978), 151--207.
[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.
[CP2019] V. Cossart and O. Piltant, Resolution of singularities of arithmetical threefolds, J. Algebra 529 (2019), 268--535.

Imports (1)

FormalConjecturesUtil

def AlgebraicGeometry.Scheme.HasResolution Documented declaration: HasResolution line 67 source
Source documentation
A scheme X over a base S with structure morphism sX : X ⟶ S admits a resolution of singularities if there is an integral scheme Y, smooth over S, together with a proper morphism f : Y ⟶ X that is birational over X, i.e. that restricts to an isomorphism between dense open subschemes of Y and of X.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: AlgebraicGeometry.Scheme, Quiver.Hom
Proof uses: Exists, And, AlgebraicGeometry.IsIntegral, AlgebraicGeometry.IsProper, AlgebraicGeometry.Smooth, CategoryTheory.CategoryStruct.comp, AlgebraicGeometry.Scheme.BirationalOver, CategoryTheory.CategoryStruct.id
7 instances, coercions and auxiliary constants left out.
```
def Scheme.HasResolution {S X : Scheme.{u}} (sX : X ⟶ S) : Prop :=
…
```
theorem AlgebraicGeometry.Scheme.hasResolution_of_smooth A scheme that is already smooth over the base is its own resolution line 73 source
Source documentation
A scheme that is already smooth over the base is its own resolution.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: AlgebraicGeometry.Scheme, Quiver.Hom, AlgebraicGeometry.IsIntegral, AlgebraicGeometry.Smooth, AlgebraicGeometry.Scheme.HasResolution
Proof uses: Exists.intro, Exists, And, AlgebraicGeometry.IsProper, CategoryTheory.CategoryStruct.comp, AlgebraicGeometry.Scheme.BirationalOver, CategoryTheory.CategoryStruct.id, And.intro, inferInstance, Eq.mpr, id, Eq, congrArg, CategoryTheory.Category.id_comp, AlgebraicGeometry.Scheme.BirationalOver.refl
12 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem Scheme.hasResolution_of_smooth {S X : Scheme.{u}} (sX : X ⟶ S) [IsIntegral X]
    [Smooth sX] : Scheme.HasResolution sX :=
…
```
Mentions: AlgebraicGeometry.Scheme.HasResolution
theorem AlgebraicGeometry.Scheme.surjective_of_birationalOver_id A proper birational morphism onto a scheme is surjective line 83 source
Source documentation
A proper birational morphism onto a scheme is surjective. In particular a resolution of singularities is onto, which is what rules out the inclusion of the smooth locus of X as a trivial solution.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: AlgebraicGeometry.Scheme, Quiver.Hom, AlgebraicGeometry.IsProper, AlgebraicGeometry.Scheme.BirationalOver, CategoryTheory.CategoryStruct.id, Function.Surjective, CommRingCat, AlgebraicGeometry.SheafedSpace.toPresheafedSpace, AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace, AlgebraicGeometry.Scheme.toLocallyRingedSpace, TopCat, ContinuousMap, CategoryTheory.ConcreteCategory.hom, AlgebraicGeometry.PresheafedSpace.Hom.base, AlgebraicGeometry.LocallyRingedSpace.Hom.toHom, AlgebraicGeometry.Scheme.Hom.toLRSHom'
Proof uses: AlgebraicGeometry.Scheme.PartialIso, AlgebraicGeometry.Scheme.PartialIso.IsOver, AlgebraicGeometry.Scheme.PartialIso.source, Eq, AlgebraicGeometry.Scheme.Opens.ι, AlgebraicGeometry.Scheme.PartialIso.target, CategoryTheory.Iso.hom, AlgebraicGeometry.Scheme.PartialIso.iso, id, Eq.mp, CategoryTheory.CategoryStruct.comp, TopCat.Hom.hom, congrArg, congrFun', ContinuousMap.comp, AlgebraicGeometry.PresheafedSpace.Hom, AlgebraicGeometry.LocallyRingedSpace.Hom, CategoryTheory.Category.comp_id, Eq.symm, Dense and 24 more
37 instances, coercions and auxiliary constants left out.

Tactic trace: 11 steps
Open to load the checked before-and-after goal states.
```
theorem Scheme.surjective_of_birationalOver_id {X Y : Scheme.{u}} (f : Y ⟶ X) [IsProper f]
    (hf : Scheme.BirationalOver f (𝟙 X)) : Function.Surjective f.base := by
…
```
theorem AlgebraicGeometry.resolution_of_singularities Resolution of singularities in positive characteristic sorry line 105 source
Source documentation
Resolution of singularities in positive characteristic. Let $k$ be a perfect field of characteristic $p > 0$ and let $X$ be an integral scheme that is separated and of finite type over $k$. Then there is an integral scheme $Y$ that is smooth over $k$ together with a proper birational morphism $Y \to X$.
This is open from dimension four on; see [Hau2010]. Perfectness of $k$ is needed for the conclusion as stated; see exists_not_hasResolution_of_not_perfectField.

depends on sorry what this means
Statement uses: Field, PerfectField, Nat, Fact, Nat.Prime, CharP, AlgebraicGeometry.Scheme, Quiver.Hom, AlgebraicGeometry.Spec, CommRingCat.of, AlgebraicGeometry.IsIntegral, AlgebraicGeometry.LocallyOfFiniteType, AlgebraicGeometry.QuasiCompact, AlgebraicGeometry.IsSeparated, AlgebraicGeometry.Scheme.HasResolution
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat
17 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem resolution_of_singularities (k : Type u) [Field k] [PerfectField k] (p : ℕ)
    [Fact p.Prime] [CharP k p] {X : Scheme.{u}} (sX : X ⟶ Spec (.of k)) [IsIntegral X]
    [LocallyOfFiniteType sX] [QuasiCompact sX] [IsSeparated sX] :
    Scheme.HasResolution sX := by
…
```
Mentions: AlgebraicGeometry.Scheme.HasResolution
theorem AlgebraicGeometry.resolution_of_singularities_of_charZero Hironaka's theorem sorry line 117 source
Source documentation
Hironaka's theorem. Every integral scheme that is separated and of finite type over a field of characteristic zero admits a resolution of singularities. This is the main theorem of [Hir1964]; see [Kol2007], Theorem 36, for a statement in the generality used here.

depends on sorry what this means
Statement uses: Field, CharZero, AlgebraicGeometry.Scheme, Quiver.Hom, AlgebraicGeometry.Spec, CommRingCat.of, AlgebraicGeometry.IsIntegral, AlgebraicGeometry.LocallyOfFiniteType, AlgebraicGeometry.QuasiCompact, AlgebraicGeometry.IsSeparated, AlgebraicGeometry.Scheme.HasResolution
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Nat
17 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem resolution_of_singularities_of_charZero (k : Type u) [Field k] [CharZero k]
    {X : Scheme.{u}} (sX : X ⟶ Spec (.of k)) [IsIntegral X] [LocallyOfFiniteType sX]
    [QuasiCompact sX] [IsSeparated sX] :
    Scheme.HasResolution sX := by
…
```
Mentions: AlgebraicGeometry.Scheme.HasResolution
theorem AlgebraicGeometry.resolution_of_singularities_of_topologicalKrullDim_le_three Resolution of singularities holds in dimension at most three over any perfect field sorry line 134 source
Source documentation
Resolution of singularities holds in dimension at most three over any perfect field. In characteristic zero this is [Hir1964]. In positive characteristic, dimension at most two is [Lip1978] and dimension three is due to Cossart and Piltant: [CP2008] and [CP2009] prove it for quasi-projective varieties over a field that is differentially finite over a perfect subfield, and [CP2019], Theorem 1.1, removes both restrictions, resolving every reduced separated Noetherian quasi-excellent scheme of dimension at most three in any characteristic. That theorem gives an everywhere regular source, which over a perfect field is the same as a smooth one. The problem is open in positive characteristic from dimension four on.

depends on sorry what this means
Statement uses: Field, PerfectField, AlgebraicGeometry.Scheme, Quiver.Hom, AlgebraicGeometry.Spec, CommRingCat.of, AlgebraicGeometry.IsIntegral, AlgebraicGeometry.LocallyOfFiniteType, AlgebraicGeometry.QuasiCompact, AlgebraicGeometry.IsSeparated, LE.le, WithBot, ENat, topologicalKrullDim, CommRingCat, AlgebraicGeometry.SheafedSpace.toPresheafedSpace, AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace, AlgebraicGeometry.Scheme.toLocallyRingedSpace, OfNat.ofNat, Nat and 1 more
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 resolution_of_singularities_of_topologicalKrullDim_le_three (k : Type u) [Field k]
    [PerfectField k] {X : Scheme.{u}} (sX : X ⟶ Spec (.of k)) [IsIntegral X]
    [LocallyOfFiniteType sX] [QuasiCompact sX] [IsSeparated sX]
    (hX : topologicalKrullDim X ≤ 3) :
    Scheme.HasResolution sX := by
…
```
Mentions: AlgebraicGeometry.Scheme.HasResolution
theorem AlgebraicGeometry.exists_not_hasResolution_of_not_perfectField Resolution of singularities fails over imperfect fields sorry line 156 source
Source documentation
Resolution of singularities fails over imperfect fields. If the field $k$ is not perfect, then there is an integral scheme $X$ of dimension zero that is separated and of finite type over $k$ and has no resolution of singularities: no integral scheme smooth over $k$ admits a proper birational morphism to $X$.
A witness: $k$ has characteristic $p > 0$ and there is some $a \in k \setminus k^p$. Take $X = \operatorname{Spec} k(a^{1/p})$. Every integral scheme birational to $X$ has function field $k(a^{1/p})$, which is not separable over $k$, whereas the function field of an integral scheme smooth over $k$ is separable over $k$.
So the hypothesis PerfectField k cannot be dropped from resolution_of_singularities or from resolution_of_singularities_of_topologicalKrullDim_le_three.

depends on sorry what this means
Statement uses: Field, Not, PerfectField, Exists, AlgebraicGeometry.Scheme, Quiver.Hom, AlgebraicGeometry.Spec, CommRingCat.of, And, AlgebraicGeometry.IsIntegral, AlgebraicGeometry.LocallyOfFiniteType, AlgebraicGeometry.QuasiCompact, AlgebraicGeometry.IsSeparated, Eq, WithBot, ENat, topologicalKrullDim, CommRingCat, AlgebraicGeometry.SheafedSpace.toPresheafedSpace, AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace and 3 more
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, Nat
29 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem exists_not_hasResolution_of_not_perfectField (k : Type u) [Field k]
    (hk : ¬ PerfectField k) :
    ∃ (X : Scheme.{u}) (sX : X ⟶ Spec (.of k)), IsIntegral X ∧ LocallyOfFiniteType sX ∧
      QuasiCompact sX ∧ IsSeparated sX ∧ topologicalKrullDim X = 0 ∧
      ¬ Scheme.HasResolution sX := by
…
```
Mentions: AlgebraicGeometry.Scheme.HasResolution