Hartshorne, Algebraic Geometry — Chapter V: Surfaces
FC06 — Hartshorne, Algebraic Geometry.
This chapter contains 11 definitions, 20 theorems, 20 propositions, 8 lemmas, 18 corollaries, 28 examples, 36 remarks, 2 conventions and 2 notations.
Of the 145 statements checked against Lean, 1 are formalized somewhere and 144 are not.
| Status | Statements | Share | What it means |
|---|---|---|---|
| not formalized | 144 | 99% | A documented search found no Lean statement of it anywhere. |
| in Mathlib | 1 | 1% | Mathlib states and proves it. |
| checked in total | 145 |
- Canonical source block: FC06 Hartshorne, Chapter V,
FC06-C05-U001–FC06-C05-U145, in canonical source-ID order. Immediately before this audit the live FC06 master, read through agent-memory, recorded C01–C04 complete and C05 active. The concurrently owned C02 block and its scratch files were not modified. - Project-first inspection is recorded against repository
A=3b2239e161592472b34e02ad3b7da308f9ce7280. Pinned Mathlib isP=db584cd6d46c92f209a44c0f1c829460d327499d, Lean 4.33.0, Apache-2.0. Current Mathlib was checked atH=5aedf732b6987e8c26ab3c9ebc855314f82b045f. The C03/C04 generator pattern is reused: parse and contiguity-check the canonical unit table, emit exactly one route per ID, verify every positive pinned path/declaration, and keep strict whole-row interface comparisons. - Strict bundle semantics govern every row. A route must realize the complete source statement. Generic prerequisites, one clause/example, a specialization without the required comparison bridge, a theorem with
sorry, an unproved blueprint, or a merely related construction does not count. - Project source searches covered surface intersection theory, Hodge/Nakai, ruled and Hirzebruch surfaces, projective bundles, blowups/exceptional curves/resolution, cubic and del Pezzo surfaces, Cremona transformations, birational surface factorization, Castelnuovo contraction/minimal models, Kodaira dimension and surface classification. No project-existing owner of a complete C05 row was found.
- Pinned Mathlib has mature scheme rational-map/birational infrastructure. U116 is a direct owner:
Scheme.RationalMap.domainis the supremum of all representative domains,PartialMap.le_domain_toRationalMapis its maximality inclusion, andScheme.RationalMap.toPartialMaprealizes a rational map on that domain for reduced source and separated target. Smooth projective surfaces satisfy those hypotheses; Hartshorne’s fundamental-point set is the complement of the maximal domain. - The same rational-map infrastructure does not construct the closed graph/total transform of U117 or the codimension, connectedness, blowup-factorization and surface-factorization theorems U118–U127. Those rows remain unmatched.
- Pinned
Mathlib/RingTheory/ReesAlgebra.leanexplicitly presents the Rees algebra as groundwork useful for defining blowups in the future; no pinned blowup scheme exists. This agrees with the already-promoted C02 U239/U243 unmatched decisions for blowup-by-Proj and its exceptional ideal. Consequently none of the point-blowup, exceptional-curve, Picard/intersection-transform, resolution, Cremona, cubic-surface or Castelnuovo rows can be promoted from Rees/Proj primitives alone. - Pinned/current searches found no surface intersection pairing, Hodge index theorem, Nakai–Moishezon criterion, geometrically ruled/projective-bundle surface classification, Birkhoff–Grothendieck splitting, cubic-surface 27-lines theorem, Kodaira dimension, or Enriques–Kodaira classification.
- Current/open Mathlib searches on 2026-09-06 found no open PR matching blowup schemes, Hodge index/Nakai, ruled surfaces, cubic surfaces, Castelnuovo contraction or Kodaira dimension. Generic Zariski Main Theorem and birationality code is retained only as near-miss evidence for U120 and later rows because the Hartshorne total-transform/factorization statements are absent.
- External/current checks included
a-dangelo/Lean-AGat35d2ef18d5c2b3800312c1b3e2c67d176a19e6fd(Apache-2.0), whose public roadmap still lists intersection theory and Bézout/Zariski-Main work as future work; it has no checked C05 surface route.ProjConstruction/Projated778ef92453f1be91988cbcd11dded470eea8d3formalizes multigraded Proj and ring dilatations. The associated Mayeux–Zhang 2026 JAR article explicitly states that the global quasi-coherent Proj construction needed for scheme blowups is not carried out and is future work, so it does not supply the point-blowup rows. - No checked project/P/H/open/external route was found for the Hodge–Nakai programme, ruled-surface classification, blowup/resolution theory, cubic/del Pezzo surface geometry, surface factorization/minimal models, or Kodaira-dimension classification beyond the exact U116 rational-map-domain definition.
N=2026-09-06marks a dated unmatched decision after project-first, pinned/current Mathlib, open/current work, indexed web/GitHub search, and relevant external Lean checks.
Convention — surfaces, curves, and points in Chapter V
A surface means a nonsingular projective surface over the fixed algebraically closed field k. A curve on a surface means any effective divisor, possibly singular, reducible, or nonreduced; points are closed unless stated otherwise.
Not formalized. none; no complete checked declaration under strict bundle semantics — Mathlib has schemes, regularity/smoothness, projectivity and divisors separately, but no checked bundled “surface” interface imposing Hartshorne’s nonsingular-projective convention together with his curve/closed-point conventions.
Definition/construction — transverse intersection and divisor intersection pairing setup
Two curves C,D meet transversally at P when local equations generate the maximal ideal of O_{X,P}. Div X is the divisor group and Pic X the group of invertible sheaves, identified with divisors modulo linear equivalence.
Not formalized. none; no complete checked declaration under strict bundle semantics — Cartier divisors/Picard-type primitives exist in Mathlib, but no checked surface intersection-multiplicity interface realizes the transverse-intersection setup and divisor/Picard identification as one source row.
Theorem 1.1
There is a unique symmetric bilinear pairing Div X×Div X→Z, written C·D, invariant under linear equivalence and normalized so that two nonsingular curves meeting transversally have intersection equal to the number of intersection points.
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked P/H surface intersection pairing Div X × Div X → Z with Hartshorne’s uniqueness, bilinearity, linear-equivalence invariance and transverse normalization was found.
Lemma 1.2
Given irreducible curves C_1,…,C_r and a very ample divisor D on a surface, a general member D′∈|D| is irreducible, nonsingular, and meets every C_i transversally.
Not formalized. none; no complete checked declaration under strict bundle semantics — As of 2026-09-06, no checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: Given irreducible curves C_1,…,C_r and a very ample divisor D on a surface, a general member D′∈|D| is irreducible, nonsingular, and meets every C_i transversally. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, an incomplete proof, or a proper subset as the route for this ID.
Lemma 1.3
If C is an irreducible nonsingular curve and D meets C transversally, then # (C∩D)=deg_C(L(D)|_C).
Not formalized. none; no complete checked declaration under strict bundle semantics — As of 2026-09-06, no checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: If C is an irreducible nonsingular curve and D meets C transversally, then # (C∩D)=deg_C(L(D)|_C). Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, an incomplete proof, or a proper subset as the route for this ID.
Proposition 1.4
If \(C\) and \(D\) are curves on \(X\) having no common irreducible component, then \[ C . D = \sum _ { P \in C \cap D } ( C . D ) _ { P } . \]
Not formalized. none; no complete checked declaration under strict bundle semantics — As of 2026-09-06, no checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: If \(C\) and \(D\) are curves on \(X\) having no common irreducible component, then \[ C . D = \sum _ { P \in C \cap D } ( C . D ) _ { P } . \] Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, an incomplete proof, or a proper subset as the route for this ID.
Example 1.4.1
For a curve C on a surface, the self-intersection C² equals deg_C L(C)|C; equivalently it is the degree of the normal sheaf N{C/X}.
Not formalized. none; no complete checked declaration under strict bundle semantics — As of 2026-09-06, no checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: For a curve C on a surface, the self-intersection C² equals deg_C L(C)|C; equivalently it is the degree of the normal sheaf N{C/X}. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, an incomplete proof, or a proper subset as the route for this ID.
Example 1.4.2
On P² the class h of a line generates Pic P² and h²=1; hence curves of degrees n and m have intersection number nm, recovering Bézout when they have no common component.
Not formalized. none; no complete checked declaration under strict bundle semantics — As of 2026-09-06, no checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: On P² the class h of a line generates Pic P² and h²=1; hence curves of degrees n and m have intersection number nm, recovering Bézout when they have no common component. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, an incomplete proof, or a proper subset as the route for this ID.
Example 1.4.3
On a smooth quadric Q≅P¹×P¹, the two ruling classes l,m satisfy l²=m²=0 and l·m=1; consequently divisors of types (a,b) and (a′,b′) intersect in ab′+a′b.
Not formalized. none; no complete checked declaration under strict bundle semantics — As of 2026-09-06, no checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: On a smooth quadric Q≅P¹×P¹, the two ruling classes l,m satisfy l²=m²=0 and l·m=1; consequently divisors of types (a,b) and (a′,b′) intersect in ab′+a′b. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, an incomplete proof, or a proper subset as the route for this ID.
Example 1.4.4
For an effective divisor D on a surface, p_a(D)=1+1/2·D·(D+K_X).
Not formalized. none; no complete checked declaration under strict bundle semantics — As of 2026-09-06, no checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: For an effective divisor D on a surface, p_a(D)=1+1/2·D·(D+K_X). Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, an incomplete proof, or a proper subset as the route for this ID.
Proposition 1.5
Adjunction for surfaces: if C is a nonsingular genus-g curve on X and K_X is canonical, then 2g−2=C·(C+K_X).
Not formalized. none; no complete checked declaration under strict bundle semantics — As of 2026-09-06, no checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: Adjunction for surfaces: if C is a nonsingular genus-g curve on X and K_X is canonical, then 2g−2=C·(C+K_X). Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, an incomplete proof, or a proper subset as the route for this ID.
Example 1.5.1
This gives a quick method of computing the genus of a curve on a surface. For example, if \(C\) is a curve of degree \(d\) in \(\mathbf { P } ^ { 2 }\) ,then \[ 2 g \ : - \ : 2 \ : = \ : d ( d \ : - \ : 3 ) \] so \(\begin{array} { r } { \langle J \rangle = \frac { 1 } { 2 } ( d - 1 ) ( d - 2 ) } \end{array}\) Cf. (II,Ex. 8.4).
Not formalized. none; no complete checked declaration under strict bundle semantics — As of 2026-09-06, no checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: This gives a quick method of computing the genus of a curve on a surface. For example, if \(C\) is a curve of degree \(d\) in \(\mathbf { P } ^ { 2 }\) ,then \[ 2 g \ : - \ : 2 \ : = \ : d ( d \ : - \ : 3 ) \] so \(\begin{array} { r } { \langle J \rangle = \frac { 1 } { 2 } ( d - 1 ) ( d - 2 ) } \end{array}\) Cf. (II,Ex. 8.4). Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, an incomplete proof, or a proper subset as the route for this ID.
Example 1.5.2
If \(C\) is a curve of type \(^ { ( a , b ) }\) on the quadric surface, then \(C + K\) has type \(( \not { a } \ : - \ : 2 , \ : b \ : - \ : 2 )\) ,so \[ 2 g \ : - \ : 2 \ : = \ : a ( b \ : - \ : 2 ) \ : + \ : ( a \ : - \ : 2 ) b , \] so \(g = a b - a - b + 1\) Cf. (III,Ex. 5.6). Now we come to the Riemann-Roch theorem. For any divisor \(D\) on the surface \(X\) ,we let \(l ( D ) = \dim _ { k } H ^ { 0 } ( X , { \mathcal { L } } ( D ) )\) . Thus \(l ( D ) = \mathrm { d i m } \left| D \right| + 1\) ,where \(| D |\) is the complete linear system of \(D\) . We define the superabundance \(s ( D )\) to be dim \(H ^ { 1 } ( X , { \mathcal { L } } ( D ) )\) .
Not formalized. none; no complete checked declaration under strict bundle semantics — As of 2026-09-06, no checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: If \(C\) is a curve of type \(^ { ( a , b ) }\) on the quadric surface, then \(C + K\) has type \(( \not { a } \ : - \ : 2 , \ : b \ : - \ : 2 )\) ,so \[ 2 g \ : - \ : 2 \ : = \ : a ( b \ : - \ : 2 ) \ : + \ : ( a \ : - \ : 2 ) b , \] so \(g = a b - a - b + 1\) Cf. (III,Ex. 5.6). Now we come to the Riemann-Roch theorem. For any divisor \(D\) on the surface \(X\) ,we let \(l ( D ) = \dim _ { k } H ^ { 0 } ( X , { \mathcal { L } } ( D ) )\) . Thus \(l ( D ) = \mathrm { d i m } \left\| D \right\| + 1\) ,where \(\| D \|\) is the complete linear system of \(D\) . We define the superabundance \(s ( D )\) to be dim \(H ^ { 1 } ( X , { \mathcal { L } } ( D ) )\) . Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, an incomplete proof, or a proper subset as the route for this ID.
Theorem 1.6
If H is ample and D·H=0, then D^2≤0; equality holds exactly when D is numerically equivalent to zero.
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked surface Hodge-index theorem owns the negative-definiteness/equality criterion in this row.
Remark 1.6.1
There is another formula,which is sometimes considered to be part of the Riemann-Roch theorem, namely \[ 1 2 ( 1 + p _ { a } ) = K ^ { 2 } + c _ { 2 } , \] where \(c _ { 2 }\) is the second Chern class of the tangent sheaf of \(X\) . This is a consequence of the generalized Grothendieck-Hirzebruch Riemann-Roch theorem (App. A, 4.1.2). As applications of the Riemann-Roch theorem, we will prove the Hodge index theorem and Nakai’s criterion for an ample divisor.
Not formalized. none; no complete checked declaration under strict bundle semantics — As of 2026-09-06, no checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: There is another formula,which is sometimes considered to be part of the Riemann-Roch theorem, namely \[ 1 2 ( 1 + p _ { a } ) = K ^ { 2 } + c _ { 2 } , \] where \(c _ { 2 }\) is the second Chern class of the tangent sheaf of \(X\) . This is a consequence of the generalized Grothendieck-Hirzebruch Riemann-Roch theorem (App. A, 4.1.2). As applications of the Riemann-Roch theorem, we will prove the Hodge index theorem and Nakai’s criterion for an ample divisor. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, an incomplete proof, or a proper subset as the route for this ID.
Remark 1.6.2
In the following,note that if we fix a very ample divisor \(H\) on a surface \(X\) ,then for any curve \(C\) on \(X\) , the intersection number \(C . H\) is just equal to the degree of \(C\) in the projective embedding determined by \(H\) (Ex.1.2). In particular, it is positive. More generally,having fixed an ample divisor \(H\) on \(X\) , the number \(C . H\) plays a role similar to the degree of a divisor on a curve.
Not formalized. none; no complete checked declaration under strict bundle semantics — As of 2026-09-06, no checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: In the following,note that if we fix a very ample divisor \(H\) on a surface \(X\) ,then for any curve \(C\) on \(X\) , the intersection number \(C . H\) is just equal to the degree of \(C\) in the projective embedding determined by \(H\) (Ex.1.2). In particular, it is positive. More generally,having fixed an ample divisor \(H\) on \(X\) , the number \(C . H\) plays a role similar to the degree of a divisor on a curve. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, an incomplete proof, or a proper subset as the route for this ID.
Lemma 1.7
Let \(H\) be an ample divisor on the surface \(X\) . Then there is an integer \(n _ { 0 }\) such that for any divisor \(D\) ,if \(D . H > n _ { 0 }\) ,then \(H ^ { 2 } ( X , { \mathcal { L } } ( D ) ) = 0\)
Not formalized. none; no complete checked declaration under strict bundle semantics — As of 2026-09-06, no checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: Let \(H\) be an ample divisor on the surface \(X\) . Then there is an integer \(n _ { 0 }\) such that for any divisor \(D\) ,if \(D . H > n _ { 0 }\) ,then \(H ^ { 2 } ( X , { \mathcal { L } } ( D ) ) = 0\) Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, an incomplete proof, or a proper subset as the route for this ID.
Remark 1.7.1
This result can be regarded as the analogue for surfaces of the result that says on a curve \(X\) , there is an integer \(n _ { 0 }\) (namely \(2 g _ { X } \mathrm { ~ - ~ } 2 )\) such that if deg \(D > n _ { 0 }\) ,then \(H ^ { 1 } ( X , { \mathcal { L } } ( D ) ) = 0\) (IV, 1.3.4).
Not formalized. none; no complete checked declaration under strict bundle semantics — As of 2026-09-06, no checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: This result can be regarded as the analogue for surfaces of the result that says on a curve \(X\) , there is an integer \(n _ { 0 }\) (namely \(2 g _ { X } \mathrm { ~ - ~ } 2 )\) such that if deg \(D > n _ { 0 }\) ,then \(H ^ { 1 } ( X , { \mathcal { L } } ( D ) ) = 0\) (IV, 1.3.4). Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, an incomplete proof, or a proper subset as the route for this ID.
Corollary 1.8
Let \(H\) be an ample divisor on \(X\) ,and let \(D\) be a divisor such that \(D . H > 0\) and \(D ^ { 2 } > 0\) Then for all \(n \gg 0 , n D\) is linearly equivalent to an effective divisor.
Not formalized. none; no complete checked declaration under strict bundle semantics — As of 2026-09-06, no checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: Let \(H\) be an ample divisor on \(X\) ,and let \(D\) be a divisor such that \(D . H > 0\) and \(D ^ { 2 } > 0\) Then for all \(n \gg 0 , n D\) is linearly equivalent to an effective divisor. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, an incomplete proof, or a proper subset as the route for this ID.
Definition
A divisor \(D\) on a surface \(X\) is numerically equivalent to zero, written \(D \equiv 0\) if \(D . E = 0\) for all divisors \(E\) We say \(D\) and \(E\) are numerically equivalent,written \(D \equiv E\) ,if \(D - E \equiv 0\)
Not formalized. none; no complete checked declaration under strict bundle semantics — Numerical equivalence here is defined through the surface intersection pairing, which is not implemented in the checked corpus; generic equivalence/order infrastructure is not a route.
Theorem 1.9
(Hodge Index Theorem). Let \(H\) be an ample divisor on the surface \(X\) ，and suppose that \(D\) is a divisor, \(D \not \equiv 0\) with \(D . H = 0\) Then \(D ^ { 2 } < 0\)
Not formalized. none; no complete checked declaration under strict bundle semantics — As of 2026-09-06, no checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: (Hodge Index Theorem). Let \(H\) be an ample divisor on the surface \(X\) ，and suppose that \(D\) is a divisor, \(D \not \equiv 0\) with \(D . H = 0\) Then \(D ^ { 2 } < 0\) Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, an incomplete proof, or a proper subset as the route for this ID.
Remark 1.9.1
The Hodge index theorem says that after passing to Num(X) and tensoring with R, the intersection form is nondegenerate of signature (1,ρ−1), where ρ=rank Num(X).
Not formalized. none; no complete checked declaration under strict bundle semantics — As of 2026-09-06, no checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: The Hodge index theorem says that after passing to Num(X) and tensoring with R, the intersection form is nondegenerate of signature (1,ρ−1), where ρ=rank Num(X). Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, an incomplete proof, or a proper subset as the route for this ID.
Example 1.9.2
On the quadric surface X (1.4.3) we can take H of type (1,1) and \(D\) of type \(( 1 , - 1 )\) . Then \(H ^ { 2 } = 2 , H . D = 0 , D ^ { 2 } = - 2\) and \(D , H\) form a basis of Pic \(X\) . In this case the only divisor numerically equivalent to O is 0, so Pic \(X = \mathsf { N u m } \ X\) . The pairing on Num \(X \odot _ { \cdot } \mathbf { R }\) is diagonalized by taking the basis \(( 1 / \sqrt { 2 } ) H , ( 1 / \sqrt { 2 } ) D\)
Not formalized. none; no complete checked declaration under strict bundle semantics — As of 2026-09-06, no checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: On the quadric surface X (1.4.3) we can take H of type (1,1) and \(D\) of type \(( 1 , - 1 )\) . Then \(H ^ { 2 } = 2 , H . D = 0 , D ^ { 2 } = - 2\) and \(D , H\) form a basis of Pic \(X\) . In this case the only divisor numerically equivalent to O is 0, so Pic \(X = \mathsf { N u m } \ X\) . The pairing on Num \(X \odot _ { \cdot } \mathbf { R }\) is diagonalized by taking the basis \(( 1 / \sqrt { 2 } ) H , ( 1 / \sqrt { 2 } ) D\) Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, an incomplete proof, or a proper subset as the route for this ID.
Theorem 1.10
(Nakai-Moishezon Criterion). \(A\) divisor \(D\) on the surface \(X\) is ample if and only if \(D ^ { 2 } > 0\) and \(D . C > 0\) for all irreducible curves \(C\) in \(X\)
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked Nakai–Moishezon criterion for surfaces was found in P, H, open Mathlib work, or the external Lean projects checked.
Example 1.10.1
On a smooth quadric, a divisor of type (a,b) is ample exactly when a>0 and b>0. Hartshorne contrasts this with Mumford examples showing that D·C>0 for every irreducible curve need not imply ampleness when D²=0.
Not formalized. none; no complete checked declaration under strict bundle semantics — As of 2026-09-06, no checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: On a smooth quadric, a divisor of type (a,b) is ample exactly when a>0 and b>0. Hartshorne contrasts this with Mumford examples showing that D·C>0 for every irreducible curve need not imply ampleness when D²=0. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, an incomplete proof, or a proper subset as the route for this ID.
Definition: A geometrically ruled surface is a nonsingular projective surface X with a…
A geometrically ruled surface is a nonsingular projective surface X with a surjective morphism π:X→C to a nonsingular curve, all fibres isomorphic to P¹, and admitting a section.
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked geometrically-ruled-surface structure with P¹ fibres and a section was found.
Example 2.0.1
Every ruled surface π:X→C is isomorphic over C to P(E) for a rank-two locally free sheaf E on C.
Not formalized. none; no complete checked declaration under strict bundle semantics — Mathlib has Proj/projective-spectrum machinery but no checked projective-bundle construction P(E) for a rank-two locally free sheaf on a curve, so the ruled-surface representation theorem is not realized.
Lemma 2.1
Let \(\pi { \colon } X \to C\) be a ruled surface, let \(D\) be a divisor on \(X\) ，and suppose that \(D . f = n \geqslant 0\) where \(f\) is a fibre of \(\pi\) .Then \(\pi _ { * } { \mathcal { L } } ( D )\) is \(a\) locally free sheaf of rank \(n + 1\) on \(C\) . In particular, \(\pi _ { * } \mathcal { C } _ { X } = \mathcal { C } _ { C }\)
Not formalized. none; no complete checked declaration under strict bundle semantics — As of 2026-09-06, no checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: Let \(\pi { \colon } X \to C\) be a ruled surface, let \(D\) be a divisor on \(X\) ，and suppose that \(D . f = n \geqslant 0\) where \(f\) is a fibre of \(\pi\) .Then \(\pi _ { * } { \mathcal { L } } ( D )\) is \(a\) locally free sheaf of rank \(n + 1\) on \(C\) . In particular, \(\pi _ { * } \mathcal { C } _ { X } = \mathcal { C } _ { C }\) Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, an incomplete proof, or a proper subset as the route for this ID.
Proposition 2.2
If π:X→C is ruled, then X≅P(E) over C for a rank-two locally free sheaf E. Conversely every P(E) is ruled, and P(E)≅P(E′) over C exactly when E′≅E⊗L for some invertible sheaf L on C.
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked P(E) ruled-surface classification or twist-isomorphism criterion was found.
Remark 2.2.1
A surface \(X\) is called a birationally ruled surface if it is birationally equivalent to C × P1 for some curve C. (This includes the rational surfaces, because P² is birational to Pl × P1.) We see from (2.2) that every ruled surface is birationally ruled.
Not formalized. none; no complete checked declaration under strict bundle semantics — Pinned Mathlib defines scheme birationality, but no checked ruled-surface interface or theorem that every ruled surface is birational to C×P¹ closes the whole row.
Proposition 2.3
For a ruled surface X=P(E), the class of a fibre f satisfies f^2=0 and any section meets f once; intersection numbers reduce divisor calculations to a section and fibre.
Not formalized. none; no complete checked declaration under strict bundle semantics — As of 2026-09-06, no checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: For a ruled surface X=P(E), the class of a fibre f satisfies f^2=0 and any section meets f once; intersection numbers reduce divisor calculations to a section and fibre. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, an incomplete proof, or a proper subset as the route for this ID.
Lemma 2.4
Let \(D\) be a divisor on the ruled surface \(X\) ，and assume that \(D . f \geqslant 0\) Then \(R ^ { i } \pi _ { * } \mathcal { L } ( D ) = 0\) for \(i > 0\) ; and for all \(i\) \[ H ^ { i } ( X , { \mathcal { L } } ( D ) ) \cong H ^ { i } ( C , \pi _ { * } { \mathcal { L } } ( D ) ) . \]
Not formalized. none; no complete checked declaration under strict bundle semantics — As of 2026-09-06, no checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: Let \(D\) be a divisor on the ruled surface \(X\) ，and assume that \(D . f \geqslant 0\) Then \(R ^ { i } \pi _ { * } \mathcal { L } ( D ) = 0\) for \(i > 0\) ; and for all \(i\) \[ H ^ { i } ( X , { \mathcal { L } } ( D ) ) \cong H ^ { i } ( C , \pi _ { * } { \mathcal { L } } ( D ) ) . \] Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, an incomplete proof, or a proper subset as the route for this ID.
Corollary 2.5
If the genus of \(C\) is \(g\) ,then $p _ { a } ( X ) = - g , p _ { g } ( X ) = 0 , q ( X ) = g $
Not formalized. none; no complete checked declaration under strict bundle semantics — As of 2026-09-06, no checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: If the genus of \(C\) is \(g\) ,then $p _ { a } ( X ) = - g , p _ { g } ( X ) = 0 , q ( X ) = g $ Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, an incomplete proof, or a proper subset as the route for this ID.
Proposition 2.6
For X=P(E), sections σ:C→X are in bijection with quotient line bundles E↠L; the corresponding section satisfies σ^*O_X(1)≅L, and its divisor class is determined by the kernel and quotient.
Not formalized. none; no complete checked declaration under strict bundle semantics — As of 2026-09-06, no checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: For X=P(E), sections σ:C→X are in bijection with quotient line bundles E↠L; the corresponding section satisfies σ^*O_X(1)≅L, and its divisor class is determined by the kernel and quotient. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, an incomplete proof, or a proper subset as the route for this ID.
Corollary 2.7
Any locally free sheaf \(\pmb { \delta } ^ { \mathcal { O } }\) of rank 2 on a curve \(C\) is an extension of invertible sheaves.
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked theorem that every rank-two vector bundle on a curve is an extension of line bundles was found.
Remark 2.7.1
The same result holds for locally free sheaves of arbitrary rank (Ex. 2.3).
Not formalized. none; no complete checked declaration under strict bundle semantics — As of 2026-09-06, no checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: The same result holds for locally free sheaves of arbitrary rank (Ex. 2.3). Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, an incomplete proof, or a proper subset as the route for this ID.
Proposition 2.8
Every ruled surface can be written P(E) with E normalized: H^0(E)≠0 but H^0(E⊗L)=0 for all line bundles L of negative degree. Then e=−deg E is an invariant of X, and there is a distinguished section C_0 with O_X(C_0)≅O_X(1).
Not formalized. none; no complete checked declaration under strict bundle semantics — As of 2026-09-06, no checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: Every ruled surface can be written P(E) with E normalized: H^0(E)≠0 but H^0(E⊗L)=0 for all line bundles L of negative degree. Then e=−deg E is an invariant of X, and there is a distinguished section C_0 with O_X(C_0)≅O_X(1). Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, an incomplete proof, or a proper subset as the route for this ID.
Notation 2.8.1
Fix X=P(E) over a genus-g curve C with E normalized; write e=−deg E, choose the distinguished section C_0 with O_X(C_0)≅O_{P(E)}(1), and write pullbacks of divisors from C as bf. Then Pic X is generated by C_0 and π^*Pic C, while Num X is generated by C_0 and f.
Not formalized. none; no complete checked declaration under strict bundle semantics — As of 2026-09-06, no checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: Fix X=P(E) over a genus-g curve C with E normalized; write e=−deg E, choose the distinguished section C_0 with O_X(C_0)≅O_{P(E)}(1), and write pullbacks of divisors from C as bf. Then Pic X is generated by C_0 and π^*Pic C, while Num X is generated by C_0 and f. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, an incomplete proof, or a proper subset as the route for this ID.
Proposition 2.9
If \(D\) is any section of \(X\) ,corresponding to a surjection $ $ \(\mathcal { L } 0\) andif \({ \mathcal { L } } = { \mathcal { L } } ( { \mathfrak { d } } )\) for some divisor \(\mathfrak { d }\) on \(C\) then deg \(\mathfrak { d } = C _ { 0 } . D\) and \[ D \sim C _ { 0 } + ( \mathfrak { d } \mathrm { ~ - ~ } \mathfrak { e } ) f . \] In particular, we have \(C _ { 0 } ^ { 2 } = \deg { \mathfrak { e } } = - e\)
Not formalized. none; no complete checked declaration under strict bundle semantics — As of 2026-09-06, no checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: If \(D\) is any section of \(X\) ,corresponding to a surjection $ $ \(\mathcal { L } 0\) andif \({ \mathcal { L } } = { \mathcal { L } } ( { \mathfrak { d } } )\) for some divisor \(\mathfrak { d }\) on \(C\) then deg \(\mathfrak { d } = C _ { 0 } . D\) and \[ D \sim C _ { 0 } + ( \mathfrak { d } \mathrm { ~ - ~ } \mathfrak { e } ) f . \] In particular, we have \(C _ { 0 } ^ { 2 } = \deg { \mathfrak { e } } = - e\) Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, an incomplete proof, or a proper subset as the route for this ID.
Lemma 2.10
The canonical dirisor \(K\) on \(X\) is given by \[ K \sim - 2 C _ { 0 } + ( \mathfrak { t } + \mathfrak { e } ) f \] where t is the canonical divisor on \(C\)
Not formalized. none; no complete checked declaration under strict bundle semantics — As of 2026-09-06, no checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: The canonical dirisor \(K\) on \(X\) is given by \[ K \sim - 2 C _ { 0 } + ( \mathfrak { t } + \mathfrak { e } ) f \] where t is the canonical divisor on \(C\) Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, an incomplete proof, or a proper subset as the route for this ID.
Corollary 2.11
For numerical equiralence, we hare and therefore \[ \begin{array} { c } { { K \equiv - 2 C _ { 0 } + ( 2 g - 2 - e ) f } } \ { { } } \ { { K ^ { 2 } = 8 ( 1 - g ) . } } \end{array} \]
Not formalized. none; no complete checked declaration under strict bundle semantics — As of 2026-09-06, no checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: For numerical equiralence, we hare and therefore \[ \begin{array} { c } { { K \equiv - 2 C _ { 0 } + ( 2 g - 2 - e ) f } } \ { { } } \ { { K ^ { 2 } = 8 ( 1 - g ) . } } \end{array} \] Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, an incomplete proof, or a proper subset as the route for this ID.
Example 2.11.1
For any curve \(C\) ， the ruled surface \(X = C \times \mathbf { P } ^ { 1 }\) corresponds to the (normalized) locally free sheaf \(\mathcal { E } = \mathcal { O } _ { C } \oplus \mathcal { O } _ { C }\) on \(C\) In this case \(e = 0\) ,and \(C _ { 0 }\) is any fibre of the second projection.
Not formalized. none; no complete checked declaration under strict bundle semantics — As of 2026-09-06, no checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: For any curve \(C\) ， the ruled surface \(X = C \times \mathbf { P } ^ { 1 }\) corresponds to the (normalized) locally free sheaf \(\mathcal { E } = \mathcal { O } _ { C } \oplus \mathcal { O } _ { C }\) on \(C\) In this case \(e = 0\) ,and \(C _ { 0 }\) is any fibre of the second projection. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, an incomplete proof, or a proper subset as the route for this ID.
Example 2.11.2
If \(C\) is a curve of genus \(\geqslant 1\) ，and \(\mathcal { E } = \mathcal { C } _ { c } \oplus \mathcal { L }\) where deg \(\mathcal { L } = 0\) but \(\mathcal { L } \not \equiv \mathcal { C } _ { C }\) ， then there are two choices of normalized \(\mathcal { E }\) ， namely \(\boldsymbol { \mathcal { E } }\) and \(\mathcal { E } \otimes \mathcal { L } ^ { - 1 }\) .We have \(e = 0\) deg \(\textrm { \textbf { e } } = 0\) ，but e is determined only up to sign. There are exactly two choices of \(C _ { 0 }\) ,both with \(C _ { 0 } ^ { 2 } = 0\)
Not formalized. none; no complete checked declaration under strict bundle semantics — As of 2026-09-06, no checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: If \(C\) is a curve of genus \(\geqslant 1\) ，and \(\mathcal { E } = \mathcal { C } _ { c } \oplus \mathcal { L }\) where deg \(\mathcal { L } = 0\) but \(\mathcal { L } \not \equiv \mathcal { C } _ { C }\) ， then there are two choices of normalized \(\mathcal { E }\) ， namely \(\boldsymbol { \mathcal { E } }\) and \(\mathcal { E } \otimes \mathcal { L } ^ { - 1 }\) .We have \(e = 0\) deg \(\textrm { \textbf { e } } = 0\) ，but e is determined only up to sign. There are exactly two choices of \(C _ { 0 }\) ,both with \(C _ { 0 } ^ { 2 } = 0\) Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, an incomplete proof, or a proper subset as the route for this ID.
Example 2.11.3
On any curve \(C\) ,let \(\mathcal { E } = \mathcal { O } _ { C } \oplus \mathcal { L }\) with deg \(\mathcal { L } < 0\) Then the normalized \(\mathscr { E }\) is unique, \({ \mathcal { L } } = { \mathcal { L } } ( { \mathfrak { e } } )\) and e is unique. The section \(C _ { 0 }\) is unique, with \(C _ { 0 } ^ { 2 } = - e < 0\) In this case \(e = - \deg \mathcal { L } > 0\)
Not formalized. none; no complete checked declaration under strict bundle semantics — As of 2026-09-06, no checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: On any curve \(C\) ,let \(\mathcal { E } = \mathcal { O } _ { C } \oplus \mathcal { L }\) with deg \(\mathcal { L } < 0\) Then the normalized \(\mathscr { E }\) is unique, \({ \mathcal { L } } = { \mathcal { L } } ( { \mathfrak { e } } )\) and e is unique. The section \(C _ { 0 }\) is unique, with \(C _ { 0 } ^ { 2 } = - e < 0\) In this case \(e = - \deg \mathcal { L } > 0\) Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, an incomplete proof, or a proper subset as the route for this ID.
Example 2.11.4
If X_0 is the cone over a degree-d curve C⊂P^n, blowing up the vertex gives a ruled surface over C of the form P(O_C⊕O_C(−1)); the exceptional section C_0 has C_0^2=−d and the ruled invariant is e=d.
Not formalized. none; no complete checked declaration under strict bundle semantics — As of 2026-09-06, no checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: If X_0 is the cone over a degree-d curve C⊂P^n, blowing up the vertex gives a ruled surface over C of the form P(O_C⊕O_C(−1)); the exceptional section C_0 has C_0^2=−d and the ruled invariant is e=d. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, an incomplete proof, or a proper subset as the route for this ID.
Example 2.11.5
As a special case of (2.11.4), we see that \(\mathbf { P } ^ { 2 }\) with one point blown up is isomorphic to the rational ruled surface over \(\mathbf { P } ^ { 1 }\) defined by \(\mathcal { E } = \mathcal { O } \oplus \mathcal { O } ( - 1 )\) having \(e = 1\) ：
Not formalized. none; no complete checked declaration under strict bundle semantics — As of 2026-09-06, no checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: As a special case of (2.11.4), we see that \(\mathbf { P } ^ { 2 }\) with one point blown up is isomorphic to the rational ruled surface over \(\mathbf { P } ^ { 1 }\) defined by \(\mathcal { E } = \mathcal { O } \oplus \mathcal { O } ( - 1 )\) having \(e = 1\) ： Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, an incomplete proof, or a proper subset as the route for this ID.
Example 2.11.6
On an elliptic curve C, a nontrivial extension 0→O_C→E→L(P)→0 with deg L(P)=1 is unique up to isomorphism after scaling the extension class; E is normalized and yields a ruled surface with invariant e=−1.
Not formalized. none; no complete checked declaration under strict bundle semantics — As of 2026-09-06, no checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: On an elliptic curve C, a nontrivial extension 0→O_C→E→L(P)→0 with deg L(P)=1 is unique up to isomorphism after scaling the extension class; E is normalized and yields a ruled surface with invariant e=−1. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, an incomplete proof, or a proper subset as the route for this ID.
Theorem 2.12
Let \(X\) be a ruled surface orer the curve \(C\) of genus g,determined \(b \mathbf { \eta } _ { \mathrm { . } } ^ { \cdot }\) a normalized locally free sheaf \(\boldsymbol { \mathcal { E } }\) ， (a）If \(\boldsymbol { \mathcal { E } }\) is decomposable (i.e., a direct sum of two inrertible sheares) then \(\xi \cong \mathcal { O } _ { C } \oplus \mathcal { L }\) for some \(\mathcal { L }\) with deg \(\mathcal { L } \leqslant 0\) Therefore \(e \geqslant 0\) Al values of \(e \geqslant 0\) are possible. (b)If \(\mathcal { E }\) is indecomposable,then \(- 2 g \leqslant e \leqslant 2 g - 2\) \(. I n\) fact,there are eren stronger restrictions on \(e\) (Ex. 2.5).)
Not formalized. none; no complete checked declaration under strict bundle semantics — As of 2026-09-06, no checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: Let \(X\) be a ruled surface orer the curve \(C\) of genus g,determined \(b \mathbf { \eta } _ { \mathrm { . } } ^ { \cdot }\) a normalized locally free sheaf \(\boldsymbol { \mathcal { E } }\) ， (a）If \(\boldsymbol { \mathcal { E } }\) is decomposable (i.e., a direct sum of two inrertible sheares) then \(\xi \cong \mathcal { O } _ { C } \oplus \mathcal { L }\) for some \(\mathcal { L }\) with deg \(\mathcal { L } \leqslant 0\) Therefore \(e \geqslant 0\) Al values of \(e \geqslant 0\) are possible. (b)If \(\mathcal { E }\) is indecomposable,then \(- 2 g \leqslant e \leqslant 2 g - 2\) \(. I n\) fact,there are eren stronger restrictions on \(e\) (Ex. 2.5).) Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, an incomplete proof, or a proper subset as the route for this ID.
Corollary 2.13
If \(g = 0\) then \(e \geqslant 0\) ,and for each \(e \geqslant 0\) there is exactly one rational ruled surface with invariant \(e\) ，given by \(\xi ~ = ~ \mathcal { C } \oplus \mathcal { C } ( - e )\) orer \(C = { \bf \delta p } ^ { 1 }\) ，
Not formalized. none; no complete checked declaration under strict bundle semantics — As of 2026-09-06, no checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: If \(g = 0\) then \(e \geqslant 0\) ,and for each \(e \geqslant 0\) there is exactly one rational ruled surface with invariant \(e\) ，given by \(\xi ~ = ~ \mathcal { C } \oplus \mathcal { C } ( - e )\) orer \(C = { \bf \delta p } ^ { 1 }\) ， Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, an incomplete proof, or a proper subset as the route for this ID.
Corollary 2.14
Erery locally free sheaf \(\mathcal { E }\) of rank 2 on \(\mathbf { P } ^ { 1 }\) is decomposable.
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked Birkhoff–Grothendieck splitting theorem for rank-two bundles on P¹ was found.
Theorem 2.15
If \(X\) is a ruled surface over an elliptic curve \(C\) ，corresponding to an indecomposable \(\mathcal { E }\) ，then \(e = 0\) 0r \(^ { - 1 }\) ,and there is exactly one such ruled surface over \(C\) for each of these two ralues of \(e\)
Not formalized. none; no complete checked declaration under strict bundle semantics — As of 2026-09-06, no checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: If \(X\) is a ruled surface over an elliptic curve \(C\) ，corresponding to an indecomposable \(\mathcal { E }\) ，then \(e = 0\) 0r \(^ { - 1 }\) ,and there is exactly one such ruled surface over \(C\) for each of these two ralues of \(e\) Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, an incomplete proof, or a proper subset as the route for this ID.
Corollary 2.16
For every integer n on an elliptic curve C, isomorphism classes of indecomposable rank-two locally free sheaves of degree n are naturally parametrized by the points of C.
Not formalized. none; no complete checked declaration under strict bundle semantics — As of 2026-09-06, no checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: For every integer n on an elliptic curve C, isomorphism classes of indecomposable rank-two locally free sheaves of degree n are naturally parametrized by the points of C. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, an incomplete proof, or a proper subset as the route for this ID.
Remark 2.16.1
For fixed rank and degree, vector bundles on a curve occur in moduli. In genus zero every bundle splits; in genus one Atiyah classifies indecomposables; for genus at least two stability becomes essential and leads to moduli spaces of stable bundles.
Not formalized. none; no complete checked declaration under strict bundle semantics — As of 2026-09-06, no checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: For fixed rank and degree, vector bundles on a curve occur in moduli. In genus zero every bundle splits; in genus one Atiyah classifies indecomposables; for genus at least two stability becomes essential and leads to moduli spaces of stable bundles. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, an incomplete proof, or a proper subset as the route for this ID.
Theorem 2.17
Let \(X _ { e }\) ,for any \(e \geqslant 0\) ,be the rational ruled surface defined by \(\xi ^ { \epsilon } = \mathcal { O } \oplus \mathcal { O } ( - e )\) on \(C = \mathbf { P } ^ { 1 }\) (2.13). Then: (a) there is a section \(D \sim C _ { 0 } +\) nf if and only if \(n = 0\) or \(n \geqslant e\) In particular,there is a section \(C _ { 1 } \sim C _ { 0 } + e f\) with \(C _ { 0 } \cap C _ { 1 } = \emptyset\) and \(C _ { 1 } ^ { 2 } = e\) ：， (b) the linear system \(\left| C _ { 0 } + n f \right|\) is base-point-free if and only if \(n \geqslant e\) ： (c) the linear system \(\left| C _ { 0 } + n f \right|\) is very ample if and only if \(n > e\)
Not formalized. none; no complete checked declaration under strict bundle semantics — As of 2026-09-06, no checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: Let \(X _ { e }\) ,for any \(e \geqslant 0\) ,be the rational ruled surface defined by \(\xi ^ { \epsilon } = \mathcal { O } \oplus \mathcal { O } ( - e )\) on \(C = \mathbf { P } ^ { 1 }\) (2.13). Then: (a) there is a section \(D \sim C _ { 0 } +\) nf if and only if \(n = 0\) or \(n \geqslant e\) In particular,there is a section \(C _ { 1 } \sim C _ { 0 } + e f\) with \(C _ { 0 } \cap C _ { 1 } = \emptyset\) and \(C _ { 1 } ^ { 2 } = e\) ：， (b) the linear system \(\left\| C _ { 0 } + n f \right\|\) is base-point-free if and only if \(n \geqslant e\) ： (c) the linear system \(\left\| C _ { 0 } + n f \right\|\) is very ample if and only if \(n > e\) Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, an incomplete proof, or a proper subset as the route for this ID.
Corollary 2.18
On the rational ruled surface X_e, D=aC_0+bf is ample (equivalently very ample) exactly when a>0 and b>ae. Hartshorne also lists the exceptional boundary cases in which |D| contains an irreducible nonsingular curve.
Not formalized. none; no complete checked declaration under strict bundle semantics — As of 2026-09-06, no checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: On the rational ruled surface X_e, D=aC_0+bf is ample (equivalently very ample) exactly when a>0 and b>ae. Hartshorne also lists the exceptional boundary cases in which |D| contains an irreducible nonsingular curve. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, an incomplete proof, or a proper subset as the route for this ID.
Remark 2.18.1
For e=0 the rational ruled surface X_0 is the smooth quadric; the ruled-surface calculations recover the earlier results on curves and divisors on P¹×P¹.
Not formalized. none; no complete checked declaration under strict bundle semantics — As of 2026-09-06, no checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: For e=0 the rational ruled surface X_0 is the smooth quadric; the ruled-surface calculations recover the earlier results on curves and divisors on P¹×P¹. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, an incomplete proof, or a proper subset as the route for this ID.
Corollary 2.19
For every \(\begin{array} { r } { \eta > \ell \geqslant 0 } \end{array}\) ,there is an embedding of the rational ruled surface \(X _ { e }\) as a rational scroll of degree \(d = 2 n - e\) in \(\mathbf { P } ^ { d + 1 }\) (A scroll is a ruled surface embedded in \(\mathbf { P } ^ { N }\) in such a way that all the fibres \(f\) have degree 1.)
Not formalized. none; no complete checked declaration under strict bundle semantics — As of 2026-09-06, no checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: For every \(\begin{array} { r } { \eta > \ell \geqslant 0 } \end{array}\) ,there is an embedding of the rational ruled surface \(X _ { e }\) as a rational scroll of degree \(d = 2 n - e\) in \(\mathbf { P } ^ { d + 1 }\) (A scroll is a ruled surface embedded in \(\mathbf { P } ^ { N }\) in such a way that all the fibres \(f\) have degree 1.) Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, an incomplete proof, or a proper subset as the route for this ID.
Example 2.19.1
The embeddings from suitable divisors on X_e give the classical rational normal scrolls: X_0 with n=1 is the smooth quadric in P³, X_1 with n=2 is the cubic scroll in P⁴, and degree-four scrolls in P⁵ arise from e=0 or e=2.
Not formalized. none; no complete checked declaration under strict bundle semantics — As of 2026-09-06, no checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: The embeddings from suitable divisors on X_e give the classical rational normal scrolls: X_0 with n=1 is the smooth quadric in P³, X_1 with n=2 is the cubic scroll in P⁴, and degree-four scrolls in P⁵ arise from e=0 or e=2. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, an incomplete proof, or a proper subset as the route for this ID.
Remark 2.19.2
Every smooth nondegenerate surface of minimal degree in P^{d+1} is a rational normal scroll, except for the plane and the Veronese surface; Hartshorne uses this as context for the ruled-surface ampleness problem.
Not formalized. none; no complete checked declaration under strict bundle semantics — As of 2026-09-06, no checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: Every smooth nondegenerate surface of minimal degree in P^{d+1} is a rational normal scroll, except for the plane and the Veronese surface; Hartshorne uses this as context for the ruled-surface ampleness problem. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, an incomplete proof, or a proper subset as the route for this ID.
Proposition 2.20
Let \(X\) be a ruled surface over a curve \(C\) ,with invariant \(e \geqslant 0\) (a)If \(Y \equiv a C _ { 0 } + i\) bf isan irreducible curve \(\neq C _ { 0 }\) ,f,then \(a > 0 , b \geqslant a e\) (b) \(A\) divisor \(D \equiv a C _ { 0 } + b f\) is ample if and only if \(a > 0 , b > a e\)
Not formalized. none; no complete checked declaration under strict bundle semantics — As of 2026-09-06, no checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: Let \(X\) be a ruled surface over a curve \(C\) ,with invariant \(e \geqslant 0\) (a)If \(Y \equiv a C _ { 0 } + i\) bf isan irreducible curve \(\neq C _ { 0 }\) ,f,then \(a > 0 , b \geqslant a e\) (b) \(A\) divisor \(D \equiv a C _ { 0 } + b f\) is ample if and only if \(a > 0 , b > a e\) Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, an incomplete proof, or a proper subset as the route for this ID.
Proposition 2.21
Let \(X\) be a ruled surface over a curve \(C\) of genus \(g\) ,with invariant \(e < 0\) ,and assume furthermore either char \(k = 0\) or \(g \leqslant 1\) ： (a）If \(Y \equiv a C _ { 0 } + b f\) is an irreducible curve \(\neq C _ { 0 } , f ;\) theneither \(a = 1\) \(b \geqslant 0\) or \(a \geqslant 2\) \(b \geqslant { \frac { 1 } { 2 } } a e\) (b） \(A\) divisor \(D \equiv a C _ { 0 } + b f\) is ampleif and only if \(a > 0 , b > { \frac { 1 } { 2 } } a e\)
Not formalized. none; no complete checked declaration under strict bundle semantics — As of 2026-09-06, no checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: Let \(X\) be a ruled surface over a curve \(C\) of genus \(g\) ,with invariant \(e < 0\) ,and assume furthermore either char \(k = 0\) or \(g \leqslant 1\) ： (a）If \(Y \equiv a C _ { 0 } + b f\) is an irreducible curve \(\neq C _ { 0 } , f ;\) theneither \(a = 1\) \(b \geqslant 0\) or \(a \geqslant 2\) \(b \geqslant { \frac { 1 } { 2 } } a e\) (b） \(A\) divisor \(D \equiv a C _ { 0 } + b f\) is ampleif and only if \(a > 0 , b > { \frac { 1 } { 2 } } a e\) Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, an incomplete proof, or a proper subset as the route for this ID.
Remark 2.21.1
In the remaining case \(e < 0\) ,char \(k = p > 0 , g \geqslant 2\) ,we cannot get necessary and sufficient conditions for \(D\) to be ample, but it is possible to get some partial results (Ex. 2.14) and (Ex.2.15).
Not formalized. none; no complete checked declaration under strict bundle semantics — As of 2026-09-06, no checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: In the remaining case \(e < 0\) ,char \(k = p > 0 , g \geqslant 2\) ,we cannot get necessary and sufficient conditions for \(D\) to be ample, but it is possible to get some partial results (Ex. 2.14) and (Ex.2.15). Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, an incomplete proof, or a proper subset as the route for this ID.
Remark 2.22.2
For ruled surfaces over curves of positive genus, very ampleness is subtler than in the rational case and is not determined solely by the numerical equivalence class.
Not formalized. none; no complete checked declaration under strict bundle semantics — As of 2026-09-06, no checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: For ruled surfaces over curves of positive genus, very ampleness is subtler than in the rational case and is not determined solely by the numerical equivalence class. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, an incomplete proof, or a proper subset as the route for this ID.
Definition — monoidal transformation of a surface
A monoidal transformation is the blowup of a nonsingular surface at one closed point.
Not formalized. none; no complete checked declaration under strict bundle semantics — Pinned Mathlib has RingTheory/ReesAlgebra.lean, whose module documentation says the Rees algebra will be useful for defining blowups in the future, but it has no blowup-scheme construction. The already-promoted C02 U239 blowup-by-Proj row is likewise unmatched, so the point-blowup definition is not promoted here.
Convention — exceptional curve of a point blowup
For π:X~→X the blowup at P, E=π^{-1}(P) is the exceptional curve and π is an isomorphism away from E and P.
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked point-blowup scheme exists in P/H; hence there is no checked exceptional divisor with the stated complement-isomorphism package. Rees-algebra or generic Proj data is a proper subset only.
Proposition 3.1
For the blowup π:X~→X of a point on a nonsingular projective surface, X~ is again nonsingular projective, the exceptional curve E≅P^1, and E^2=−1.
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked theorem constructs the blowup of a smooth projective surface at a point and proves smoothness/projectivity, E≅P¹, and E²=-1.
Remark 3.1.1
There is a converse to this result, which we will prove later (5.7),namely,any curve E ≦ Pl in a surface X’,with E² = -1, is obtained as the exceptional curve by a monoidal transformation from some other surface \(X\) ：
Not formalized. none; no complete checked declaration under strict bundle semantics — As of 2026-09-06, no checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: There is a converse to this result, which we will prove later (5.7),namely,any curve E ≦ Pl in a surface X’,with E² = -1, is obtained as the exceptional curve by a monoidal transformation from some other surface \(X\) ： Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, an incomplete proof, or a proper subset as the route for this ID.
Proposition 3.2
For the blowup π:X~→X at a point with exceptional E, Pic(X~)≅πPic(X)⊕Z[E]. The intersection form is determined by (π^C·πD)=C·D, π^C·E=0, and E^2=−1.
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked point-blowup Picard decomposition or intersection-form transformation theorem was found.
Proposition 3.3
The canonical divisor of \(\tilde { X }\) is given by \(K _ { \tilde { x } } = \pi ^ { * } K _ { x } + E\) Therefore \(K _ { \tilde { X } } ^ { 2 } = K _ { X } ^ { 2 } - 1\) ，
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked canonical-divisor transformation formula under a surface point blowup was found.
Remark 3.3.1
Thus the invariant \(K ^ { 2 }\) of a surface is not a birational invariant. For a specific example,we have \(K ^ { 2 }\) of \(\mathbf { P } ^ { 2 }\) is 9 (1.4.4), \(K ^ { 2 }\) of the rational ruled surface \(X _ { 1 }\) is 8 (2.11), and \(X _ { 1 }\) is isomorphic to a monoidal transformation of \(\mathbf { P } ^ { 2 }\) (2.11.5). Next we want to show that the arithmetic genus \(p _ { a }\) is preserved by a monoidal transformation. For that, we must compare the cohomology of the structure sheaves on \(X\) and \(\tilde { X }\) .We will use the theorem on formal functions (III,11.1tcute \(R ^ { \iota } \pi _ { * } \mathcal { C } _ { \tilde { X } }\) ，
Not formalized. none; no complete checked declaration under strict bundle semantics — As of 2026-09-06, no checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: Thus the invariant \(K ^ { 2 }\) of a surface is not a birational invariant. For a specific example,we have \(K ^ { 2 }\) of \(\mathbf { P } ^ { 2 }\) is 9 (1.4.4), \(K ^ { 2 }\) of the rational ruled surface \(X _ { 1 }\) is 8 (2.11), and \(X _ { 1 }\) is isomorphic to a monoidal transformation of \(\mathbf { P } ^ { 2 }\) (2.11.5). Next we want to show that the arithmetic genus \(p _ { a }\) is preserved by a monoidal transformation. For that, we must compare the cohomology of the structure sheaves on \(X\) and \(\tilde { X }\) .We will use the theorem on formal functions (III,11.1tcute \(R ^ { \iota } \pi _ { * } \mathcal { C } _ { \tilde { X } }\) ， Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, an incomplete proof, or a proper subset as the route for this ID.
Proposition 3.4
For the blowup π:X~→X at a point with exceptional E, K_{X~}∼π^*K_X+E.
Not formalized. none; no complete checked declaration under strict bundle semantics — As of 2026-09-06, no checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: For the blowup π:X~→X at a point with exceptional E, K_{X~}∼π^*K_X+E. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, an incomplete proof, or a proper subset as the route for this ID.
Corollary 3.5
Let \(\pi { \mathrel { : } } { \tilde { X } } \to X\) be a monoidal transformation. Then \(p _ { a } ( X ) =\) \(p _ { a } ( { \tilde { X } } )\) ：
Not formalized. none; no complete checked declaration under strict bundle semantics — As of 2026-09-06, no checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: Let \(\pi { \mathrel { : } } { \tilde { X } } \to X\) be a monoidal transformation. Then \(p _ { a } ( X ) =\) \(p _ { a } ( { \tilde { X } } )\) ： Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, an incomplete proof, or a proper subset as the route for this ID.
Remark 3.5.1
A point blowup preserves irregularity q=h^1(O_X) and geometric genus p_g=h^2(O_X). For a curve C through the center, the strict transform is the blowup/closure transform used in the subsequent multiplicity formulas.
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked point-blowup theorem preserves irregularity/geometric genus and supplies the strict-transform construction in Hartshorne’s surface setting.
Definition: Let \(C\) be an effective Cartier divisor on the surface \(X\) ,and let \(f\) be a…
Let \(C\) be an effective Cartier divisor on the surface \(X\) ,and let \(f\) be a local equation for C at the point P. Then we define the multiplicity of C at P, denoted by μp(C), to be the largest integer r such that f∈ mp, where \(\mathfrak { m } _ { P } \subseteq { \mathcal { O } } _ { P , X }\) is the maximal ideal.
Not formalized. none; no complete checked declaration under strict bundle semantics — As of 2026-09-06, no checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: Let \(C\) be an effective Cartier divisor on the surface \(X\) ,and let \(f\) be a local equation for C at the point P. Then we define the multiplicity of C at P, denoted by μp(C), to be the largest integer r such that f∈ mp, where \(\mathfrak { m } _ { P } \subseteq { \mathcal { O } } _ { P , X }\) is the maximal ideal. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, an incomplete proof, or a proper subset as the route for this ID.
Remark 3.5.2
For a curve C through P, its multiplicity μ_P(C) is nonnegative, is positive exactly when P∈C, and equals one exactly when C is nonsingular at P.
Not formalized. none; no complete checked declaration under strict bundle semantics — As of 2026-09-06, no checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: For a curve C through P, its multiplicity μ_P(C) is nonnegative, is positive exactly when P∈C, and equals one exactly when C is nonsingular at P. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, an incomplete proof, or a proper subset as the route for this ID.
Proposition 3.6
Repeated point blowups resolve the singularities of a curve on a nonsingular surface: after finitely many monoidal transformations, the strict transform is nonsingular.
Not formalized. none; no complete checked declaration under strict bundle semantics — As of 2026-09-06, no checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: Repeated point blowups resolve the singularities of a curve on a nonsingular surface: after finitely many monoidal transformations, the strict transform is nonsingular. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, an incomplete proof, or a proper subset as the route for this ID.
Corollary 3.7
With the same hypotheses, we hare \(\tilde { C } . E = \boldsymbol { r }\) and \(p _ { a } ( { \tilde { C } } ) =\) \(p _ { a } ( C ) \ : - \ : \frac { 1 } { 2 } r ( r ^ { } - 1 )\) ：
Not formalized. none; no complete checked declaration under strict bundle semantics — As of 2026-09-06, no checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: With the same hypotheses, we hare \(\tilde { C } . E = \boldsymbol { r }\) and \(p _ { a } ( { \tilde { C } } ) =\) \(p _ { a } ( C ) \ : - \ : \frac { 1 } { 2 } r ( r ^ { } - 1 )\) ： Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, an incomplete proof, or a proper subset as the route for this ID.
Proposition 3.8
Every irreducible curve on a nonsingular surface becomes nonsingular after finitely many point blowups with suitable centers.
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked resolution-of-a-curve-on-a-smooth-surface theorem by finitely many point blowups was found.
Remark 3.8.1
Castelnuovo contraction criterion: every exceptional curve of the first kind on a nonsingular projective surface can be contracted to a nonsingular point, inverse to a monoidal transformation.
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked Castelnuovo contraction theorem for a (-1)-curve was found.
Theorem 3.9
(Embedded Resolution of Curves in Surfaces). Let \(Y\) beany curve in the surface \(X\) .Then there exists a finite sequence of monoidal transformations \(X ^ { \prime } = X _ { n } \to X _ { n - 1 } \to . . . \to X _ { 0 } = X\) ,such that if \(f \colon X ^ { \prime } \to X\) is their composition, then the total inrerse image \(f ^ { - 1 } ( Y )\) is a dirisor with normal crossings (3.8.1).
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked embedded resolution of curves in smooth surfaces by monoidal transformations was found.
Example 3.9.1
If \(Y\) is the plane cuspidal curve \(\boldsymbol { \mathrm { J } } ^ { 2 } = \boldsymbol { x } ^ { 3 }\) , then the singularity of \(Y\) is resolved by one monoidal transformation. However, to get \(f ^ { - 1 } ( Y )\) to have normal crossings, we need three monoidal transformations (Fig. 20). Figure 20. Embedded resolution of a cusp. In the context of successive monoidal transformations, it is convenient to introduce the language of infinitely near points.
Not formalized. none; no complete checked declaration under strict bundle semantics — As of 2026-09-06, no checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: If \(Y\) is the plane cuspidal curve \(\boldsymbol { \mathrm { J } } ^ { 2 } = \boldsymbol { x } ^ { 3 }\) , then the singularity of \(Y\) is resolved by one monoidal transformation. However, to get \(f ^ { - 1 } ( Y )\) to have normal crossings, we need three monoidal transformations (Fig. 20). Figure 20. Embedded resolution of a cusp. In the context of successive monoidal transformations, it is convenient to introduce the language of infinitely near points. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, an incomplete proof, or a proper subset as the route for this ID.
Definition: Let \(X\) be a surface
Let \(X\) be a surface. Then any point on any surface \(X ^ { \prime }\) ,obtained from \(X\) by a finite succession of monoidal transformations, is called an infinitely near point of \(X\) If \(g \colon X ^ { \prime \prime } \to X ^ { \prime }\) is a further succession of monoidal transformations,and if \(Q ^ { \prime \prime } \in X ^ { \prime \prime }\) is a point in the open set where \(g\) is an isomorphism, then we identify \(\mathcal { Q } ^ { \prime \prime }\) with \(g ( Q ^ { \prime \prime } )\) as infinitely near points of \(X\) .In particular, all the ordinary points of \(X\) are included among the infinitely near points.
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked infinitely-near-point construction based on iterated surface blowups was found.
Example 3.9.2
Let \(C\) be an irreducible curve on a surface \(X\) ，with normalization \(\tilde { C }\) .Then we have \[ g ( \tilde { C } ) = p _ { a } ( C ) - \sum _ { P } \frac { 1 } { 2 } r _ { P } ( r _ { P } - 1 ) , \] where \(r _ { P }\) is the multiplicity, and the sum is taken over all singular points \(P\) of \(C\) , including infinitely near singular points. Indeed,by (3.8) we pass from \(C\) to \(\tilde { C }\) by blowing up the singular points in succession,until there are none left. Each time, by (3.7), the arithmetic genus drops by \({ \frac { 1 } { 2 } } r ( r - 1 )\)
Not formalized. none; no complete checked declaration under strict bundle semantics — As of 2026-09-06, no checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: Let \(C\) be an irreducible curve on a surface \(X\) ，with normalization \(\tilde { C }\) .Then we have \[ g ( \tilde { C } ) = p _ { a } ( C ) - \sum _ { P } \frac { 1 } { 2 } r _ { P } ( r _ { P } - 1 ) , \] where \(r _ { P }\) is the multiplicity, and the sum is taken over all singular points \(P\) of \(C\) , including infinitely near singular points. Indeed,by (3.8) we pass from \(C\) to \(\tilde { C }\) by blowing up the singular points in succession,until there are none left. Each time, by (3.7), the arithmetic genus drops by \({ \frac { 1 } { 2 } } r ( r - 1 )\) Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, an incomplete proof, or a proper subset as the route for this ID.
Example 3.9.3
In particular,working with the infinitesimal neighborhood of one point at a time, we see that the integer \(\delta _ { P }\) of (IV,Ex.1.8) can be computed as \(\sum { \textstyle \frac { 1 } { 2 } } r _ { Q } ( r _ { Q } - 1 )\) taken over all infinitely near singular points \(Q\) lying over \(P\) ,including \(P\)
Not formalized. none; no complete checked declaration under strict bundle semantics — As of 2026-09-06, no checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: In particular,working with the infinitesimal neighborhood of one point at a time, we see that the integer \(\delta _ { P }\) of (IV,Ex.1.8) can be computed as \(\sum { \textstyle \frac { 1 } { 2 } } r _ { Q } ( r _ { Q } - 1 )\) taken over all infinitely near singular points \(Q\) lying over \(P\) ,including \(P\) Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, an incomplete proof, or a proper subset as the route for this ID.
Remark 3.9.4
A reduced curve singularity on a smooth surface is refined by the multiplicities and configuration of its infinitely-near singular points. Hartshorne uses this discrete blowup data to define an equivalence relation finer than δ but weaker than analytic isomorphism.
Not formalized. none; no complete checked declaration under strict bundle semantics — As of 2026-09-06, no checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: A reduced curve singularity on a smooth surface is refined by the multiplicities and configuration of its infinitely-near singular points. Hartshorne uses this discrete blowup data to define an equivalence relation finer than δ but weaker than analytic isomorphism. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, an incomplete proof, or a proper subset as the route for this ID.
Example 3.9.5
A double point is classified by its behavior after blowing up: a node has two transverse points over the center, a cusp has one tangential branch, while the remaining case leaves a double point infinitely near; iterating gives the corresponding singularity type.
Not formalized. none; no complete checked declaration under strict bundle semantics — As of 2026-09-06, no checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: A double point is classified by its behavior after blowing up: a node has two transverse points over the center, a cusp has one tangential branch, while the remaining case leaves a double point infinitely near; iterating gives the corresponding singularity type. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, an incomplete proof, or a proper subset as the route for this ID.
Definition/construction — linear systems with assigned base points
For points P_i on a surface and a complete system |D|, |D−P_1−⋯−P_r| is the sublinear system of divisors through the assigned base points. After blowing them up, it corresponds to |π^*D−E_1−⋯−E_r|.
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked surface blowup/linear-system interface realizes assigned base points and the transform |π*D-ΣE_i|.
Definition — unassigned and infinitely-near base points
A base point remaining on the transformed system after blowing up assigned points is an unassigned base point, viewed as infinitely near to the original surface; multiplicities and iterated infinitely-near assignments are allowed.
Not formalized. none; no complete checked declaration under strict bundle semantics — As of 2026-09-06, no checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: A base point remaining on the transformed system after blowing up assigned points is an unassigned base point, viewed as infinitely near to the original surface; multiplicities and iterated infinitely-near assignments are allowed. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, an incomplete proof, or a proper subset as the route for this ID.
Remark 4.0.1
Using this language, we can rephrase the condition (I, 7.8.2) for a complete linear system \(| D |\) to be very ample as follows: \(| D |\) is very ample if and only if(a) \(| D |\) has no base points,and(b) for every \(P \in X , | D - P |\) has no unassigned base points. Indeed, \(| D |\) separates the points \(P\) and \(Q\) if and only if \(Q\) is not a base point of \(| D - \dot { P } |\) and \(| D |\) separates tangent vectors at \(P\) if and only if \(\left| D - P \right|\) has no unassigned base points infinitely near to \(P\) ：
Not formalized. none; no complete checked declaration under strict bundle semantics — As of 2026-09-06, no checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: Using this language, we can rephrase the condition (I, 7.8.2) for a complete linear system \(\| D \|\) to be very ample as follows: \(\| D \|\) is very ample if and only if(a) \(\| D \|\) has no base points,and(b) for every \(P \in X , \| D - P \|\) has no unassigned base points. Indeed, \(\| D \|\) separates the points \(P\) and \(Q\) if and only if \(Q\) is not a base point of \(\| D - \dot { P } \|\) and \(\| D \|\) separates tangent vectors at \(P\) if and only if \(\left\| D - P \right\|\) has no unassigned base points infinitely near to \(P\) ： Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, an incomplete proof, or a proper subset as the route for this ID.
Remark 4.0.2
A complete linear system is very ample iff it has no base points and, after assigning any point P, the residual system |D−P| has no unassigned base points, including infinitely-near ones.
Not formalized. none; no complete checked declaration under strict bundle semantics — As of 2026-09-06, no checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: A complete linear system is very ample iff it has no base points and, after assigning any point P, the residual system |D−P| has no unassigned base points, including infinitely-near ones. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, an incomplete proof, or a proper subset as the route for this ID.
Remark 4.0.3
Blowing up six points of P^2 in general position, the anticanonical system of cubics through them is very ample and embeds the blowup as a nonsingular cubic surface in P^3.
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked theorem realizes the six-point blowup of P² and anticanonical cubic-surface embedding.
Proposition 4.1
Let D be the linear system of conics in \(\mathbf { P } ^ { 2 }\) with assigned base points \(P _ { 1 } , \ldots , P _ { r }\) and assume that no three of the \(P _ { i }\) are collinear. If \(r \leqslant 4\) ， then \(\mathfrak { d }\) has no unassigned base points. This result remains true if \(P _ { 2 }\) is infinitely near \(P _ { 1 }\) ：
Not formalized. none; no complete checked declaration under strict bundle semantics — As of 2026-09-06, no checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: Let D be the linear system of conics in \(\mathbf { P } ^ { 2 }\) with assigned base points \(P _ { 1 } , \ldots , P _ { r }\) and assume that no three of the \(P _ { i }\) are collinear. If \(r \leqslant 4\) ， then \(\mathfrak { d }\) has no unassigned base points. This result remains true if \(P _ { 2 }\) is infinitely near \(P _ { 1 }\) ： Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, an incomplete proof, or a proper subset as the route for this ID.
Corollary 4.2
With the same hypotheses,we have: (a）if \(r \leqslant 5\) ,then dim \(\mathfrak { d } = 5 - r\) (b）if \(r = 5\) ,then there exists a unique conic containing \(P _ { \downarrow } , \dots , P _ { 5 }\) ,which isnecessarily irreducible. Furthermore,these results remain true if \(P _ { 5 }\) is infinitely near any one of \(P _ { \mathrm { 1 } } , \dots , P _ { 4 }\)
Not formalized. none; no complete checked declaration under strict bundle semantics — As of 2026-09-06, no checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: With the same hypotheses,we have: (a）if \(r \leqslant 5\) ,then dim \(\mathfrak { d } = 5 - r\) (b）if \(r = 5\) ,then there exists a unique conic containing \(P _ { \downarrow } , \dots , P _ { 5 }\) ,which isnecessarily irreducible. Furthermore,these results remain true if \(P _ { 5 }\) is infinitely near any one of \(P _ { \mathrm { 1 } } , \dots , P _ { 4 }\) Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, an incomplete proof, or a proper subset as the route for this ID.
Remark 4.2.1
This last statement is the classical result that a conic is uniquely determined by giving 5 points, or 4 points and a tangent direction at one of them, or 3 points with tangent directions at two of them,or even 3 points with a tangent direction and a second order tangent direction at one of them (when \(P _ { 5 }\) is infinitely near \(P _ { 2 }\) which is infinitely near \(P _ { 1 }\) ！
Not formalized. none; no complete checked declaration under strict bundle semantics — As of 2026-09-06, no checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: This last statement is the classical result that a conic is uniquely determined by giving 5 points, or 4 points and a tangent direction at one of them, or 3 points with tangent directions at two of them,or even 3 points with a tangent direction and a second order tangent direction at one of them (when \(P _ { 5 }\) is infinitely near \(P _ { 2 }\) which is infinitely near \(P _ { 1 }\) ！ Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, an incomplete proof, or a proper subset as the route for this ID.
Example 4.2.2
If \(r = 1\) ,then D has no unassgned base points, and for any point \(P\) \(P , \mathfrak { d } \mathrm { ~ - ~ } P\) has no unassigned base points,so by (4.0.3), \(\mathfrak { d } ^ { \prime }\) is very ample on \(X ^ { \prime }\) . Since dim \(\mathfrak { d } ^ { \prime } = 4\) ,it gives an embedding of \(X ^ { \prime }\) in \(\mathbf { P } ^ { 4 }\) ,as a surface of degree 3,which is the number of unassigned intersection points oftwo divisors in d. In fact, \(X ^ { \prime }\) is just the rational ruled surface with \(e = 1\) ,and this embedding is the rational cubic scroll (2.19.1).
Not formalized. none; no complete checked declaration under strict bundle semantics — As of 2026-09-06, no checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: If \(r = 1\) ,then D has no unassgned base points, and for any point \(P\) \(P , \mathfrak { d } \mathrm { ~ - ~ } P\) has no unassigned base points,so by (4.0.3), \(\mathfrak { d } ^ { \prime }\) is very ample on \(X ^ { \prime }\) . Since dim \(\mathfrak { d } ^ { \prime } = 4\) ,it gives an embedding of \(X ^ { \prime }\) in \(\mathbf { P } ^ { 4 }\) ,as a surface of degree 3,which is the number of unassigned intersection points oftwo divisors in d. In fact, \(X ^ { \prime }\) is just the rational ruled surface with \(e = 1\) ,and this embedding is the rational cubic scroll (2.19.1). Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, an incomplete proof, or a proper subset as the route for this ID.
Example 4.2.3
Blowing up three noncollinear points of P², the conics through them define the standard quadratic Cremona transformation; on the blowup the system is base-point-free and gives a morphism back to P².
Not formalized. none; no complete checked declaration under strict bundle semantics — Pinned Mathlib has birational/rational-map infrastructure, but no checked blowup resolution of the quadratic Cremona transformation and its transformed conic system.
Proposition 4.3
Let D be the linear system of plane cubic curves with assigned base points \(P _ { 1 } , \ldots , P _ { r }\) ,and assume that no 4 of the \(P _ { i }\) are collinear,and no 7 of them lie on a conic. If \(r \leqslant 7\) ,then D has no unassigned base points. This result remains true if \(P _ { 2 }\) is infinitely near \(P _ { 1 }\) ：
Not formalized. none; no complete checked declaration under strict bundle semantics — As of 2026-09-06, no checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: Let D be the linear system of plane cubic curves with assigned base points \(P _ { 1 } , \ldots , P _ { r }\) ,and assume that no 4 of the \(P _ { i }\) are collinear,and no 7 of them lie on a conic. If \(r \leqslant 7\) ,then D has no unassigned base points. This result remains true if \(P _ { 2 }\) is infinitely near \(P _ { 1 }\) ： Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, an incomplete proof, or a proper subset as the route for this ID.
Corollary 4.4
With the same hypotheses,we have (a)if \(r \leqslant 8\) ,then dim \(\mathfrak { d } = 9 \ : - \ : r\) and (b）if \(r = 8\) ,dim \(\mathfrak { d } = 1\) and almost every curve in D is irreducible.
Not formalized. none; no complete checked declaration under strict bundle semantics — As of 2026-09-06, no checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: With the same hypotheses,we have (a)if \(r \leqslant 8\) ,then dim \(\mathfrak { d } = 9 \ : - \ : r\) and (b）if \(r = 8\) ,dim \(\mathfrak { d } = 1\) and almost every curve in D is irreducible. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, an incomplete proof, or a proper subset as the route for this ID.
Corollary 4.5
Giten 8 points \(P _ { 1 } , \dots , P _ { 8 }\) in the plane,no 4 collinear, and no 7 lying on a conic, there is a uniquely determined point \(P _ { 9 }\) (possibly an infinitely near point) such that erery cubic through \(P _ { \mathrm { 1 } } , \dots , P _ { \mathrm { 8 } }\) also passes through \(P _ { 9 }\) This is still true if \(P _ { 2 }\) is infinitely near \(P _ { 1 }\) ,and \(P _ { 8 }\) is infinitely near any one of \(P _ { 1 } , \ldots , P _ { 7 }\) ：
Not formalized. none; no complete checked declaration under strict bundle semantics — As of 2026-09-06, no checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: Giten 8 points \(P _ { 1 } , \dots , P _ { 8 }\) in the plane,no 4 collinear, and no 7 lying on a conic, there is a uniquely determined point \(P _ { 9 }\) (possibly an infinitely near point) such that erery cubic through \(P _ { \mathrm { 1 } } , \dots , P _ { \mathrm { 8 } }\) also passes through \(P _ { 9 }\) This is still true if \(P _ { 2 }\) is infinitely near \(P _ { 1 }\) ,and \(P _ { 8 }\) is infinitely near any one of \(P _ { 1 } , \ldots , P _ { 7 }\) ： Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, an incomplete proof, or a proper subset as the route for this ID.
Remark 4.5.1
This classical result has a number of interesting geometrical consequences. See (Ex.4.4),(Ex. 4.5).
Not formalized. none; no complete checked declaration under strict bundle semantics — As of 2026-09-06, no checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: This classical result has a number of interesting geometrical consequences. See (Ex.4.4),(Ex. 4.5). Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, an incomplete proof, or a proper subset as the route for this ID.
Theorem 4.6
Let D be the linear system of plane cubic curves with assigned (ordinary) base points \(P _ { 1 } , \ldots , P _ { r }\) ,and assume that no 3 of the \(P _ { i }\) are collinear,and no 6 of them lie on a conic. If \(r \leqslant 6\) ，then the corresponding linear system \(\mathfrak { d } ^ { \prime }\) on the surface \(X ^ { \prime }\) obtained from \(\mathbf { P } ^ { 2 } \ b _ { \mathrm { J } } ,\) blowing up \(P _ { 1 } , \dots ,\) \(P _ { r }\) ,is very ample.
Not formalized. none; no complete checked declaration under strict bundle semantics — As of 2026-09-06, no checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: Let D be the linear system of plane cubic curves with assigned (ordinary) base points \(P _ { 1 } , \ldots , P _ { r }\) ,and assume that no 3 of the \(P _ { i }\) are collinear,and no 6 of them lie on a conic. If \(r \leqslant 6\) ，then the corresponding linear system \(\mathfrak { d } ^ { \prime }\) on the surface \(X ^ { \prime }\) obtained from \(\mathbf { P } ^ { 2 } \ b _ { \mathrm { J } } ,\) blowing up \(P _ { 1 } , \dots ,\) \(P _ { r }\) ,is very ample. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, an incomplete proof, or a proper subset as the route for this ID.
Corollary 4.7
After blowing up r≤6 suitably general points of P², the anticanonical system embeds the resulting surface in P^{9−r} with degree 9−r and canonical sheaf O(−1); for r=6 this is a smooth cubic surface in P³.
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked del Pezzo anticanonical embedding theorem for blowups of up to six points of P² was found.
Remark 4.7.1
A del Pezzo surface is a smooth surface X⊂P^d of degree d with ω_X≅O_X(−1). The blowups of P² at r≤6 general points give degrees 9−r; every smooth cubic surface arises from six such blowups.
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked del Pezzo-surface definition/classification bridge owns the complete degree/canonical-sheaf/blowup/cubic-surface bundle.
Remark 4.7.2
Dimension counting shows the cubic surfaces obtained by blowing up six general plane points form a 19-dimensional family, equal to the dimension of the full family of cubic surfaces in P³; hence a general smooth cubic is obtained this way.
Not formalized. none; no complete checked declaration under strict bundle semantics — As of 2026-09-06, no checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: Dimension counting shows the cubic surfaces obtained by blowing up six general plane points form a 19-dimensional family, equal to the dimension of the full family of cubic surfaces in P³; hence a general smooth cubic is obtained this way. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, an incomplete proof, or a proper subset as the route for this ID.
Notation 4.7.3
Fix six general points P_1,…,P_6 in P² and let X be their blowup embedded anticanonically as a cubic surface. Write l for the pullback of a line and e_i for the six exceptional classes; these form the standard basis used for the 27-line calculation.
Not formalized. none; no complete checked declaration under strict bundle semantics — As of 2026-09-06, no checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: Fix six general points P_1,…,P_6 in P² and let X be their blowup embedded anticanonically as a cubic surface. Write l for the pullback of a line and e_i for the six exceptional classes; these form the standard basis used for the 27-line calculation. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, an incomplete proof, or a proper subset as the route for this ID.
Proposition 4.8
For a smooth cubic surface obtained by blowing up six general points of P², Pic X is free on l,e_1,…,e_6 with l²=1, e_i²=−1 and all other basic intersections zero; h=3l−Σe_i and K_X=−h. These formulas determine degrees and arithmetic genera of divisor classes.
Not formalized. none; no complete checked declaration under strict bundle semantics — As of 2026-09-06, no checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: For a smooth cubic surface obtained by blowing up six general points of P², Pic X is free on l,e_1,…,e_6 with l²=1, e_i²=−1 and all other basic intersections zero; h=3l−Σe_i and K_X=−h. These formulas determine degrees and arithmetic genera of divisor classes. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, an incomplete proof, or a proper subset as the route for this ID.
Remark 4.8.1
If \(C\) is any irreducible curve in \(X\) ,other than \(E _ { 1 } , \ldots , E _ { 6 }\) ,then \(\pi ( C )\) is an irreducible plane curve \(C _ { 0 }\) ,and \(C\) in turn is the strict transform of \(C _ { 0 }\) Let \(C _ { 0 }\) have degree \(a\) ,and suppose that \(C _ { 0 }\) has a point of multiplicity \(b _ { i }\) at each \(P _ { i }\) Then \(\bar { \pi ^ { * } } C _ { 0 } = C + \bar { \sum } b _ { i } E _ { i }\) ,by (3.6). Since \(C _ { 0 } \sim a \cdot\) line, we conclude that \(\begin{array} { r } { C \sim a l - \sum b _ { i } e _ { i } } \end{array}\) .
Not formalized. none; no complete checked declaration under strict bundle semantics — As of 2026-09-06, no checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: If \(C\) is any irreducible curve in \(X\) ,other than \(E _ { 1 } , \ldots , E _ { 6 }\) ,then \(\pi ( C )\) is an irreducible plane curve \(C _ { 0 }\) ,and \(C\) in turn is the strict transform of \(C _ { 0 }\) Let \(C _ { 0 }\) have degree \(a\) ,and suppose that \(C _ { 0 }\) has a point of multiplicity \(b _ { i }\) at each \(P _ { i }\) Then \(\bar { \pi ^ { * } } C _ { 0 } = C + \bar { \sum } b _ { i } E _ { i }\) ,by (3.6). Since \(C _ { 0 } \sim a \cdot\) line, we conclude that \(\begin{array} { r } { C \sim a l - \sum b _ { i } e _ { i } } \end{array}\) . Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, an incomplete proof, or a proper subset as the route for this ID.
Theorem 4.9
(Twenty-Seven Lines). The cubic surface \(X\) contains exactly 27 lines.Each one has self-intersection \(^ { - 1 }\) ,and they are the only irreducible curves with negative self-intersection on \(X\) . They are (a) the exceptional curves \(E _ { i }\) \(i = 1 , \ldots , 6\) (six of these), (b) the strict transform \(\boldsymbol { F } _ { i j }\) of the line in \(\mathbf { P } ^ { 2 }\) containing \(P _ { i }\) and \(P _ { j } , 1 \leqslant\) \(i < j \leqslant 6\) (fifteen of these),and (c) the strict transform \(G _ { j }\) of the conic in \(\mathbf { P } ^ { 2 }\) containing the five \(P _ { i }\) for \(i \neq j , j = 1 , \ldots , 6\) (six of these).
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked formalization of the twenty-seven lines on a smooth cubic surface, their classes, or the negative-curve classification was found.
Remark 4.9.1
The twelve lines E_1,…,E_6,G_1,…,G_6 form a Schläfli double-six: each family is pairwise skew and E_i meets G_j exactly for i≠j. Such a double-six determines the classical configuration of 27 lines on a smooth cubic surface.
Not formalized. none; no complete checked declaration under strict bundle semantics — As of 2026-09-06, no checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: The twelve lines E_1,…,E_6,G_1,…,G_6 form a Schläfli double-six: each family is pairwise skew and E_i meets G_j exactly for i≠j. Such a double-six determines the classical configuration of 27 lines on a smooth cubic surface. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, an incomplete proof, or a proper subset as the route for this ID.
Proposition 4.10
Let \(X\) be a cubic surface as abore,and let \(E _ { 1 } ^ { ' } , \dots , E _ { 6 } ^ { ' }\) he any subset of six mutually skew lines chosen from among the 27 lines on \(X\) .Then there is another morphism \(\pi ^ { \prime } : X \to \mathbf { P } ^ { 2 }\) ,making \(X\) isomorphic to that \(\mathbf { P } ^ { 2 }\) with six points \(P _ { 1 } ^ { \prime } , \ldots , P _ { 6 } ^ { \prime }\) blown up (no 3 collinear and not all 6 on a conic),such that \(E _ { 1 } ^ { \prime } , \ldots , E _ { 6 } ^ { \prime }\) are the exceptional curves for \(\pi ^ { \prime }\)
Not formalized. none; no complete checked declaration under strict bundle semantics — As of 2026-09-06, no checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: Let \(X\) be a cubic surface as abore,and let \(E _ { 1 } ^ { ' } , \dots , E _ { 6 } ^ { ' }\) he any subset of six mutually skew lines chosen from among the 27 lines on \(X\) .Then there is another morphism \(\pi ^ { \prime } : X \to \mathbf { P } ^ { 2 }\) ,making \(X\) isomorphic to that \(\mathbf { P } ^ { 2 }\) with six points \(P _ { 1 } ^ { \prime } , \ldots , P _ { 6 } ^ { \prime }\) blown up (no 3 collinear and not all 6 on a conic),such that \(E _ { 1 } ^ { \prime } , \ldots , E _ { 6 } ^ { \prime }\) are the exceptional curves for \(\pi ^ { \prime }\) Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, an incomplete proof, or a proper subset as the route for this ID.
Remark 4.10.1
The proposition says that any six mutually skew lines among the 27 lines play the role of \(E_{1},\ldots,E_{6}\). Another way of expressing this is to consider the configuration of the 27 lines, forgetting the surface \(X\): the set of 27 elements named \(E_{i}\), \(F_{ij}\), \(G_{j}\) together with the incidence relations they satisfy. Those relations, deduced from (4.8) and (4.9), are: \(E_{i}\) does not meet \(E_{j}\) for \(i \neq j\); \(E_{i}\) meets \(F_{jk}\) if and only if \(i = j\) or \(i = k\); \(E_{i}\) meets \(G_{j}\) if and only if \(i \neq j\); \(F_{ij}\) meets \(F_{kl}\) if and only if \(i,j,k,l\) are all distinct; \(F_{ij}\) meets \(G_{k}\) if and only if \(i = k\) or \(j = k\); and \(G_{j}\) does not meet \(G_{k}\) for \(j \neq k\). Naming \(E_{1},\ldots,E_{6}\) determines the names of the remaining 21 lines, so every ordered set of six mutually skew lines is the image of \(E_{1},\ldots,E_{6}\) under a unique automorphism of the configuration. The automorphism group \(G\) therefore has order \(27 \cdot 16 \cdot 10 \cdot 6 \cdot 2 = 51840\); it is isomorphic to the Weyl group of \(\mathbf{E}_{6}\) and contains a normal subgroup of index 2 which is simple of order 25920.
Not formalized. none; no complete checked declaration under strict bundle semantics — As of 2026-09-06, no checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: The proposition says that any six mutually skew lines among the 27 lines play the role of \(E _ { 1 } , \ldots , E _ { 6 }\) . Another way of expressing this is to consider the configuration of the 27 lines (forgetting the surface \(X\) ). That means we consider simply the set of 27 elements named \(E _ { i } , F _ { i j } , G _ { j }\) (the lines) together with the incidence relations they satisfy. These incidence relations are easily deduced from (4.8) and (4.9), and say (explicity) \(E _ { i }\) does not meet \(E _ { j }\) for \(i \neq j ; E _ { i }\) meets \(F _ { j k }\) if and only if \(i = j\) or $i = k ; Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, an incomplete proof, or a proper subset as the route for this ID.
Theorem 4.11
The following conditions are equivalent, for a divisor \(D\) onthe cubic surface \(X\) ， (i) \(D\) is very ample; (ii) \(D\) is ample; (ii) \(D ^ { 2 } > 0\) ,and for every line \(L \subseteq X , D . L > 0\) (iv) for every line \(L \subseteq X , D . L > 0\)
Not formalized. none; no complete checked declaration under strict bundle semantics — As of 2026-09-06, no checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: The following conditions are equivalent, for a divisor \(D\) onthe cubic surface \(X\) ， (i) \(D\) is very ample; (ii) \(D\) is ample; (ii) \(D ^ { 2 } > 0\) ,and for every line \(L \subseteq X , D . L > 0\) (iv) for every line \(L \subseteq X , D . L > 0\) Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, an incomplete proof, or a proper subset as the route for this ID.
Lemma 4.12
Let \(D \sim a l - \sum b _ { i } e _ { i }\) be a divisor class on the cubic surface \(X\) ， and suppose that \(b _ { 1 } \geqslant b _ { 2 } \geqslant . . . \geqslant b _ { 6 } > 0\) and \(a \geqslant b _ { 1 } + b _ { 2 } + b _ { \mathsf { s } }\) .Then \(D\) is very ample.
Not formalized. none; no complete checked declaration under strict bundle semantics — As of 2026-09-06, no checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: Let \(D \sim a l - \sum b _ { i } e _ { i }\) be a divisor class on the cubic surface \(X\) ， and suppose that \(b _ { 1 } \geqslant b _ { 2 } \geqslant . . . \geqslant b _ { 6 } > 0\) and \(a \geqslant b _ { 1 } + b _ { 2 } + b _ { \mathsf { s } }\) .Then \(D\) is very ample. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, an incomplete proof, or a proper subset as the route for this ID.
Corollary 4.13
For D∼al−Σb_i e_i on the cubic surface, ampleness and very ampleness are equivalent to positivity against all 27 lines; explicitly b_i>0, a>b_i+b_j, and 2a>Σ_{i≠j}b_i. Every such class contains a nonsingular irreducible curve.
Not formalized. none; no complete checked declaration under strict bundle semantics — As of 2026-09-06, no checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: For D∼al−Σb_i e_i on the cubic surface, ampleness and very ampleness are equivalent to positivity against all 27 lines; explicitly b_i>0, a>b_i+b_j, and 2a>Σ_{i≠j}b_i. Every such class contains a nonsingular irreducible curve. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, an incomplete proof, or a proper subset as the route for this ID.
Example 4.13.1
The class 7l−3e_1−3e_2−2e_3−2e_4−2e_5−2e_6 contains a nonsingular irreducible curve of degree 7 and genus 5 in P³.
Not formalized. none; no complete checked declaration under strict bundle semantics — As of 2026-09-06, no checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: The class 7l−3e_1−3e_2−2e_3−2e_4−2e_5−2e_6 contains a nonsingular irreducible curve of degree 7 and genus 5 in P³. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, an incomplete proof, or a proper subset as the route for this ID.
Definition/construction — fundamental points of a birational transformation
A birational transformation T:X⇢Y has a largest open U⊆X on which it is represented by a morphism; Xs its set of fundamental points.
Formalized. Mathlib/AlgebraicGeometry/Birational/RationalMap.lean::Scheme.RationalMap.domain, Scheme.RationalMap.toPartialMap, Scheme.PartialMap.le_domain_toRationalMap — Pinned Mathlib defines the domain of a rational map as the supremum of the domains of all partial-map representatives, proves every representative domain lies in it, and, for reduced source and separated target, glues the rational map to a morphism on that maximal open. For Hartshorne’s nonsingular projective surfaces these hypotheses hold. Hartshorne’s fundamental points are exactly the set-theoretic complement of this maximal domain, so no additional geometric theorem is needed for the definition row.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d; H=5aedf732b6987e8c26ab3c9ebc855314f82b045f
Definition/construction — graph and total transform of a birational transformation
The graph Γ_T is the closure in X×Y of the graph over the domain of definition. For Z⊆X, its total transform is T(Z)=p_2(p_1^{-1}(Z)).
Not formalized. none; no complete checked declaration under strict bundle semantics — Pinned Mathlib formalizes rational maps and their maximal domains, but has no checked construction of the closure of a rational-map graph in X×Y together with Hartshorne’s total-transform operation; this row is therefore not a partial route extension of U116.
Lemma 5.1
For a birational transformation T:X⇢Y of projective varieties with X normal, the fundamental locus is closed of codimension at least two.
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked theorem proves that the complement of the domain of a birational map from a normal projective variety has codimension at least two.
Example 5.1.1
Let \(X\) be a surface,and let \(\pi { \colon } \tilde { X } \to X\) be the monoidal transformation with center \(P\) Then \(\pi\) is defined everywhere. Its inverse \(\pi ^ { - 1 } : X \to { \tilde { X } }\) is a birational transformation having \(P\) as a fundamental point.
Not formalized. none; no complete checked declaration under strict bundle semantics — As of 2026-09-06, no checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: Let \(X\) be a surface,and let \(\pi { \colon } \tilde { X } \to X\) be the monoidal transformation with center \(P\) Then \(\pi\) is defined everywhere. Its inverse \(\pi ^ { - 1 } : X \to { \tilde { X } }\) is a birational transformation having \(P\) as a fundamental point. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, an incomplete proof, or a proper subset as the route for this ID.
Theorem 5.2
Zariski Main Theorem in this form: if P is a fundamental point of a birational transformation from normal X, its total transform is connected; in the surface case it contains a curve.
Not formalized. none; no complete checked declaration under strict bundle semantics — Mathlib contains algebraic and scheme-theoretic Zariski Main Theorem infrastructure, but no checked theorem derives Hartshorne’s connected total transform of a fundamental point, and U117’s total transform is itself absent.
Proposition 5.3
If f:X′→X is a birational morphism of nonsingular surfaces and P is a fundamental point of f^{-1}, then f factors through the blowup of X at P.
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked point blowup exists to state or prove the factorization of a birational surface morphism through the blowup of a fundamental point.
Corollary 5.4
A birational morphism of nonsingular projective surfaces factors into finitely many monoidal transformations; the number equals the number of irreducible curves contracted to points.
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked factorization theorem for birational morphisms of smooth projective surfaces into point blowups was found.
Remark 5.4.1
It is interesting to compare the factorization of (5.3) with the universal property of blowing up proved in (II, 7.14). While the new result implies the old one in the special case of blowing up a point (since \(f ^ { - 1 } \mathfrak { m } _ { P } \cdot \mathcal { O } _ { X } ,\) being invertible implies \(f ^ { - 1 } ( P )\) has dimension 1,so \(P\) is a fundamental point),it is actually stronger, since it uses Zariski’s Main Theorem. We cannot deduce (5.3) from (II, 7.14), because the hypothesis that \(f ^ { - 1 } \mathfrak { m } _ { P } \cdot \ell _ { X ^ { \prime } } ^ { \prime }\) is invertible is impossible to verify in our case.
Not formalized. none; no complete checked declaration under strict bundle semantics — As of 2026-09-06, no checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: It is interesting to compare the factorization of (5.3) with the universal property of blowing up proved in (II, 7.14). While the new result implies the old one in the special case of blowing up a point (since \(f ^ { - 1 } \mathfrak { m } _ { P } \cdot \mathcal { O } _ { X } ,\) being invertible implies \(f ^ { - 1 } ( P )\) has dimension 1,so \(P\) is a fundamental point),it is actually stronger, since it uses Zariski’s Main Theorem. We cannot deduce (5.3) from (II, 7.14), because the hypothesis that \(f ^ { - 1 } \mathfrak { m } _ { P } \cdot \ell _ { X ^ { \prime } } ^ { \prime }\) is invertible is impossible to verify in our case. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, an incomplete proof, or a proper subset as the route for this ID.
Remark 5.4.2
Comparing (5.4) to the earlier theorem (II, 7.17), we see that the new result is more precise, because it uses only monoidal transformations,rather than the more general concept of blowing up an arbitrary sheaf of ideals.
Not formalized. none; no complete checked declaration under strict bundle semantics — As of 2026-09-06, no checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: Comparing (5.4) to the earlier theorem (II, 7.17), we see that the new result is more precise, because it uses only monoidal transformations,rather than the more general concept of blowing up an arbitrary sheaf of ideals. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, an incomplete proof, or a proper subset as the route for this ID.
Remark 5.4.3
The surface factorization statement fails in dimension at least three: blowing up a nonsingular curve in a smooth threefold cannot in general be factored first through the blowup of an arbitrary point of that curve.
Not formalized. none; no complete checked declaration under strict bundle semantics — As of 2026-09-06, no checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: The surface factorization statement fails in dimension at least three: blowing up a nonsingular curve in a smooth threefold cannot in general be factored first through the blowup of an arbitrary point of that curve. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, an incomplete proof, or a proper subset as the route for this ID.
Remark 5.4.4
Even allowing monoidal transformations along nonsingular centers, an arbitrary birational morphism of smooth projective varieties need not factor this way in dimensions at least three.
Not formalized. none; no complete checked declaration under strict bundle semantics — As of 2026-09-06, no checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: Even allowing monoidal transformations along nonsingular centers, an arbitrary birational morphism of smooth projective varieties need not factor this way in dimensions at least three. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, an incomplete proof, or a proper subset as the route for this ID.
Theorem 5.5
Every birational transformation between nonsingular projective surfaces factors into a finite sequence of monoidal transformations and their inverses.
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked factorization of arbitrary birational transformations of smooth projective surfaces into point blowups and inverse blowups was found.
Corollary 5.6
The arithmetic genus of a nonsingular projective surface is a birational invariant.
Not formalized. none; no complete checked declaration under strict bundle semantics — C02 already records the geometric-genus birational-invariance row as unmatched; no checked arithmetic-genus birational-invariance theorem for smooth projective surfaces was found either.
Remark 5.6.1
In characteristic zero, Hironaka resolution supplies a common resolution of a birational map by successive blowups along nonsingular centers; Hartshorne notes this yields birational invariance of the arithmetic genus in all dimensions.
Not formalized. none; no complete checked declaration under strict bundle semantics — As of 2026-09-06, no checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: In characteristic zero, Hironaka resolution supplies a common resolution of a birational map by successive blowups along nonsingular centers; Hartshorne notes this yields birational invariance of the arithmetic genus in all dimensions. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, an incomplete proof, or a proper subset as the route for this ID.
Theorem 5.7
Castelnuovo criterion: any exceptional curve E≅P^1 with E^2=−1 can be contracted to a nonsingular point; equivalently the surface is the blowup of the contracted surface at that point.
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked Castelnuovo contraction criterion for exceptional P¹ with self-intersection -1 was found.
Example 5.7.1
An elementary transformation of a ruled surface is obtained by blowing up a point P on a fibre and then contracting the strict transform of that fibre, which becomes a (−1)-curve.
Not formalized. none; no complete checked declaration under strict bundle semantics — As of 2026-09-06, no checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: An elementary transformation of a ruled surface is obtained by blowing up a point P on a fibre and then contracting the strict transform of that fibre, which becomes a (−1)-curve. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, an incomplete proof, or a proper subset as the route for this ID.
Remark 5.7.2
Hartshorne formulates the general contraction problem: a closed subset Y⊂X is contractible if a birational morphism contracts exactly Y to one point and is an isomorphism off Y. For curves on surfaces, negativity of the intersection form is the fundamental necessary condition, with additional algebraic criteria needed for contraction to a scheme.
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked contraction criterion for curves on algebraic surfaces based on negativity of the intersection form was found.
Example 5.7.3
Hironaka’s example blows up ten suitably independent points on a smooth plane cubic; its strict transform has self-intersection −1 but is not P¹, illustrating that negative self-intersection alone does not characterize contractible exceptional curves of the first kind.
Not formalized. none; no complete checked declaration under strict bundle semantics — As of 2026-09-06, no checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: Hironaka’s example blows up ten suitably independent points on a smooth plane cubic; its strict transform has self-intersection −1 but is not P¹, illustrating that negative self-intersection alone does not characterize contractible exceptional curves of the first kind. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, an incomplete proof, or a proper subset as the route for this ID.
Theorem 5.8
Erery surface admits a birational morphism to a relatively minimal model.
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked existence theorem for relatively minimal models of algebraic surfaces was found.
Remark 5.8.1
In spite of this result, it is not true that a surface necessarily has only finitely many exceptional curves of the first kind. For example, if we blow up r points in general position in P²,with r ≥ 9, then the resulting surface has infinitely many exceptional curves of the first kind (Ex.4.15).
Not formalized. none; no complete checked declaration under strict bundle semantics — As of 2026-09-06, no checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: In spite of this result, it is not true that a surface necessarily has only finitely many exceptional curves of the first kind. For example, if we blow up r points in general position in P²,with r ≥ 9, then the resulting surface has infinitely many exceptional curves of the first kind (Ex.4.15). Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, an incomplete proof, or a proper subset as the route for this ID.
Example 5.8.2
In the birational equivalence class of rational surfaces, \(\mathbf { P } ^ { 2 }\) is a relatively minimal model,and so is the rational ruled surface \(X _ { e }\) for each \(\epsilon \geqslant 0 , e \neq 1\) ．This follows easily from the determination of all irreducible curves on \(X _ { e }\) (2.18). On the contrary, \(X _ { 1 }\) is not relatively minimal (2.11.5).
Not formalized. none; no complete checked declaration under strict bundle semantics — As of 2026-09-06, no checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: In the birational equivalence class of rational surfaces, \(\mathbf { P } ^ { 2 }\) is a relatively minimal model,and so is the rational ruled surface \(X _ { e }\) for each \(\epsilon \geqslant 0 , e \neq 1\) ．This follows easily from the determination of all irreducible curves on \(X _ { e }\) (2.18). On the contrary, \(X _ { 1 }\) is not relatively minimal (2.11.5). Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, an incomplete proof, or a proper subset as the route for this ID.
Example 5.8.3
In the class of surfaces birational to \(\mathbf { P } ^ { 1 } \times C\) ，where \(C\) isa curve of genus \(g > 0\) ,every geometrically ruled surface \(\pi { \colon X } \to C\) is relatively minimal. Indeed, if \(Y\) is any rational curve in \(X\) ,then \(\pi ( Y )\) is a point because of (IV, 2.5.4). Thus \(Y\) is a fibre of \(\pi\) ， \(Y ^ { 2 } = 0\) ,and so we see that \(X\) has no exceptional curves of the first kind.
Not formalized. none; no complete checked declaration under strict bundle semantics — As of 2026-09-06, no checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: In the class of surfaces birational to \(\mathbf { P } ^ { 1 } \times C\) ，where \(C\) isa curve of genus \(g > 0\) ,every geometrically ruled surface \(\pi { \colon X } \to C\) is relatively minimal. Indeed, if \(Y\) is any rational curve in \(X\) ,then \(\pi ( Y )\) is a point because of (IV, 2.5.4). Thus \(Y\) is a fibre of \(\pi\) ， \(Y ^ { 2 } = 0\) ,and so we see that \(X\) has no exceptional curves of the first kind. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, an incomplete proof, or a proper subset as the route for this ID.
Remark 5.8.4
A classical theorem， proved in all characteristicsby Zariski[5],[6],[9] states that except for the rational and ruled surfaces. every surface is birational to a (unique) minimal model. One can also show that in the case of rational and ruled surfaces, every relatively minimal model is one of those listed in (5.8.2) and (5.8.3). See Nagata [5] or Hartshorne [4].
Not formalized. none; no complete checked declaration under strict bundle semantics — As of 2026-09-06, no checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: A classical theorem， proved in all characteristicsby Zariski[5],[6],[9] states that except for the rational and ruled surfaces. every surface is birational to a (unique) minimal model. One can also show that in the case of rational and ruled surfaces, every relatively minimal model is one of those listed in (5.8.2) and (5.8.3). See Nagata [5] or Hartshorne [4]. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, an incomplete proof, or a proper subset as the route for this ID.
Definition — Kodaira dimension
For projective X with canonical divisor K, κ(X)=trdeg_k(⊕_{n≥0}H^0(X,L(nK)))−1. Equivalently it is the maximal dimension of an image defined by |nK|; set κ=−1 if every |nK| is empty. It is birationally invariant.
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked Kodaira-dimension definition for algebraic varieties/surfaces via the canonical section ring or pluricanonical maps was found.
Theorem 6.1
For a nonsingular projective surface, κ=−1 iff |12K| is empty iff the surface is rational or ruled.
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked Enriques–Kodaira classification theorem identifies κ=-1, emptiness of |12K|, and rational/ruled surfaces.
Theorem 6.2
Castelnuovo rationality criterion: X is rational iff p_a(X)=0 and P_2(X)=h^0(X,L(2K))=0.
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked Castelnuovo rationality criterion for smooth projective surfaces was found.
Remark 6.2.1
A separable two-dimensional Lüroth theorem follows: if k⊂L⊂k(t,u) and k(t,u)/L is finite separable, then L is purely transcendental over k.
Not formalized. none; no complete checked declaration under strict bundle semantics — Pinned Mathlib has the one-variable field-theoretic Lüroth theorem, but no checked separable two-dimensional Lüroth theorem for intermediate fields of k(t,u).
Theorem 6.3
For characteristic different from 2 and 3, κ=0 iff 12K∼0. The minimal surfaces are K3, Enriques, abelian, or hyperelliptic surfaces, with the invariants stated by Hartshorne.
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked classification of minimal κ=0 surfaces into K3, Enriques, abelian and hyperelliptic cases with Hartshorne’s invariants was found.
Theorem 6.4
For characteristic different from 2 and 3, every surface with κ=1 is an elliptic surface: it admits a morphism to a curve whose general fibres are nonsingular elliptic curves.
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked classification theorem that every κ=1 surface (in the stated characteristics) is elliptic was found.
Theorem 6.5
κ=2 iff some pluricanonical system |nK| defines a birational morphism onto its image; these are the surfaces of general type.
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked theorem identifies κ=2 with a birational pluricanonical map and the general-type condition.