FC12 — Beauville, Complex Algebraic Surfaces, 2nd ed.
FC12 — Beauville, Complex Algebraic Surfaces.
This chapter contains 3 definitions, 1 theorem, 6 propositions, 2 lemmas, 3 corollaries, 7 examples, 2 constructions and 4 remarks.
Of the 28 statements checked against Lean, 0 are formalized somewhere and 28 are not.
| Status | Statements | Share | What it means |
|---|---|---|---|
| not formalized | 28 | 100% | A documented search found no Lean statement of it anywhere. |
| checked in total | 28 |
- Canonical block
FC12-C08-U001–FC12-C08-U028, exactly 28 contiguous units. - Search order: project
A=12618f8abc2b4852b3da9ab65c3bc547ac4c1f19, pinned MathlibP=db584cd6d46c92f209a44c0f1c829460d327499d, current MathlibH=71a80585ee495fc24472fd0eaffc89d94e4fd8d6, current/open/indexed services, packages/Reservoir, broad GitHub Lean, and local references/mappings. - Result: 0 positive routes, 28 dated
unmatchedrows. - Project search found a genuine abstract
K3lattice inLeanCategories/Lattices/Valued/Standard.lean; it is deliberately not used as a surface owner. P/H and current-H grep find noK3Surface, Enriques surface, Kummer surface, du Val/rational-double-point layer, or polarized-K3 projective-model package. - Generic étale infrastructure likewise does not supply U024: no checked torsion-line-bundle-to-double-cover construction was found. Number-theoretic Kummer extensions/theorems are unrelated to Kummer surfaces.
- Broad GitHub/indexed search on 2026-09-07 returned no compatible Lean implementation of the K3/Enriques/Kummer surface statements.
N=2026-09-07marks dated unmatched decisions. Strict whole-row semantics apply uniformly.
Lemma VIII.1
Lemma VIII.1 Let \(s\) be a minimal surface with \(\kappa = 0\) . Then: (a) \(K ^ { 2 } = 0\) ： (b) \(x ( \mathcal { O } _ { s } ) \geqslant \mathbf { 0 } _ { : }\) (c） let \(\pmb { n }\) and m be two positive integers such that \(P _ { n } = P _ { m } = 1\) ; then if \(\pmb { d }\) is the g.c.d. of n and \(\mathbf { \nabla } _ { \mathbf { \mathbf { m } } }\) ， \(P _ { d } = 1\)
Not formalized. none; no complete checked declaration under strict bundle semantics — No K3/Enriques/bielliptic surface object, Kodaira-dimension-zero classification, canonical-class/plurigenus surface invariant, or topological/coherent invariant package exists in P/H. The project’s K3 lattice records only the abstract lattice 3U ⊥ 2E₈, not an algebraic surface. Strict whole-row semantics reject proper subsets and representation by the project’s abstract K3 lattice in place of a K3 surface.
Theorem VIII.2
Theorem VIII.2. A minimal surface of Kodaira dimension \(0\) is exactly one of: an Enriques surface \((p_g,q)=(0,0)\) with \(2K\equiv0\); a bielliptic surface \((0,1)\); a K3 surface \((1,0)\) with \(K\equiv0\); or an Abelian surface \((1,2)\).
Not formalized. none; no complete checked declaration under strict bundle semantics — No K3/Enriques/bielliptic surface object, Kodaira-dimension-zero classification, canonical-class/plurigenus surface invariant, or topological/coherent invariant package exists in P/H. The project’s K3 lattice records only the abstract lattice 3U ⊥ 2E₈, not an algebraic surface. Strict whole-row semantics reject proper subsets and representation by the project’s abstract K3 lattice in place of a K3 surface.
Definition: An Enriques surface is a minimal surface with \(\kappa=0\), \(pg=q=0\), and…
An Enriques surface is a minimal surface with \(\kappa=0\), \(p_g=q=0\), and \(2K\equiv0\).
Not formalized. none; no complete checked declaration under strict bundle semantics — No K3/Enriques/bielliptic surface object, Kodaira-dimension-zero classification, canonical-class/plurigenus surface invariant, or topological/coherent invariant package exists in P/H. The project’s K3 lattice records only the abstract lattice 3U ⊥ 2E₈, not an algebraic surface. Strict whole-row semantics reject proper subsets and representation by the project’s abstract K3 lattice in place of a K3 surface.
Definition: A K3 surface is a minimal surface with \(\kappa=0\), \(pg=1\), \(q=0\), and…
A K3 surface is a minimal surface with \(\kappa=0\), \(p_g=1\), \(q=0\), and \(K\equiv0\).
Not formalized. none; no complete checked declaration under strict bundle semantics — No K3/Enriques/bielliptic surface object, Kodaira-dimension-zero classification, canonical-class/plurigenus surface invariant, or topological/coherent invariant package exists in P/H. The project’s K3 lattice records only the abstract lattice 3U ⊥ 2E₈, not an algebraic surface. Strict whole-row semantics reject proper subsets and representation by the project’s abstract K3 lattice in place of a K3 surface.
Proposition VIII.3
Proposition VIII.3 Let \(s\) be a surface, \(C _ { i }\) irreducible curves on \(s\) and \(m _ { i } > 0\) integers. Set \(\begin{array} { r } { F = \sum m _ { i } C _ { i } } \end{array}\) ，and suppose that for each \(\pmb { i } _ { : }\) \(F . C _ { \bf i } \leqslant 0\) Let \(D = \sum r _ { i } C _ { i }\) with \(r _ { i } \in \mathbb { Z }\) (or even \(r _ { i } \in \mathbb { Q }\) ，and \(D \neq 0\) Then (a) \(D ^ { 2 } \leqslant 0\) ： (b）if \(\pmb { F }\) is connected and \(D ^ { 2 } = 0\) ，one has \(D = r F\) for some \(r \in \mathbb { Q }\) and \(F . C _ { i } = 0\) for all \(\pmb { \mathscr { i } }\) This means that the intersection matrix \(( C _ { i } . C _ { j } )\) is negative semi-definite, and that its kernel has dimension at most 1if \(\pmb { F }\) is connected.
Not formalized. none; no complete checked declaration under strict bundle semantics — This row requires the intersection form/Néron–Severi group and curve/divisor theory of an algebraic surface, which are absent. Generic bilinear-form/lattice code is not a bridge to surface intersection theory. Strict whole-row semantics reject proper subsets and representation by the project’s abstract K3 lattice in place of a K3 surface.
Corollary VIII.4
Corollary VIII.4 Let \(s\) be a surface, \(B\) a smooth curve, and \(p : S B\) a surjective morphism with connected fibres. Suppose that \(p ^ { * } b = F _ { b } =\) \(\sum _ { i } m _ { i } F _ { i }\) for some \(\pmb { b } \in \pmb { B }\) ； then if \(\begin{array} { r } { \dot { D } = \sum _ { i } r _ { i } F _ { i } } \end{array}\) ，with \(r _ { i } \in \mathbb { Z }\) , we have \(D ^ { 2 } \leqslant 0\) ， with equality if and only if \(D = r F _ { b }\) for some \(r \in \mathbb { Q }\)
Not formalized. none; no complete checked declaration under strict bundle semantics — This row requires the intersection form/Néron–Severi group and curve/divisor theory of an algebraic surface, which are absent. Generic bilinear-form/lattice code is not a bridge to surface intersection theory. Strict whole-row semantics reject proper subsets and representation by the project’s abstract K3 lattice in place of a K3 surface.
Corollary VII1.5
Corollary VII1.5 Let \(s\) be a surface, \(g : S S ^ { \prime }\) a surjective morphism to a (possibly singular) projective surface \(S ^ { \prime }\) ，and let \(C _ { i }\) be irreducible curves of \(s\) such that \(\pmb { \mathscr { g } } ( C _ { i } ) = \pmb { \mathscr { p } } \in S ^ { \prime }\) . Then for any \(\begin{array} { r } { D = \sum _ { i } r _ { i } C _ { i } } \end{array}\) ，with \(r _ { i } \in \mathbb { Z }\) , one has \(D ^ { 2 } < 0\) ：
Not formalized. none; no complete checked declaration under strict bundle semantics — This row requires the intersection form/Néron–Severi group and curve/divisor theory of an algebraic surface, which are absent. Generic bilinear-form/lattice code is not a bridge to surface intersection theory. Strict whole-row semantics reject proper subsets and representation by the project’s abstract K3 lattice in place of a K3 surface.
Corollary VII.7
Corollary VIII.7. A minimal surface with \(\kappa=0\) has torsion canonical class of order dividing \(4\) or \(6\): \(K\equiv0\) for K3 and Abelian surfaces, \(2K\equiv0\) for Enriques surfaces, and the bielliptic orders are \(2,3,4,\) or \(6\).
Not formalized. none; no complete checked declaration under strict bundle semantics — No K3/Enriques/bielliptic surface object, Kodaira-dimension-zero classification, canonical-class/plurigenus surface invariant, or topological/coherent invariant package exists in P/H. The project’s K3 lattice records only the abstract lattice 3U ⊥ 2E₈, not an algebraic surface. Strict whole-row semantics reject proper subsets and representation by the project’s abstract K3 lattice in place of a K3 surface.
Construction / invariant
For a K3 surface, \(K\equiv0\) and \(q=0\) imply \(\chi_{\rm top}=24\) and \(b_2=22\).
Not formalized. none; no complete checked declaration under strict bundle semantics — No K3/Enriques/bielliptic surface object, Kodaira-dimension-zero classification, canonical-class/plurigenus surface invariant, or topological/coherent invariant package exists in P/H. The project’s K3 lattice records only the abstract lattice 3U ⊥ 2E₈, not an algebraic surface. Strict whole-row semantics reject proper subsets and representation by the project’s abstract K3 lattice in place of a K3 surface.
Example VIII.8
Example VIII.8. The smooth complete intersections \(S_4\subset\mathbf P^3\), \(S_{2,3}\subset\mathbf P^4\), and \(S_{2,2,2}\subset\mathbf P^5\) have trivial canonical class and are K3 surfaces.
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked Lean formalization of K3 complete-intersection examples, polarized K3 linear systems/projective models, cohomology vanishing, existence/deformation/moduli statements, or their dimensions was found. Strict whole-row semantics reject proper subsets and representation by the project’s abstract K3 lattice in place of a K3 surface.
Lemma VIII.9
Lemma VIII.9 Let \(V \subset \mathbb { P } ^ { n }\) be a d-dimensional complete intersection;then \(H ^ { i } ( V , \mathcal { O } _ { V } ) = 0\) for \(0 < i < d\) ：
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked Lean formalization of K3 complete-intersection examples, polarized K3 linear systems/projective models, cohomology vanishing, existence/deformation/moduli statements, or their dimensions was found. Strict whole-row semantics reject proper subsets and representation by the project’s abstract K3 lattice in place of a K3 surface.
Example VIII.10
Example VII.1O Kummer surfaces Let \(\pmb { A }\) be an Abelian surface; if we choose an origin, \(\pmb { A }\) acquires a group structure. Let \(\pmb { \tau }\) be the involution of \(\pmb { A }\) given by \(a \mapsto - a\) . The fixed points of \(\pmb { \tau }\) are the points of order 2 of the group \(\pmb { A }\) ，which is isomorphic as a group to \(( \mathbb { R } / \mathbb { Z } ) ^ { 4 }\) ; there are thus 16 points of order 2, \(\displaystyle p _ { 1 } , \ldots , p _ { 1 6 } .\) Let \(\epsilon : { \hat { A } } A\) be the blow-up of these 16 points, and \(E _ { i } = \epsilon ^ { - 1 } ( p _ { i } )\) the exceptional curves;the involution \(\pmb { \tau }\) extends to an involution \(\pmb { \sigma }\) of \(\hat { A }\) ; denote by \(X\) the quotient \(X = \hat { A } / \{ 1 , \sigma \}\) ,and let \(\pi : { \hat { A } } \to X\) be the projection.
Not formalized. none; no complete checked declaration under strict bundle semantics — No Abelian-surface blow-up/Kummer quotient/resolution or Kummer quartic surface with sixteen nodes is formalized. Number-theoretic Kummer declarations are unrelated. Strict whole-row semantics reject proper subsets and representation by the project’s abstract K3 lattice in place of a K3 surface.
Proposition VII1.11
Proposition VII1.11 \(X = { \hat { A } } / \{ 1 , \sigma \}\) is a K3 surface, the Kummer surface’of A.
Not formalized. none; no complete checked declaration under strict bundle semantics — No Abelian-surface blow-up/Kummer quotient/resolution or Kummer quartic surface with sixteen nodes is formalized. Number-theoretic Kummer declarations are unrelated. Strict whole-row semantics reject proper subsets and representation by the project’s abstract K3 lattice in place of a K3 surface.
Remark VIII.12(1)
The singular quotient \(A/\{\pm1\}\) has sixteen ordinary double points; its Kummer resolution contracts the sixteen exceptional curves to those nodes.
Not formalized. none; no complete checked declaration under strict bundle semantics — No Abelian-surface blow-up/Kummer quotient/resolution or Kummer quartic surface with sixteen nodes is formalized. Number-theoretic Kummer declarations are unrelated. Strict whole-row semantics reject proper subsets and representation by the project’s abstract K3 lattice in place of a K3 surface.
Remark VIII.12(2)
For the Jacobian of a genus-\(2\) curve, the singular Kummer quotient embeds as a quartic surface in \(\mathbf P^3\) with sixteen ordinary double points.
Not formalized. none; no complete checked declaration under strict bundle semantics — No Abelian-surface blow-up/Kummer quotient/resolution or Kummer quartic surface with sixteen nodes is formalized. Number-theoretic Kummer declarations are unrelated. Strict whole-row semantics reject proper subsets and representation by the project’s abstract K3 lattice in place of a K3 surface.
Remark VIII.12(3)
The sixteen exceptional curves on a Kummer K3 surface form an orthogonal system in \(NS(X)\); together with a polarization they imply \(\rho(X)\ge17\).
Not formalized. none; no complete checked declaration under strict bundle semantics — This row requires the intersection form/Néron–Severi group and curve/divisor theory of an algebraic surface, which are absent. Generic bilinear-form/lattice code is not a bridge to surface intersection theory. Strict whole-row semantics reject proper subsets and representation by the project’s abstract K3 lattice in place of a K3 surface.
Proposition VII.13
Proposition VII.13 Let \(s\) be a K3 surface, \(C \subset S\) a smooth curve of genus \(\pmb { \mathscr { g } }\) . Then (i) \(C ^ { 2 } = 2 g - 2\) and \(h ^ { 0 } ( C ) = g + 1\) (ii）If \({ \pmb g } \geqslant { \pmb 1 }\) the system \(| C |\) is without base points, so defines a morphism \(\phi : S \mathbb { P } ^ { g }\) ； the restriction of \(\phi\) to \(c\) is the canonical morphism \(C \to \mathbb { P } ^ { g - 1 }\) defined \(b y \ | \omega _ { C } |\) (ii)）If \({ \mathfrak { g } } = 2\) ， \(\phi : S \to \mathbb { P } ^ { 2 }\) is a morphism of degree 2, whose branch locus is a sextic of \(\mathbb { P } ^ { 2 }\) (iv) Suppose \(\pmb { \mathscr { g } } \geqslant \mathbf { 3 }\) ; then either \(\phi\) is a birational morphism, and a generic curve of \(| C |\) is non-hyperelliptic; or \(\phi\) is a 2-to-1 morphism to a rational surface (possibly singular) of degree \({ \pmb g } - { \pmb 1 }\) in \({ \mathfrak { P } } ^ { { \mathfrak { g } } }\) . A generic curve of \(\vert C \vert\) is then hyperelliptic. (v）If \(\textbf { \textit { g } } \geqslant \textbf { \textit { 3 } }\) (resp. \({ \pmb { \mathscr { g } } } = { \bf 2 } ,\) ）， the morphism \(\phi ^ { \prime }\) defined by |2Cl (resp. \(| 3 C | )\) is birational.
Not formalized. none; no complete checked declaration under strict bundle semantics — This row requires the intersection form/Néron–Severi group and curve/divisor theory of an algebraic surface, which are absent. Generic bilinear-form/lattice code is not a bridge to surface intersection theory. Strict whole-row semantics reject proper subsets and representation by the project’s abstract K3 lattice in place of a K3 surface.
Example VIII.14 (\(g=3\))
A genus-\(3\) polarized K3 surface with birational polarization maps to a quartic surface in \(\mathbf P^3\).
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked Lean formalization of K3 complete-intersection examples, polarized K3 linear systems/projective models, cohomology vanishing, existence/deformation/moduli statements, or their dimensions was found. Strict whole-row semantics reject proper subsets and representation by the project’s abstract K3 lattice in place of a K3 surface.
Example VIII.14 (\(g=4\))
A genus-\(4\) polarized K3 surface with birational polarization is a degree-\(6\) complete intersection of a quadric and a cubic in \(\mathbf P^4\).
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked Lean formalization of K3 complete-intersection examples, polarized K3 linear systems/projective models, cohomology vanishing, existence/deformation/moduli statements, or their dimensions was found. Strict whole-row semantics reject proper subsets and representation by the project’s abstract K3 lattice in place of a K3 surface.
Example VIII.14 (\(g=5\))
A generic genus-\(5\) polarized K3 surface is a degree-\(8\) complete intersection of three quadrics in \(\mathbf P^5\).
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked Lean formalization of K3 complete-intersection examples, polarized K3 linear systems/projective models, cohomology vanishing, existence/deformation/moduli statements, or their dimensions was found. Strict whole-row semantics reject proper subsets and representation by the project’s abstract K3 lattice in place of a K3 surface.
Definition / comparison
The exceptional divisors contracted by the projective models of polarized K3 surfaces produce the special surface singularities called rational double points.
Not formalized. none; no complete checked declaration under strict bundle semantics — No algebraic-surface rational-double-point/du Val singularity object or contraction theorem was found in P/H or external Lean search. Strict whole-row semantics reject proper subsets and representation by the project’s abstract K3 lattice in place of a K3 surface.
Proposition VII1.15
Proposition VII1.15 For every \({ \textbf { \textit { g } } } \geqslant { \textbf { \textit { 3 } } }\) ， there exist \(\kappa 3\) surfaces \({ \boldsymbol { S } } =\) \(S _ { 2 g - 2 }\) embedded in \({ \mathfrak { P } } ^ { g }\)
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked Lean formalization of K3 complete-intersection examples, polarized K3 linear systems/projective models, cohomology vanishing, existence/deformation/moduli statements, or their dimensions was found. Strict whole-row semantics reject proper subsets and representation by the project’s abstract K3 lattice in place of a K3 surface.
Remark VIII.16
Remark VIII.16. Polarized K3 surfaces of degrees \(2g-2\) for \(g=3,4,5\) form irreducible 19-dimensional families; deformation theory gives a 20-dimensional local K3 moduli space whose algebraic locus is a dense countable union of 19-dimensional subspaces.
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked Lean formalization of K3 complete-intersection examples, polarized K3 linear systems/projective models, cohomology vanishing, existence/deformation/moduli statements, or their dimensions was found. Strict whole-row semantics reject proper subsets and representation by the project’s abstract K3 lattice in place of a K3 surface.
Construction: An order-two line bundle \(L\) with a chosen trivialization…
An order-two line bundle \(L\) with a chosen trivialization \(L^{\otimes2}\simeq\mathcal O_X\) determines an étale double cover \(\widetilde X\to X\) on which the pullback of \(L\) is trivial.
Not formalized. none; no complete checked declaration under strict bundle semantics — P/H has étale-site and generic cover infrastructure, but no checked construction taking an order-two invertible sheaf with L⊗² ≅ O_X to the corresponding finite étale double cover and trivializing its pullback. Strict whole-row semantics reject proper subsets and representation by the project’s abstract K3 lattice in place of a K3 surface.
Proposition VII.17
Proposition VII.17 Let \(s\) be an Enriques surface, and \(\pi : \tilde { S } \to S\) the étale double cover corresponding to the invertible sheaf \({ \mathcal { O } } _ { s } ( K )\) of order two. Then \(\tilde { s }\) isa \(K 3\) surface. Conversely， the quotient of a K3 surface by a fired-point free involution is an Enriques surface.
Not formalized. none; no complete checked declaration under strict bundle semantics — No Enriques canonical double cover, free-involution quotient theorem for K3 surfaces, or explicit three-quadric Enriques construction is formalized. Strict whole-row semantics reject proper subsets and representation by the project’s abstract K3 lattice in place of a K3 surface.
Example VIII.18
Example VIII.18. A smooth complete intersection in \(\mathbf P^5\) of three quadrics \(Q_i(X_0,X_1,X_2)+Q_i\prime(X_3,X_4,X_5)=0\) is a K3 surface. If the two triples of plane conics have no common point, the involution changing the signs of \(X_3,X_4,X_5\) is fixed-point free, so the quotient is an Enriques surface; the generic Enriques surface occurs in this way.
Not formalized. none; no complete checked declaration under strict bundle semantics — No Enriques canonical double cover, free-involution quotient theorem for K3 surfaces, or explicit three-quadric Enriques construction is formalized. Strict whole-row semantics reject proper subsets and representation by the project’s abstract K3 lattice in place of a K3 surface.
Example VII1.19
Example VIII.19 (Reye congruence). For a sufficiently general projective \(3\)-space \(P\) of quadrics in \(\mathbf P^3\), let \(S\) be the variety of lines contained in a pencil of quadrics from \(P\). Under the stated genericity hypotheses on common base points and quadric vertices, this is the Reye-congruence surface used in Proposition VIII.20.
Not formalized. none; no complete checked declaration under strict bundle semantics — No Reye-congruence construction or theorem identifying it as an Enriques surface was found. Strict whole-row semantics reject proper subsets and representation by the project’s abstract K3 lattice in place of a K3 surface.
Proposition VII1.20
Proposition VII1.20 \(\pmb { S }\) is an Enriques surface.
Not formalized. none; no complete checked declaration under strict bundle semantics — No Reye-congruence construction or theorem identifying it as an Enriques surface was found. Strict whole-row semantics reject proper subsets and representation by the project’s abstract K3 lattice in place of a K3 surface.