FC12 — Beauville, Complex Algebraic Surfaces, 2nd ed.
FC12 — Beauville, Complex Algebraic Surfaces.
This chapter contains 2 definitions, 1 theorem, 7 propositions, 4 lemmas, 1 corollary, 7 examples, 1 remark, 1 convention and 1 other statements.
Of the 25 statements checked against Lean, 0 are formalized somewhere and 25 are not.
| Status | Statements | Share | What it means |
|---|---|---|---|
| not formalized | 25 | 100% | A documented search found no Lean statement of it anywhere. |
| checked in total | 25 |
- Canonical source block: FC12 Beauville, Chapter IV,
FC12-C04-U001–FC12-C04-U025, exactly 25 unique contiguous rows. - Search order: project
A=12618f8abc2b4852b3da9ab65c3bc547ac4c1f19, pinned MathlibP=db584cd6d46c92f209a44c0f1c829460d327499d, currentH=71a80585ee495fc24472fd0eaffc89d94e4fd8d6, current/open/indexed search, Reservoir/packages, broad GitHub Lean, and local FC06/FC13 mappings. - C04 has 0 positive routes and 25 dated
unmatchedrows. - The chapter sits beyond three already-established gaps: no geometric blow-up, no scheme divisor/intersection pairing, and no algebraic projective-bundle/Hirzebruch-surface layer. Those gaps block the del Pezzo and rational-surface constructions even where projective space and rational maps themselves exist.
- Targeted P/H and broad GitHub searches found no Veronese/Steiner surface formalization, cubic ruled surface, del Pezzo surfaces, 27-line theorem/configuration, or cubic-surface blow-up classification. A GitHub hit named
delPezzois a Sage/Python package, not Lean. - U004 is not promoted from polynomial dimension combinatorics because the source statement is sheaf cohomology
H⁰(P^r,O(k)), and no checked twisting-sheaf/global-section identification exists at P/H. N=2026-09-07marks dated unmatched decisions. Strict whole-row semantics apply uniformly.
Convention / notation
For \(\mathbb F_n=\mathbf P_{\mathbf P^1}(\mathcal O\oplus\mathcal O(n))\), \(h\) denotes the tautological divisor class and \(f\) the fibre class.
Not formalized. none; no complete checked declaration under strict bundle semantics — This row depends on the absent algebraic projective-bundle/Hirzebruch-surface and surface intersection/Picard layer; projective spaces or Proj alone do not state it. Strict whole-row semantics reject proper subsets and substantive reconstruction from projective-space, polynomial, rational-map, or generic complete-intersection ingredients.
Proposition IV.1
Proposition IV.1 (i) Pic \(\mathbb { F } _ { n } = \mathbb { Z } h \oplus \mathbb { Z } f\) ，with \(f ^ { 2 } = 0 , f . h = 1 , h ^ { 2 } = n\) (ii）If \(n > 0\) ， then there is a unique irreducible curve \(B\) on \(\mathbb { F } _ { n }\) with negative self-intersection. If \(\pmb { b }\) is its class in Pic \(\mathbb { F } _ { n }\) ，then \(b =\) \(h - n f\) ， \(\ b ^ { 2 } = - n\) ： (iii) \(\mathbb { F } _ { n }\) and \(\mathbb { F } _ { m }\) are not isomorphic unless \(n = m\) \(\mathbb { F } _ { n }\) is minimal except if \(n = 1 ; \mathbb { F } _ { 1 }\) is isomorphic to \(\mathbb { P } ^ { 2 }\) with a point blown \({ \pmb u } _ { p }\) ，
Not formalized. none; no complete checked declaration under strict bundle semantics — This row depends on the absent algebraic projective-bundle/Hirzebruch-surface and surface intersection/Picard layer; projective spaces or Proj alone do not state it. Strict whole-row semantics reject proper subsets and substantive reconstruction from projective-space, polynomial, rational-map, or generic complete-intersection ingredients.
Example / construction IV.2(1)
A birational presentation of a rational surface by \(\mathbf P^2\) produces a plane linear system; its dimension is computed from the space of degree-\(d\) forms with the imposed base conditions.
Not formalized. none; no complete checked declaration under strict bundle semantics — The row depends essentially on blow-ups, divisor linear systems, surface intersection theory, del Pezzo/cubic-surface classification, or their line configurations, none of which is formalized in P/H or the project. Strict whole-row semantics reject proper subsets and substantive reconstruction from projective-space, polynomial, rational-map, or generic complete-intersection ingredients.
Fact IV.3
Fact IV.3. \(\dim H^0(\mathbf P^r,\mathcal O_{\mathbf P^r}(k))=\binom{r+k}{r}\).
Not formalized. none; no complete checked declaration under strict bundle semantics — Mathlib has homogeneous multivariate polynomials and finite-dimensional combinatorics, but no checked theorem identifying H⁰(P^r,O(k)) with degree-k homogeneous forms and deriving the stated binomial dimension; the coherent sheaf/global-section interface is missing. Strict whole-row semantics reject proper subsets and substantive reconstruction from projective-space, polynomial, rational-map, or generic complete-intersection ingredients.
Example / construction IV.2(2)
Blowing up the base points of a plane linear system replaces it by a morphism associated with a divisor class \(dL-\sum m_iE_i\).
Not formalized. none; no complete checked declaration under strict bundle semantics — The row depends essentially on blow-ups, divisor linear systems, surface intersection theory, del Pezzo/cubic-surface classification, or their line configurations, none of which is formalized in P/H or the project. Strict whole-row semantics reject proper subsets and substantive reconstruction from projective-space, polynomial, rational-map, or generic complete-intersection ingredients.
Example / construction IV.2(3)
The resolved linear system embeds the blow-up exactly when it separates points and tangent directions.
Not formalized. none; no complete checked declaration under strict bundle semantics — The row depends essentially on blow-ups, divisor linear systems, surface intersection theory, del Pezzo/cubic-surface classification, or their line configurations, none of which is formalized in P/H or the project. Strict whole-row semantics reject proper subsets and substantive reconstruction from projective-space, polynomial, rational-map, or generic complete-intersection ingredients.
Example / construction IV.2(4)
For an embedded blow-up of \(\mathbf P^2\), the Picard basis \(L,E_i\) computes the hyperplane class, degree, and curve degrees by intersection.
Not formalized. none; no complete checked declaration under strict bundle semantics — The row depends essentially on blow-ups, divisor linear systems, surface intersection theory, del Pezzo/cubic-surface classification, or their line configurations, none of which is formalized in P/H or the project. Strict whole-row semantics reject proper subsets and substantive reconstruction from projective-space, polynomial, rational-map, or generic complete-intersection ingredients.
Example / construction IV.2(5)
Passing to the subsystem of curves through a point corresponds to projecting the embedded rational surface away from the image of that point.
Not formalized. none; no complete checked declaration under strict bundle semantics — The row depends essentially on blow-ups, divisor linear systems, surface intersection theory, del Pezzo/cubic-surface classification, or their line configurations, none of which is formalized in P/H or the project. Strict whole-row semantics reject proper subsets and substantive reconstruction from projective-space, polynomial, rational-map, or generic complete-intersection ingredients.
Lemma IV.4
Lemma IV.4 Let \(s\) be a surface in \(\mathbb { P } ^ { N }\) and \(p \in \mathbb { P } ^ { N } - S \ ( r e s p . \ p \in S )\) ： Let \(f : S \to \mathbb { P } ^ { N - 1 }\) (resp. \(\hat { S } \to { \mathbb P } ^ { N - 1 }\) ） be the projection away from \(\pmb { p }\) For \(f\) to be an embedding, it is necessary and sufficient that there should be no line through \(\pmb { p }\) meeting \(s\) in at least 2 (resp. 3) points, counted with multiplicity. The set of bisecants (resp. tangents) to \(s\) is parametrized by the complement of the diagonal in \(S \times S\) (resp.the projective tangent bundle to \(S )\) .It follows that the union of the bisecants (resp. tangents) to \(s\) lies in a subvariety of \(\mathbb { P } ^ { N }\) of dimension \(\leqslant 5\) (resp. \(\leqslant 4\) ).Then Lemma IV.4 gives the following result:
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked Lean formalization was found for secant/tangent projection criteria, generic projection of surfaces, projected Veronese/Steiner surfaces, or their singularity statements. Strict whole-row semantics reject proper subsets and substantive reconstruction from projective-space, polynomial, rational-map, or generic complete-intersection ingredients.
Proposition IV.5
Proposition IV.5. Every smooth projective surface admits an embedding in \(\mathbf P^5\) by generic projection from a sufficiently high projective embedding. A generic projection of a surface in \(\mathbf P^5\) is an immersion and is injective except for finitely many identified pairs.
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked Lean formalization was found for secant/tangent projection criteria, generic projection of surfaces, projected Veronese/Steiner surfaces, or their singularity statements. Strict whole-row semantics reject proper subsets and substantive reconstruction from projective-space, polynomial, rational-map, or generic complete-intersection ingredients.
Example / construction
The complete conic system embeds \(\mathbf P^2\) into \(\mathbf P^5\) as the degree-\(4\) Veronese surface; its lines map to a two-dimensional family of conics.
Not formalized. none; no complete checked declaration under strict bundle semantics — Mathlib has projective space and polynomial maps but no checked Veronese surface embedding together with the line-to-conic family statement. Strict whole-row semantics reject proper subsets and substantive reconstruction from projective-space, polynomial, rational-map, or generic complete-intersection ingredients.
Proposition IV.6
Proposition IV.6. Projection of the Veronese surface \(V\subset\mathbf P^5\) from a generic point of \(\mathbf P^5\) restricts to an isomorphism of \(V\) onto its image in \(\mathbf P^4\).
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked Lean formalization was found for secant/tangent projection criteria, generic projection of surfaces, projected Veronese/Steiner surfaces, or their singularity statements. Strict whole-row semantics reject proper subsets and substantive reconstruction from projective-space, polynomial, rational-map, or generic complete-intersection ingredients.
Definition / example
A generic projection of the projected Veronese surface to \(\mathbf P^3\) is a degree-\(4\) Steiner surface, with three double lines meeting at a triple point.
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked Lean formalization was found for secant/tangent projection criteria, generic projection of surfaces, projected Veronese/Steiner surfaces, or their singularity statements. Strict whole-row semantics reject proper subsets and substantive reconstruction from projective-space, polynomial, rational-map, or generic complete-intersection ingredients.
Example / construction
Projection of the Veronese surface from a point on it embeds \(\mathbb F_1\) in \(\mathbf P^4\) by \(|h+f|\) as the cubic ruled surface; its ruling fibres and negative section map to its lines.
Not formalized. none; no complete checked declaration under strict bundle semantics — This row depends on the absent algebraic projective-bundle/Hirzebruch-surface and surface intersection/Picard layer; projective spaces or Proj alone do not state it. Strict whole-row semantics reject proper subsets and substantive reconstruction from projective-space, polynomial, rational-map, or generic complete-intersection ingredients.
Proposition IV.7
Proposition IV.7 The cubic ruled surface \(S \subset \mathbb { P } ^ { 4 }\) is contained in a 2-dimensional linear system of quadrics in \(\mathbb { P } ^ { 4 }\) ，of which it is the intersection. For every pencil of quadrics \(\{ \lambda Q _ { 1 } + \mu Q _ { 2 } \}\) containing \(s\) \(Q _ { 1 } \cap Q _ { 2 } = S \cup P\) ，where \(P\) is a plane and \(S \cap P\) a conic. Conversely, for every conic on \(s\) lying in a plane \(P\) ， \(\mathcal { S } \cup \mathcal { P }\) is the intersection of two quadrics.
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked Lean owner was found for the cubic ruled surface as a two-dimensional system/intersection of quadrics with the stated residual-plane and converse properties. Strict whole-row semantics reject proper subsets and substantive reconstruction from projective-space, polynomial, rational-map, or generic complete-intersection ingredients.
Corollary IV.8
Corollary IV.8 The projection of \(s\) from a point \(p \in \mathbb { P } ^ { 4 } - S\) is a cubic surface whose only singularities are a double line.
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked Lean formalization was found for secant/tangent projection criteria, generic projection of surfaces, projected Veronese/Steiner surfaces, or their singularity statements. Strict whole-row semantics reject proper subsets and substantive reconstruction from projective-space, polynomial, rational-map, or generic complete-intersection ingredients.
Definition / convention
Points \(p_1,\dots,p_r\in\mathbf P^2\) with \(r\le6\) are in general position when no three are collinear and no six lie on a conic.
Not formalized. none; no complete checked declaration under strict bundle semantics — Collinearity and conics can be expressed using generic projective geometry, but no canonical general position object or theorem owns Beauville’s exact bundled definition for up to six points of P². Strict whole-row semantics reject proper subsets and substantive reconstruction from projective-space, polynomial, rational-map, or generic complete-intersection ingredients.
Proposition IV.9
Proposition IV.9. Blowing up \(r\le6\) points of \(\mathbf P^2\) in general position, the cubics through them embed the blow-up \(P_r\) in \(\mathbf P^{9-r}\) as a del Pezzo surface of degree \(9-r\); in particular degree \(3\) gives a cubic surface and degree \(4\) a complete intersection of two quadrics.
Not formalized. none; no complete checked declaration under strict bundle semantics — The row depends essentially on blow-ups, divisor linear systems, surface intersection theory, del Pezzo/cubic-surface classification, or their line configurations, none of which is formalized in P/H or the project. Strict whole-row semantics reject proper subsets and substantive reconstruction from projective-space, polynomial, rational-map, or generic complete-intersection ingredients.
Remarks IV.10
Remarks IV.10. On the blow-up \(P_r\) of \(\mathbf P^2\) at \(r\le6\) general points, the cubics through the points form the complete anticanonical system; together with \(\mathbf P^1\times\mathbf P^1\), these give the standard del Pezzo surfaces.
Not formalized. none; no complete checked declaration under strict bundle semantics — The row depends essentially on blow-ups, divisor linear systems, surface intersection theory, del Pezzo/cubic-surface classification, or their line configurations, none of which is formalized in P/H or the project. Strict whole-row semantics reject proper subsets and substantive reconstruction from projective-space, polynomial, rational-map, or generic complete-intersection ingredients.
Lemma IV.11
Lemma IV.11 Let \(S \subset \mathbb { P } ^ { r + 2 }\) be a surface that is the complete intersection of hypersurfaces \(H _ { 1 } , \ldots , H _ { r }\) of degrees \(d _ { 1 } , \ldots , d _ { r }\) respectively. Then \(\begin{array} { r } { \mathcal { O } _ { S } ( K _ { S } ) \cong \mathcal { O } _ { S } ( \sum d _ { i } - r - 3 ) } \end{array}\) ：
Not formalized. none; no complete checked declaration under strict bundle semantics — Mathlib has Kähler differentials and projective complete-intersection ingredients, but no canonical-bundle/adjunction theorem for a smooth complete-intersection surface giving O_S(Σd_i-r-3). Strict whole-row semantics reject proper subsets and substantive reconstruction from projective-space, polynomial, rational-map, or generic complete-intersection ingredients.
Proposition IV.12
Proposition IV.12 \(S _ { d }\) contains a finite number of lines. They are the images under \(j\) of the following curves in \(P _ { r }\) (i) the exceptional curves \(E _ { i }\) (ii) the strict transforms of the lines \(\langle p _ { i } , p _ { j } \rangle ~ ( i \neq j )\) ： (iii) the strict transforms of the conics through 5 of the \({ \pmb p } _ { \pmb i }\) ： Their numbers are given in this table: 
Not formalized. none; no complete checked declaration under strict bundle semantics — The row depends essentially on blow-ups, divisor linear systems, surface intersection theory, del Pezzo/cubic-surface classification, or their line configurations, none of which is formalized in P/H or the project. Strict whole-row semantics reject proper subsets and substantive reconstruction from projective-space, polynomial, rational-map, or generic complete-intersection ingredients.
Theorem IV.13
Theorem IV.13. Every smooth cubic surface in \(\mathbf P^3\) is a del Pezzo surface of degree \(3\), hence isomorphic to the blow-up of \(\mathbf P^2\) at six points in general position.
Not formalized. none; no complete checked declaration under strict bundle semantics — The row depends essentially on blow-ups, divisor linear systems, surface intersection theory, del Pezzo/cubic-surface classification, or their line configurations, none of which is formalized in P/H or the project. Strict whole-row semantics reject proper subsets and substantive reconstruction from projective-space, polynomial, rational-map, or generic complete-intersection ingredients.
Lemma IV.14
Lemma IV.14 \(s\) contains a line.
Not formalized. none; no complete checked declaration under strict bundle semantics — The row depends essentially on blow-ups, divisor linear systems, surface intersection theory, del Pezzo/cubic-surface classification, or their line configurations, none of which is formalized in P/H or the project. Strict whole-row semantics reject proper subsets and substantive reconstruction from projective-space, polynomial, rational-map, or generic complete-intersection ingredients.
Lemma IV.15
Lemma IV.15 Let \(\ell \subset S\) be a line; then there are exactly 10 other lines in \(s\) meeting \(\ell\) (and distinct from \(\ell _ { \cdot }\) ). These fall into \(\boldsymbol { ^ 5 }\) disjoint pairs of concurrent lines. In particular, \(s\) contains two disjoint lines.
Not formalized. none; no complete checked declaration under strict bundle semantics — The row depends essentially on blow-ups, divisor linear systems, surface intersection theory, del Pezzo/cubic-surface classification, or their line configurations, none of which is formalized in P/H or the project. Strict whole-row semantics reject proper subsets and substantive reconstruction from projective-space, polynomial, rational-map, or generic complete-intersection ingredients.
Proposition IV.16
Proposition IV.16 Let \(\pmb { S }\) be the complete intersection of two quadricsin \(\mathbb { P } ^ { 4 }\) . Then \(\pmb { S }\) is a del Pezzo surface \(S _ { 4 }\) ：
Not formalized. none; no complete checked declaration under strict bundle semantics — The row depends essentially on blow-ups, divisor linear systems, surface intersection theory, del Pezzo/cubic-surface classification, or their line configurations, none of which is formalized in P/H or the project. Strict whole-row semantics reject proper subsets and substantive reconstruction from projective-space, polynomial, rational-map, or generic complete-intersection ingredients.