FC12 — Beauville, Complex Algebraic Surfaces, 2nd ed.
FC12 — Beauville, Complex Algebraic Surfaces.
This chapter contains 5 definitions, 2 theorems, 5 propositions, 3 lemmas, 1 corollary, 2 examples, 3 remarks and 3 other statements.
Of the 24 statements checked against Lean, 0 are formalized somewhere and 24 are not.
| Status | Statements | Share | What it means |
|---|---|---|---|
| not formalized | 24 | 100% | A documented search found no Lean statement of it anywhere. |
| checked in total | 24 |
- Canonical source block: FC12 Beauville, Chapter III,
FC12-C03-U001–FC12-C03-U024, exactly 24 unique contiguous rows. - Search order: project
A=12618f8abc2b4852b3da9ab65c3bc547ac4c1f19, pinned MathlibP=db584cd6d46c92f209a44c0f1c829460d327499d, currentH=71a80585ee495fc24472fd0eaffc89d94e4fd8d6, then current/open/indexed Mathlib, packages/Reservoir, broad GitHub Lean search, and local FC06/FC13 mappings/reference corpora. - C03 has 0 positive routes and 24 dated
unmatchedrows. - P/H has rational maps, projective schemes/spaces and vector-bundle foundations, but targeted source search found no algebraic
ProjectiveBundle/projectivization over a scheme, tautological line bundle for it, or geometrically ruled surface API. ThereforeProjis not used as a false owner for Beauville’sP_C(E)rows. - No Noether–Enriques theorem, classification of ruled surfaces, rank-two bundle classification on curves, Picard/intersection formulas for ruled surfaces, surface birational invariants, or coherent-sheaf Künneth theorem was found in Mathlib, the project, packages, or broad GitHub Lean search.
N=2026-09-07marks dated unmatched decisions. Strict whole-row semantics apply uniformly.
Definition III.1
Definition III.1 A surface \(s\) is ruled if it is birationally equivalent to \(C \times \mathbb { P } ^ { 1 }\) , where \(c\) is a smooth curve. If \(C = \mathbb { P } ^ { 1 }\) ， \(s\) is said to be rational.
Not formalized. none; no complete checked declaration under strict bundle semantics — Mathlib has birational rational maps and products/projective spaces, but no ruled-surface predicate/classification object tying a smooth surface birationally to C × P¹ or defining rational surfaces at this source level. Strict whole-row semantics reject proper subsets and reconstruction from generic rational-map, vector-bundle, Proj, sheaf, or category-theoretic ingredients.
Example III.2(a)
\(C\times\mathbf P^1\) is a ruled surface over the curve \(C\).
Not formalized. none; no complete checked declaration under strict bundle semantics — Mathlib has birational rational maps and products/projective spaces, but no ruled-surface predicate/classification object tying a smooth surface birationally to C × P¹ or defining rational surfaces at this source level. Strict whole-row semantics reject proper subsets and reconstruction from generic rational-map, vector-bundle, Proj, sheaf, or category-theoretic ingredients.
Example III.2(b)
For a rank-two vector bundle \(E\) on \(C\), the projective bundle \(\mathbf P_C(E)\) is a ruled surface over \(C\).
Not formalized. none; no complete checked declaration under strict bundle semantics — Pinned/current Mathlib has no algebraic projective-bundle construction P_C(E) over a scheme, no tautological line bundle/quotient-section correspondence, and no geometrically ruled surface package. Proj and generic vector-bundle infrastructure do not state the source row. Strict whole-row semantics reject proper subsets and reconstruction from generic rational-map, vector-bundle, Proj, sheaf, or category-theoretic ingredients.
Definition III.3
Definition III.3. A geometrically ruled surface over a smooth curve \(C\) is a smooth morphism \(p:S\to C\) whose fibres are all isomorphic to \(\mathbf P^1\).
Not formalized. none; no complete checked declaration under strict bundle semantics — Pinned/current Mathlib has no algebraic projective-bundle construction P_C(E) over a scheme, no tautological line bundle/quotient-section correspondence, and no geometrically ruled surface package. Proj and generic vector-bundle infrastructure do not state the source row. Strict whole-row semantics reject proper subsets and reconstruction from generic rational-map, vector-bundle, Proj, sheaf, or category-theoretic ingredients.
Theorem III.4
Theorem III.4 (Noether–Enriques). If \(p:S\to C\) is a morphism from a surface to a smooth curve and one fibre is smooth and isomorphic to \(\mathbf P^1\), then over a Zariski neighbourhood \(U\) of that point one has \(p^{-1}(U)\simeq U\times\mathbf P^1\) over \(U\); in particular \(S\) is ruled.
Not formalized. none; no complete checked declaration under strict bundle semantics — Pinned/current Mathlib has no algebraic projective-bundle construction P_C(E) over a scheme, no tautological line bundle/quotient-section correspondence, and no geometrically ruled surface package. Proj and generic vector-bundle infrastructure do not state the source row. Strict whole-row semantics reject proper subsets and reconstruction from generic rational-map, vector-bundle, Proj, sheaf, or category-theoretic ingredients.
Useful Remark III.5
Useful Remark III.5. The Noether–Enriques argument may be carried out locally over the base curve and then glued, so the local \(\mathbf P^1\)-bundle structure extends over a suitable open set.
Not formalized. none; no complete checked declaration under strict bundle semantics — Pinned/current Mathlib has no algebraic projective-bundle construction P_C(E) over a scheme, no tautological line bundle/quotient-section correspondence, and no geometrically ruled surface package. Proj and generic vector-bundle infrastructure do not state the source row. Strict whole-row semantics reject proper subsets and reconstruction from generic rational-map, vector-bundle, Proj, sheaf, or category-theoretic ingredients.
Remark III.6
Remark III.6. The projective-bundle description in Noether–Enriques can be recovered from the rank-two bundle \(E=p_*\mathcal O_S(H)\) and the natural morphism \(S\to\mathbf P_C(E)\).
Not formalized. none; no complete checked declaration under strict bundle semantics — Pinned/current Mathlib has no algebraic projective-bundle construction P_C(E) over a scheme, no tautological line bundle/quotient-section correspondence, and no geometrically ruled surface package. Proj and generic vector-bundle infrastructure do not state the source row. Strict whole-row semantics reject proper subsets and reconstruction from generic rational-map, vector-bundle, Proj, sheaf, or category-theoretic ingredients.
Proposition III.7
Proposition III.7 Every geometrically ruled surface over \(c\) is \(c\) -isomorphic to \(\mathbb { P } _ { C } ( E )\) for some rank 2 vector bundle over \(c\) . The bundles \(\mathbb { P } _ { C } ( E )\) \(\mathbb { P } _ { C } ( E ^ { \prime } )\) are \(c\) -isomorphic if and only if there exists a line bundle \(\pmb { L }\) on \(c\) such that \(E ^ { \prime } \cong E \otimes L\) ：
Not formalized. none; no complete checked declaration under strict bundle semantics — Pinned/current Mathlib has no algebraic projective-bundle construction P_C(E) over a scheme, no tautological line bundle/quotient-section correspondence, and no geometrically ruled surface package. Proj and generic vector-bundle infrastructure do not state the source row. Strict whole-row semantics reject proper subsets and reconstruction from generic rational-map, vector-bundle, Proj, sheaf, or category-theoretic ingredients.
Lemma III.8
Lemma III.8 Let \(s\) be a minimal surface, \(\ b { C }\) a smooth curve, \(p : S C\) a morphism with generic fibre isomorphic to \(\mathbb { P } ^ { 1 }\) . Then \(s\) is geometrically ruled by \(\pmb { p }\) (i.e. \(C\) -isomorphic to a projective bundle \(\mathbb { P } _ { C } ( E ) )\)
Not formalized. none; no complete checked declaration under strict bundle semantics — Pinned/current Mathlib has no algebraic projective-bundle construction P_C(E) over a scheme, no tautological line bundle/quotient-section correspondence, and no geometrically ruled surface package. Proj and generic vector-bundle infrastructure do not state the source row. Strict whole-row semantics reject proper subsets and reconstruction from generic rational-map, vector-bundle, Proj, sheaf, or category-theoretic ingredients.
Lemma II1.9
Lemma II1.9 Let \(\pmb { p }\) be a surjective morphism from a surface to \(\pmb { a }\) smooth curve with connected fibres, \(\begin{array} { r } { F = \sum n _ { i } C _ { i } } \end{array}\) a reducible fibre of \(\pmb { p }\) ， Then \(C _ { i } ^ { 2 } < 0\) for all \(\mathbf { \chi } _ { i }\) ，
Not formalized. none; no complete checked declaration under strict bundle semantics — The negativity of components of a reducible fibre is a surface intersection-theory theorem; the intersection pairing required to state it is absent. Strict whole-row semantics reject proper subsets and reconstruction from generic rational-map, vector-bundle, Proj, sheaf, or category-theoretic ingredients.
Theorem III.10
Theorem III.10 Let \(C\) be a smooth irrational curve. The minimal models of \(C \times \mathbb { P } ^ { 1 }\) are the geometrically ruled surfaces over \(C\) ， that is the projective bundles \(\mathbb { P } _ { C } ( E )\)
Not formalized. none; no complete checked declaration under strict bundle semantics — Pinned/current Mathlib has no algebraic projective-bundle construction P_C(E) over a scheme, no tautological line bundle/quotient-section correspondence, and no geometrically ruled surface package. Proj and generic vector-bundle infrastructure do not state the source row. Strict whole-row semantics reject proper subsets and reconstruction from generic rational-map, vector-bundle, Proj, sheaf, or category-theoretic ingredients.
Lemma III.11
Lemma III.11 (i) There exists an exact sequence \(0 \to L \to E \to M \to 0\) with \(L , M\) in Pic \(C\) ：(i） If \(h ^ { 0 } ( E ) \geqslant 1\) ， we can take \(L = \mathcal { O } _ { C } ( D )\) ，with \(D \geqslant 0\) (ii)）If \(h ^ { 0 } ( E ) \geqslant 2\) and \(\deg ( E ) > 0\) , we can assume \(D > 0\) ：
Not formalized. none; no complete checked declaration under strict bundle semantics — Mathlib has abstract exact sequences/modules and some vector-bundle infrastructure, but no coherent vector-bundle cohomology/degree theory on smooth curves sufficient for the stated line-subbundle extension, rank-two Riemann–Roch, extension-class classification, or Birkhoff/Atiyah classification row. Strict whole-row semantics reject proper subsets and reconstruction from generic rational-map, vector-bundle, Proj, sheaf, or category-theoretic ingredients.
Corollary III.12
Corollary III.12 (Riemann-Roch for rank 2 vector bundles) We have \[ \chi ( E ) = \deg ( E ) + 2 - 2 g ( C ) \ . \]
Not formalized. none; no complete checked declaration under strict bundle semantics — Mathlib has abstract exact sequences/modules and some vector-bundle infrastructure, but no coherent vector-bundle cohomology/degree theory on smooth curves sufficient for the stated line-subbundle extension, rank-two Riemann–Roch, extension-class classification, or Birkhoff/Atiyah classification row. Strict whole-row semantics reject proper subsets and reconstruction from generic rational-map, vector-bundle, Proj, sheaf, or category-theoretic ingredients.
Remark III.13
Remark III.13. Lemma III.11(i) implies that the fibration \(\mathbf P_C(E)\to C\) admits a section; equivalently, a quotient line bundle of \(E\) determines a section of the associated projective bundle.
Not formalized. none; no complete checked declaration under strict bundle semantics — Pinned/current Mathlib has no algebraic projective-bundle construction P_C(E) over a scheme, no tautological line bundle/quotient-section correspondence, and no geometrically ruled surface package. Proj and generic vector-bundle infrastructure do not state the source row. Strict whole-row semantics reject proper subsets and reconstruction from generic rational-map, vector-bundle, Proj, sheaf, or category-theoretic ingredients.
Definition / construction III.14
III.14 (extension classes). An extension \(0\to L\to E\to M\to0\) determines a class in \(H^1(C,L\otimes M^{-1})\); the extension splits exactly when this class vanishes, and proportional nonzero classes define isomorphic extensions.
Not formalized. none; no complete checked declaration under strict bundle semantics — Mathlib has abstract exact sequences/modules and some vector-bundle infrastructure, but no coherent vector-bundle cohomology/degree theory on smooth curves sufficient for the stated line-subbundle extension, rank-two Riemann–Roch, extension-class classification, or Birkhoff/Atiyah classification row. Strict whole-row semantics reject proper subsets and reconstruction from generic rational-map, vector-bundle, Proj, sheaf, or category-theoretic ingredients.
Proposition II1.15
Proposition III.15. Rank-two bundles on \(\mathbf P^1\) split, so every geometrically ruled surface over \(\mathbf P^1\) is some \(\mathbb F_n\). Over an elliptic curve, every rank-two bundle is decomposable or, up to tensoring by a line bundle, one of the two indicated nontrivial extensions. In genus \(g\), indecomposable rank-two bundles occur in families of dimension at least \(2g-3\).
Not formalized. none; no complete checked declaration under strict bundle semantics — Mathlib has abstract exact sequences/modules and some vector-bundle infrastructure, but no coherent vector-bundle cohomology/degree theory on smooth curves sufficient for the stated line-subbundle extension, rank-two Riemann–Roch, extension-class classification, or Birkhoff/Atiyah classification row. Strict whole-row semantics reject proper subsets and reconstruction from generic rational-map, vector-bundle, Proj, sheaf, or category-theoretic ingredients.
Remark III.16
Remark III.16. For \(C\ne\mathbf P^1\), \(\mathbf P_C(E)\simeq\mathbf P_C(E')\) iff there are \(u\in\operatorname{Aut}(C)\) and \(L\in\operatorname{Pic}(C)\) with \(u^*E'\simeq E\otimes L\).
Not formalized. none; no complete checked declaration under strict bundle semantics — Pinned/current Mathlib has no algebraic projective-bundle construction P_C(E) over a scheme, no tautological line bundle/quotient-section correspondence, and no geometrically ruled surface package. Proj and generic vector-bundle infrastructure do not state the source row. Strict whole-row semantics reject proper subsets and reconstruction from generic rational-map, vector-bundle, Proj, sheaf, or category-theoretic ingredients.
Definition / construction III.17
III.17 (projective bundles). For \(S=\mathbf P_C(E)\), the tautological line bundle \(\mathcal O_S(1)\) is defined from the tautological subbundle of \(p^*E\); sections of \(p\) correspond to quotient line bundles of \(E\) and determine divisor classes on \(S\).
Not formalized. none; no complete checked declaration under strict bundle semantics — Pinned/current Mathlib has no algebraic projective-bundle construction P_C(E) over a scheme, no tautological line bundle/quotient-section correspondence, and no geometrically ruled surface package. Proj and generic vector-bundle infrastructure do not state the source row. Strict whole-row semantics reject proper subsets and reconstruction from generic rational-map, vector-bundle, Proj, sheaf, or category-theoretic ingredients.
Proposition III.18
Proposition III.18 Let \(S = \mathbb { P } _ { C } ( E )\) be a geometrically ruled surface over \(c\) ， \(p : S C\) the structure map. Write \(\pmb { h }\) for the class of the sheaf \(\mathcal { O } _ { s } ( 1 )\) in Pic \(s\) (or in \(H ^ { 2 } ( S , \mathbb { Z } ) )\) . Then (i) \(\operatorname { P i c } S = p ^ { * } \operatorname { P i c } C \oplus \mathbb { Z } h\) () \(H ^ { 2 } ( S , \mathbb { Z } ) = \mathbb { Z } h \oplus \mathbb { Z } f\) ，where \(\pmb { f }\) is the class of a fibre.(m) \(h ^ { 2 } = \deg ( E )\) ， (iv) \([ K ] = - 2 h + ( \deg ( E ) + 2 g ( C ) - 2 ) f i n \ H ^ { 2 } ( S , \mathbb { Z } ) .\)
Not formalized. none; no complete checked declaration under strict bundle semantics — Pinned/current Mathlib has no algebraic projective-bundle construction P_C(E) over a scheme, no tautological line bundle/quotient-section correspondence, and no geometrically ruled surface package. Proj and generic vector-bundle infrastructure do not state the source row. Strict whole-row semantics reject proper subsets and reconstruction from generic rational-map, vector-bundle, Proj, sheaf, or category-theoretic ingredients.
Definition / notation
The standard numerical invariants are \(q(S)=h^1(\mathcal O_S)\), \(p_g(S)=h^0(K_S)\), the plurigenera \(P_n(S)=h^0(nK_S)\), the Betti numbers \(b_i\), and \(\chi_{\rm top}(S)=\sum(-1)^ib_i\).
Not formalized. none; no complete checked declaration under strict bundle semantics — The irregularity, geometric genus, plurigenera, Betti-number comparison, and their ruled/birational formulas require coherent/topological cohomology and canonical divisors for smooth projective surfaces; no complete P/H interface was found. Strict whole-row semantics reject proper subsets and reconstruction from generic rational-map, vector-bundle, Proj, sheaf, or category-theoretic ingredients.
Fact II1.19
Fact III.19. For a smooth projective surface, \(q(S)=h^0(S,\Omega_S^1)=\frac12b_1(S)\).
Not formalized. none; no complete checked declaration under strict bundle semantics — The irregularity, geometric genus, plurigenera, Betti-number comparison, and their ruled/birational formulas require coherent/topological cohomology and canonical divisors for smooth projective surfaces; no complete P/H interface was found. Strict whole-row semantics reject proper subsets and reconstruction from generic rational-map, vector-bundle, Proj, sheaf, or category-theoretic ingredients.
Proposition III.20
Proposition III.20. The irregularity \(q\), geometric genus \(p_g\), and all plurigenera \(P_n\) are birational invariants of smooth projective surfaces; in contrast, \(K^2\) and \(b_2\) need not be birational invariants.
Not formalized. none; no complete checked declaration under strict bundle semantics — The irregularity, geometric genus, plurigenera, Betti-number comparison, and their ruled/birational formulas require coherent/topological cohomology and canonical divisors for smooth projective surfaces; no complete P/H interface was found. Strict whole-row semantics reject proper subsets and reconstruction from generic rational-map, vector-bundle, Proj, sheaf, or category-theoretic ingredients.
Proposition III.21
Proposition III.21. If \(S\) is ruled over \(C\), then \(q(S)=g(C)\), \(p_g(S)=0\), and \(P_n(S)=0\) for every \(n\ge2\); if \(S\) is geometrically ruled, then \(K_S^2=8(1-g(C))\) and \(b_2(S)=2\).
Not formalized. none; no complete checked declaration under strict bundle semantics — The irregularity, geometric genus, plurigenera, Betti-number comparison, and their ruled/birational formulas require coherent/topological cohomology and canonical divisors for smooth projective surfaces; no complete P/H interface was found. Strict whole-row semantics reject proper subsets and reconstruction from generic rational-map, vector-bundle, Proj, sheaf, or category-theoretic ingredients.
Fact III.22
Fact III.22 (Künneth formula). For varieties \(X,Y\), \(H^n(X\times Y,\mathcal O_{X\times Y})\cong\bigoplus_{p+q=n}H^p(X,\mathcal O_X)\otimes H^q(Y,\mathcal O_Y)\).
Not formalized. none; no complete checked declaration under strict bundle semantics — Mathlib has abstract categorical Künneth-style constructions in unrelated contexts, but no checked Künneth formula for coherent sheaf cohomology of O_{X×Y} on algebraic varieties. Strict whole-row semantics reject proper subsets and reconstruction from generic rational-map, vector-bundle, Proj, sheaf, or category-theoretic ingredients.