Regular surface models and exceptional-curve contraction

Teaching exposition, CC0 1.0. This supplies the surface-model prerequisite in the semistable-model argument. The complete original licensed proof body is included as editable resolve.tex, with its actual within-chapter induction and contraction proofs.

Source and terms

The surface-resolution proof is available in

the full editable surface-resolution chapter

Surface-resolution source, source COPYING. The COPYING file states GNU Free Documentation License 1.2. This native chapter retains human Stacks authorship and its credited AI Integrated Stacks contributions, under applicable GFDL terms. The bridge and explanations written here are CC0; the native chapter and its adaptations retain their source notices.

Exact proof locators and dependency map

Used result Source locator and line What the actual proof does
Surface resolution resolve-theorem-resolve, 0BGP, line 3945 Proves condition(4) implies a finite normalized-point-blowup resolution, using the complete local induction, compatibility with completion, and gluing of local point sequences
Complete normal local surface resolution resolve-lemma-resolve-complete, 0BGN, line 3834 Induction on degree over a complete regular local subring; smaller intermediate extensions handled by induction; indecomposable separable or purely inseparable degree-p extensions reduce to rational singularities
Boundedness in the separable step resolve-lemma-go-up-separable, line 1922 Trace/discriminant inclusion bounds cohomology modulo fixed torsion; lemma-bound-a-torsion, line 1730, bounds that torsion by curve-normalization length
Boundedness in the inseparable step resolve-lemma-go-up-degree-p, line 2132 Constructs the degree-p differential trace, produces independent functionals on the basis\(1,g,\ldots,g^{p-1}\), and bounds the dualizing-trace cokernel; Matlis duality and the preceding torsion bound control \(H^1\)
Actual differential-trace proof resolve-lemma-trace-well-defined, line 183; lemma-trace-higher, line 284; lemma-trace-extends, line 374 Universal polynomial calculation proves coordinate independence; wedge construction; codimension-one extension over degree-p finite DVR extensions
Surface vanishing used in boundedness resolve-proposition-Grauert-Riemenschneider, line 1621 Proves vanishing by dualizing a hypothetical map to the residue field and contradicting the previously proved derived \(H^1\)-injectivity statement; it is not merely a characteristic-zero vanishing citation
Reduction to rational singularities resolve-lemma-reduce-to-rational, line 1870 Maximizes the bounded \(H^1\) length; Leray exactness forces every further local modification to have zero \(R^1\); dominates by normalized point blowups
Rational to Gorenstein resolve-lemma-rational-to-gorenstein, 0BBV, line 2471 Blow up the Fitting ideal to make the strict transform of the rank-one dualizing module invertible; proved normality and dualizing surjectivity along rational blowups identify it with the target dualizing module
Rational double points resolve-lemma-resolve-rational-double-points, 0BGE, line 3499 Actual preceding calculations3061–3498 treat nonsquare and square quadratic tangent cones in every characteristic and terminate via the nonsingular-arc arguments
Termination along an arc resolve-lemma-sequence-blowups, line 2586; lemma-sequence-blowups-along-arc-becomes-nonsingular, line 2680 Successive jets produce a complete DVR; equations decrease their uniformizer exponents until a generator can be removed and the local ring is regular
Completion and global gluing resolve-lemma-normalized-blowup-completion, line 3019; lemma-port-regularity-to-completion, line 2780; lemma-equivalence-sequence-normalized-blowups, line 1324 Descends the finite normalized point sequences and transfers regularity by flat completion; assembles the finitely many closed-point sequences globally
Actual exceptional-curve contraction resolve-lemma-contraction, 0C2L, line 4461 Stein factorization, formal functions and the exceptional thickening algebra give a regular2dim target point; the universal blowup map and conormal calculation identify the original surface with its blowup
Projective contraction preserving ampleness resolve-lemma-contract-ample, 0C2M, line 4666 Uses \(L(nE)\), a section nonzero on \(E\) and sections giving the original projective embedding; the resulting projective-space map is quasi-finite off \(E\) and constant on \(E\), and its Stein factor is the contraction with ample descended line bundle
Thickening/cohomology behind contraction resolve-lemma-exceptional-first-kind-local, line 4387; lemma-pic-blowup, line 4560; lemma-lift-sections-and-h1, line 4638 Computes the associated graded thickening algebra as \(k[x,y]\), descends degree-zero line bundles and proves the required \(H^1\) vanishings by the exact \(E\)-filtration

The quadratic-transformation and domination arguments, lines449–1357, supply two steps: colength decreases under a regular point blowup; normal modifications are dominated by normalized point sequences using the decreasing order of a transcendental residue \(a/b\) along a bad curve. These are not derived from an assumed surface-resolution theorem.

The precise excellent-trait bridge

Let \(R\) be the excellent equicharacteristic trait obtained in S.3a, and let \(C/K\) be the smooth geometrically connected curve of genus \(G\ge2\) after the finite separable torsion-visibility extension. Its smooth proper generic curve is projective. Choose a closed embedding in \(\mathbf P^m_K\), and take its schematic closure \(Y\) in \(\mathbf P^m_R\). The closure is integral and has no \(R\)-torsion; over a DVR, torsion-free modules are flat. It is therefore a projective flat model of \(C\).

Finite type over excellent \(R\) is excellent. Normalize \(Y\); this is finite, hence projective, and is unchanged on its already normal smooth generic curve. A normal surface has regular local rings in \(\operatorname{codim}\le1\). Its singular locus is closed because the scheme is excellent; it consequently consists of finitely many closed points. Their completed local rings are normal, since completion maps of excellent local rings are regular and normality ascends under regular maps. Thus condition(4) of0BGP is verified for \(Y\), with every hypothesis visible.

The actual forward proof of0BGP now gives normalized point blowups producing a regular surface \(X\). Each point blowup is projective and each normalization is finite in this excellent scope. Hence \(X\) is already projective over \(R\). This proves the projectivity needed by the numerical curve proof directly; it does not need the separate broad resolve-lemma-regular-dim-2-projective assertion. The modification is an isomorphism on the generic curve because that curve is a normal1dim scheme and its points have \(\operatorname{codim}\le1\) in the surface. A proper birational modification of a normal surface is an isomorphism above those points. The phrase in models-lemma-regular that an arbitrary resolution is an isomorphism on the entire normal locus is too broad: one can blow up a regular closed surface point. Only the \(\operatorname{codim}\le1\) generic-curve assertion is used here.

If \(X\) contains an exceptional curve of the first kind \(E\), it lies in the special fibre: a complete projective1dim exceptional curve cannot be a proper closed subcurve of the smooth integral generic curve. Its defining properties are \(E\simeq\mathbf P^1\) over its constant field, \(E\) Cartier, and normal bundle \(\mathcal O_E(-1)\). Apply0C2M to an ample line bundle. The contraction is a projective regular surface over \(R\), agrees with \(X\) off \(E\), and remains an integral flat model of \(C\). Flatness again follows from absence of \(R\)-torsion. One special-fibre irreducible component has been contracted and all other components have their distinct birational images. The finite component count decreases by one. Iterating therefore terminates and produces the minimal regular projective model used in the actual semistable proof.

No base function-field extension is made by these projective modifications. The completed trait and its torsion field are used to check properness only; S.7 determines the alteration's final separable base field independently.

Main components in normalized pullbacks

Two corrections to the native proof appear in the annotated patch and the corrected editable teaching version. The separately retained original resolve.tex retains its source terms.

At original resolve.tex, line1110, in the normalized-point-blowup domination proof, the normalization of the entire fibre product need not be birational: extra vertical components can occur. For example the self-fibre-product of the blowup of the origin of the affine plane includes the product of its exceptional divisors. Instead take the schematic closure of the common open graph in the fibre product, its dominant strict-transform/main component, and then normalize. This closure is integral, proper and birational over the original model. Finite normalization is available in the excellent scope used here. The injection of bad curves and the subsequent valuation decrease now concern this proper birational model, exactly as needed.

At original line3867, in resolve-lemma-resolve-complete, for an intermediate field use the dominant main component of the pullback of the resolved intermediate model, then its finite normalization. Its generic field is the specified upper field, so it is finite dominant over the resolved intermediate model of degree equal to that upper/intermediate field degree, strictly smaller than the induction degree. It is proper birational over the upper normal local surface. After local completion the finite factors have degree at most that smaller degree, so the completed local induction applies. Excellence supplies finite normalization and normal completion. Extra components of the unrestricted fibre product are never declared birational or used in the induction.

The annotations and modified teaching source retain the original source's GFDL terms and credits. Their original proof locators are listed in the correction record.

Further proof details

The following fills in the source's omitted details needed for this application.

  1. In0C2M the projective-space map is proper: \(X\) is proper over affine \(S\), the projective-space target is separated over \(S\), and the graph factorization is closed followed by the base change of \(X\to S\). The Stein factor remains quasi-finite off \(E\), since there the original map is quasi-finite and the Stein map has connected fibres; a connected zero-dimensional fibre is one point. \(E\) cannot join a different fibre point to the contracted point because its image has all first embedding coordinates zero, while every point off \(E\) has at least one such coordinate nonzero. The normal thickening calculation in0C2L proves regularity at the image point; elsewhere the contraction is the identity.

    Distinguish the restriction degree \(d=\deg(L|_E)\) from the embedding dimension \(r\). Choose embedding sections \(t_0,\ldots,t_r\) and use \(M=L(dE)\), with the additional section \(s_{r+1}\) nonzero on \(E\). The map is to \(\mathbf P^{r+1}_S\). The source uses the letter \(n\) for both numbers; no equality between them is required for the proof.

  2. In the cohomology lemma at4638, use \(0\to L((j-1)E)\to L(jE)\to\mathcal O_E(n-j)\to0\). For\(1\le j\le n+1\) the last \(H^1\) vanishes because \(n-j\ge-1\). Induction gives the \(H^1\) vanishing used to lift the section of \(L(nE)\) nonzero on \(E\). For \(n\le0\), at\(j=1\) the last \(H^0\) vanishes because \(n-1\le-1\), giving the stated \(H^1\) injection. These are exact elementary P1 computations.

  3. In the last square-cone double-point calculation, a is a unit and the leading equation is \(x_3^2+x_1(ax_2^2+bx_2x_3+cx_3^2)\) modulo \(\mathfrak m^4\). On the x2-chart set \(x_1=x_2u\) and \(x_3=x_2v\). The equation becomes \(v^2+x_2u(a+bv+cv^2)\) modulo terms divisible by \(x_2^2\). On the exceptional locus \(v=0\), a point with \(u\ne0\) is regular because the x2-linear coefficient is a unit. At \(u=0\) the quadratic tangent cone has the nonzero cross term \(ax_2u\), so any singular point there belongs to the already treated nonsquare caseI. The x3-chart has no exceptional point because its reduced equation is\(1=0\). Thus a remaining square-cone caseII point lies on the x1-chart exactly as claimed by the source's brief calculation. Its inherited x1 gives the arc invariant, and the proved arc termination applies.

  4. Local normalized-point sequences can be assembled without assuming that \(\operatorname{Spec}\) of a local ring is an open neighbourhood. A centre above a singular point is an actual closed point of the current global surface; the source's special-fibre identification identifies it with its local-sequence point. Blow up that global point, normalize, and repeat. Operations at distinct original closed points agree with the identity away from their point and are combined one at a time. This is the explicit sequence proof at1324. It also explains why the required completion descent concerns point blowups and finite normalization, rather than arbitrary formal algebraization.

Typographical slips in the source do not become mathematical claims here: the \(H^0\) blowup diagram's displayed graded quotient is to be \(\mathfrak m^{n-1}/\mathfrak m^n\), not its reverse; the final degree-p trace coefficient has the corresponding p-th power; and the tangent conic is inside \(\mathbf P^2\). The correct graded ring, derivative and quadratic calculations are supplied in the surrounding actual proofs.

Foundations retained, and integration boundary

This is a full openly licensed surface-resolution proof provider for the needed excellent2dim scope, with the projective/minimal-model application written above. It retains its explicit ordinary foundations: Cohen complete regular subring existence, excellence and finite normalization, coherent proper finiteness/formal functions, Grothendieck duality and Matlis/local duality, ordinary curve Riemann–Roch, and the two More-on-Flatness modification lemmas used to dominate a modification by a blowup and make a strict transform finite. The complete source bodies for the latter are in flat.tex: flat-lemma-dominate-modification-by-blowup and flat-lemma-finite-after-blowing-up, with exact locators in the native index. These foundations remain prerequisites of the bridge.

The stable-moduli properness and projective family-extension conclusion still come from the S.1–S.9 argument, using this actual model-existence input. A reference to0BGP alone would not supply that conclusion. The full licensed proof body and its annotated corrections are retained with GFDL/source notices; the model application above is CC0 exposition.