FC12 — Beauville, Complex Algebraic Surfaces, 2nd ed.
FC12 — Beauville, Complex Algebraic Surfaces.
This chapter contains 3 definitions, 3 theorems, 1 proposition, 2 lemmas, 2 examples, 1 construction, 2 remarks, 1 notation, 2 formulas and 3 other statements.
Of the 20 statements checked against Lean, 0 are formalized somewhere and 20 are not.
| Status | Statements | Share | What it means |
|---|---|---|---|
| not formalized | 20 | 100% | A documented search found no Lean statement of it anywhere. |
| checked in total | 20 |
- Canonical source block: FC12 Beauville, Chapter I,
FC12-C01-U001–FC12-C01-U020, exactly 20 unique contiguous rows from FC12 — Beauville, Complex Algebraic Surfaces, 2nd ed.. - Search order: project at
A=12618f8abc2b4852b3da9ab65c3bc547ac4c1f19, pinned MathlibP=db584cd6d46c92f209a44c0f1c829460d327499d(Apache-2.0, Lean 4.33.0), current MathlibH=71a80585ee495fc24472fd0eaffc89d94e4fd8d6, then current/open Mathlib work, indexed search, Reservoir/package candidates, broad GitHub Lean repositories, and local mapped-source/reference corpora. - C01 has 0 positive routes and 20 dated
unmatchedrows. Noproject-existing,mathlib,package-import, orreference-portroute survives strict whole-row checking. - The project’s
LeanCategories/Schemes/Divisors.leanis decisive evidence for the principal boundary: at P there are algebraic cycles with pushforward, but no Weil divisors, Cartier divisors, or effective Cartier divisors. P/H also has onlyCommRing.Picfor rings, not a scheme Picard group. - Targeted P/H and GitHub searches found no surface local/global intersection multiplicity package, Néron–Severi group, surface Serre duality, surface Riemann–Roch, Noether formula, genus/adjunction formula, or smooth-embedding conormal exact sequence with the source consequences. Abstract sheaf/cohomology/cycle ingredients are proper subsets and are not promoted.
- Web/GitHub search on 2026-09-07 returned no compatible Lean implementation of the missing surface theory; apparent Riemann–Roch/Serre-duality hits were planning prose or non-Lean mathematical notes rather than importable/reference Lean code.
N=2026-09-07marks dated unmatched decisions. Strict whole-row semantics apply uniformly.
Fact I.1
Fact I.1. For a smooth variety \(S\), \(\operatorname{Pic}S\) is the group of line bundles, equivalently divisor classes modulo linear equivalence. Pullback is defined for morphisms, and a generically finite morphism of surfaces has the usual pushforward on divisors.
Not formalized. none; no complete checked declaration under strict bundle semantics — Pinned/current Mathlib has the Picard group of a commutative ring, not the Picard group of a scheme/variety; the project also records that Cartier/Weil divisors are absent. AlgebraicCycle supplies pushforward of cycles but not line bundles modulo divisor linear equivalence, so the bundled Fact I.1 has no owner. Strict whole-row semantics reject proper subsets and substantive reconstruction from generic scheme, sheaf, cohomology, or cycle ingredients.
Definition I.2
Definition I.2. If \(C,C\prime\) are distinct irreducible curves on a smooth surface and \(x\in C\cap C\prime\), their local intersection multiplicity is \(m_x(C,C\prime)=\dim_{\mathbf C}\mathcal O_{S,x}/(f,g)\) for local equations \(f,g\); the curves meet transversely at \(x\) exactly when this multiplicity is \(1\).
Not formalized. none; no complete checked declaration under strict bundle semantics — No pinned/current declaration or compatible external Lean implementation was found for local intersection multiplicity of curves on a smooth surface, its transversality criterion, or the resulting global intersection number/length identification. Strict whole-row semantics reject proper subsets and substantive reconstruction from generic scheme, sheaf, cohomology, or cycle ingredients.
Definition I.3
Definition I.3. The intersection number of distinct irreducible curves is \(C\cdot C\prime=\sum_{x\in C\cap C\prime}m_x(C,C\prime)\); equivalently it is the length of the scheme-theoretic intersection \(C\cap C\prime\).
Not formalized. none; no complete checked declaration under strict bundle semantics — No pinned/current declaration or compatible external Lean implementation was found for local intersection multiplicity of curves on a smooth surface, its transversality criterion, or the resulting global intersection number/length identification. Strict whole-row semantics reject proper subsets and substantive reconstruction from generic scheme, sheaf, cohomology, or cycle ingredients.
Theorem I.4
Theorem I.4 For \(L\) ， \(L ^ { \prime }\) in Pic \(\boldsymbol { s }\) ， define \[ ( L . L ^ { \prime } ) = \chi ( \mathcal { O } _ { S } ) - \chi ( L ^ { - 1 } ) - \chi ( L ^ { \prime - 1 } ) + \chi ( L ^ { - 1 } \otimes L ^ { \prime - 1 } ) \ . \] Then( .）is a symmetric bilinear form on Pic \(s\) ，such that if \(C\) and \(C ^ { \prime }\) are two distinct irreducible curves on \(s\) then \[ ( { \mathcal O } _ { s } ( C ) . { \mathcal O } _ { s } ( C ^ { \prime } ) ) = ( C . C ^ { \prime } ) ~ . \]
Not formalized. none; no complete checked declaration under strict bundle semantics — The source row depends on the intersection pairing on the Picard group of a smooth surface. P/H has neither the scheme Picard group nor surface intersection pairing, so adjacent Euler-characteristic, projective-space, cycle, or pullback ingredients cannot state the whole result. Strict whole-row semantics reject proper subsets and substantive reconstruction from generic scheme, sheaf, cohomology, or cycle ingredients.
Lemma I.5
Lemma I.5 Let \(s \in H ^ { 0 } ( S , \mathcal { O } _ { S } ( C ) )\) (res \(p . ~ s ^ { \prime } \in H ^ { 0 } ( S , \mathcal { O } _ { S } ( C ^ { \prime } ) ) )\) beu non-zero section vanishing on \(c\) (resp. \(C ^ { \prime }\) ). The sequence \[ 0 { \mathcal O } _ { S } ( - C - C ^ { \prime } ) \stackrel { ( s ^ { \prime } , - s ) } { \longrightarrow } { \mathcal O } _ { S } ( - C ) \oplus { \mathcal O } _ { S } ( - C ^ { \prime } ) \stackrel { ( s , s ^ { \prime } ) } { \longrightarrow } { \mathcal O } _ { S } \longrightarrow { \mathcal O } _ { C \cap C ^ { \prime } } \longrightarrow 0 \] is exact.
Not formalized. none; no complete checked declaration under strict bundle semantics — Mathlib has exact-sequence machinery and sheaves of modules, but no divisor line-bundle layer on schemes with the sections and scheme-theoretic intersection needed to state this Koszul exact sequence at the source interface. Strict whole-row semantics reject proper subsets and substantive reconstruction from generic scheme, sheaf, cohomology, or cycle ingredients.
Lemma I.6
Lemma I.6 Let \(c\) be a non-singular irreducible curve on \(s\) For all \(\ b { L } \in \mathbb { P i c } \ b { S }\) ， we have \[ ( { \mathcal O } _ { s } ( C ) . L ) = \deg ( L _ { | C } ) \ . \]
Not formalized. none; no complete checked declaration under strict bundle semantics — The source row depends on the intersection pairing on the Picard group of a smooth surface. P/H has neither the scheme Picard group nor surface intersection pairing, so adjacent Euler-characteristic, projective-space, cycle, or pullback ingredients cannot state the whole result. Strict whole-row semantics reject proper subsets and substantive reconstruction from generic scheme, sheaf, cohomology, or cycle ingredients.
Fact I.7
Fact I.7 Let \(D\) be a divisor on \(s\) ，and \(H\) a hyperplane section of \(s\) (for \(^ { a }\) given embedding). There exists \(\pmb { n } \geqslant 0\) such that \(D + { \pmb n } H\) is a hyperplane section (for another embedding). In particular we can write \(D \equiv A - B\) ， where \(\pmb { A }\) and \(B\) are smooth curves on \(s\) ， with \(A \equiv D + n H\) and \(B \equiv n H\) ：
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked Lean theorem was found for the hyperplane-section twisting argument that writes an arbitrary surface divisor as a difference of smooth hyperplane sections; the required divisor/very-ample/Bertini infrastructure is not present as a complete route. Strict whole-row semantics reject proper subsets and substantive reconstruction from generic scheme, sheaf, cohomology, or cycle ingredients.
Notation: For divisors \(D,D\prime\) on a surface, \(D\cdot D\prime\) denotes the…
For divisors \(D,D\prime\) on a surface, \(D\cdot D\prime\) denotes the intersection product of the corresponding line bundles.
Not formalized. none; no complete checked declaration under strict bundle semantics — The source row depends on the intersection pairing on the Picard group of a smooth surface. P/H has neither the scheme Picard group nor surface intersection pairing, so adjacent Euler-characteristic, projective-space, cycle, or pullback ingredients cannot state the whole result. Strict whole-row semantics reject proper subsets and substantive reconstruction from generic scheme, sheaf, cohomology, or cycle ingredients.
Proposition I.8
Proposition I.8 (i) Let \(c\) be a smooth curve, \(f : S C\) a surjective morphism, \(\pmb { F }\) fibre of \(\pmb { f }\) . Then \(F ^ { 2 } = 0\) ： (ii) Let \(S ^ { \prime }\) be a surface, \(g : S S ^ { \prime }\) a generically finite morphism of degree d, \(D\) and \(D ^ { \prime }\) divisors on \(s\) . Then \({ \pmb g } ^ { * } { \cal D } . { \pmb g } ^ { * } { \cal D } ^ { \prime } = d ( { \cal D } . { \cal D } ^ { \prime } )\)
Not formalized. none; no complete checked declaration under strict bundle semantics — The source row depends on the intersection pairing on the Picard group of a smooth surface. P/H has neither the scheme Picard group nor surface intersection pairing, so adjacent Euler-characteristic, projective-space, cycle, or pullback ingredients cannot state the whole result. Strict whole-row semantics reject proper subsets and substantive reconstruction from generic scheme, sheaf, cohomology, or cycle ingredients.
Example I.9(a)
For \(S=\mathbf P^2\), \(\operatorname{Pic}S\cong\mathbf Z[H]\) and Bézout gives \(C\cdot C'=dd'\) for plane curves of degrees \(d,d'\).
Not formalized. none; no complete checked declaration under strict bundle semantics — The source row depends on the intersection pairing on the Picard group of a smooth surface. P/H has neither the scheme Picard group nor surface intersection pairing, so adjacent Euler-characteristic, projective-space, cycle, or pullback ingredients cannot state the whole result. Strict whole-row semantics reject proper subsets and substantive reconstruction from generic scheme, sheaf, cohomology, or cycle ingredients.
Example I.9(b)
For \(S=\mathbf P^1\times\mathbf P^1\), \(\operatorname{Pic}S=\mathbf Zh_1\oplus\mathbf Zh_2\), with \(h_1^2=h_2^2=0\) and \(h_1h_2=1\); curves of bidegrees \((m,n)\) and \((m',n')\) intersect in \(mn'+nm'\).
Not formalized. none; no complete checked declaration under strict bundle semantics — The source row depends on the intersection pairing on the Picard group of a smooth surface. P/H has neither the scheme Picard group nor surface intersection pairing, so adjacent Euler-characteristic, projective-space, cycle, or pullback ingredients cannot state the whole result. Strict whole-row semantics reject proper subsets and substantive reconstruction from generic scheme, sheaf, cohomology, or cycle ingredients.
Construction / interpretation I.10
I.10 (topological interpretation). The exponential sequence \(0\to\mathbf Z\to\mathcal O_S\to\mathcal O_S^*\to1\) identifies \(\operatorname{Pic}S\) with \(H^1(S,\mathcal O_S^*)\), gives an exact sequence \(0\to\operatorname{Pic}^0(S)\to\operatorname{Pic}(S)\xrightarrow{c_1}NS(S)\to0\), and identifies the divisor intersection form with cup product on \(NS(S)\).
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked scheme-level exponential-sequence/Picard-to-H² construction, Néron–Severi group, or identification of surface intersection with cup product was found in P/H or external Lean repositories. Strict whole-row semantics reject proper subsets and substantive reconstruction from generic scheme, sheaf, cohomology, or cycle ingredients.
Definition / construction
The Néron–Severi group \(NS(S)\) is the finitely generated image of \(c_1:\operatorname{Pic}S\to H^2(S,\mathbf Z)\); the intersection form on divisors is the cup-product form restricted to \(NS(S)\).
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked scheme-level exponential-sequence/Picard-to-H² construction, Néron–Severi group, or identification of surface intersection with cup product was found in P/H or external Lean repositories. Strict whole-row semantics reject proper subsets and substantive reconstruction from generic scheme, sheaf, cohomology, or cycle ingredients.
Theorem I.11
Theorem I.11 (Serre duality). For a surface \(S\) and line bundle \(L\), \(H^2(S,\omega_S)\) is one-dimensional and the cup-product pairing \(H^i(S,L)\otimes H^{2-i}(S,\omega_S\otimes L^{-1})\to\mathbf C\) is perfect.
Not formalized. none; no complete checked declaration under strict bundle semantics — Mathlib has abstract category-theoretic duality infrastructure but no Serre duality theorem for coherent sheaf cohomology on smooth projective surfaces with the stated perfect cup-product pairing. Strict whole-row semantics reject proper subsets and substantive reconstruction from generic scheme, sheaf, cohomology, or cycle ingredients.
Theorem I.12
Theorem I.12 (Riemann-Roch) For all L ∈ Pic S, \[ \chi ( L ) = \chi ( \mathcal { O } _ { S } ) + \frac { 1 } { 2 } ( L ^ { 2 } - L . \omega _ { S } ) \ . \]
Not formalized. none; no complete checked declaration under strict bundle semantics — No surface Riemann–Roch theorem for line bundles/divisors is formalized at P/H; the source formula and its Serre-duality consequences therefore have no complete route. Strict whole-row semantics reject proper subsets and substantive reconstruction from generic scheme, sheaf, cohomology, or cycle ingredients.
Remarks I.13
Remarks I.13. Writing \(h^i(D)=h^i(S,\mathcal O_S(D))\) and choosing a canonical divisor \(K\) with \(\mathcal O_S(K)=\omega_S\), Serre duality gives \(h^i(D)=h^{2-i}(K-D)\) and Riemann–Roch gives the standard divisor formula and its lower-bound form.
Not formalized. none; no complete checked declaration under strict bundle semantics — No surface Riemann–Roch theorem for line bundles/divisors is formalized at P/H; the source formula and its Serre-duality consequences therefore have no complete route. Strict whole-row semantics reject proper subsets and substantive reconstruction from generic scheme, sheaf, cohomology, or cycle ingredients.
Formula I.14
I.14 (Noether formula). \(\chi(\mathcal O_S)=\frac1{12}(K_S^2+\chi_{\rm top}(S))\).
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked Lean formalization of Noether’s formula for a smooth complex surface was found; Chern-class/topological Euler-characteristic infrastructure at this level is absent. Strict whole-row semantics reject proper subsets and substantive reconstruction from generic scheme, sheaf, cohomology, or cycle ingredients.
Formula I.15
1.15 The genus formula Let \(C\) be an irreducible curve on a surface \(S\) . The genus of \(C\) ， defined by \(g ( C ) = h ^ { 1 } ( C , { \mathcal { O } } _ { C } )\) ， is given by \(g ( C ) =\) \(1 + \textstyle { \frac { 1 } { 2 } } ( C ^ { 2 } + C . K )\)
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked surface adjunction/genus formula, normalization delta-invariant formula, or associated line-bundle intersection theory was found. Generic normalization or curve-genus ingredients do not own the bundled row. Strict whole-row semantics reject proper subsets and substantive reconstruction from generic scheme, sheaf, cohomology, or cycle ingredients.
Remarks I.16
Remarks I.16. For the normalization \(N\to C\) of an irreducible curve, \(g(C)=g(N)+\sum_x\dim\delta_x\), so \(g(C)=0\) forces \(C\simeq\mathbf P^1\); for smooth \(C\), the adjunction formula is \((K_S+C)|_C\simeq\omega_C\).
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked surface adjunction/genus formula, normalization delta-invariant formula, or associated line-bundle intersection theory was found. Generic normalization or curve-genus ingredients do not own the bundled row. Strict whole-row semantics reject proper subsets and substantive reconstruction from generic scheme, sheaf, cohomology, or cycle ingredients.
Fact I.17
Fact I.17. For an embedding \(j:X\hookrightarrow Y\) of smooth varieties with ideal sheaf \(I\), \(I/I^2\) is locally free of rank \(\operatorname{codim}(X,Y)\) and \(0\to I/I^2\to j^*\Omega_Y^1\to\Omega_X^1\to0\) is exact; for a smooth curve \(C\subset S\) this yields the adjunction formula \((K_S+C)|_C\simeq\omega_C\).
Not formalized. none; no complete checked declaration under strict bundle semantics — Mathlib has Kähler differentials and cotangent-space ingredients, but no checked smooth-embedding conormal exact sequence at the scheme-sheaf interface together with the resulting adjunction formula for a curve in a surface. Strict whole-row semantics reject proper subsets and substantive reconstruction from generic scheme, sheaf, cohomology, or cycle ingredients.