FC12 — Beauville, Complex Algebraic Surfaces, 2nd ed.

FC12 — Beauville, Complex Algebraic Surfaces.

This chapter contains 1 definition, 3 theorems, 4 propositions, 8 lemmas, 2 corollaries, 5 examples and 1 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

Which versions of Lean and Mathlib were searched

Canonical block: FC12-C06-U001–FC12-C06-U024, exactly 24 contiguous units.
Search order: project A=12618f8abc2b4852b3da9ab65c3bc547ac4c1f19, pinned Mathlib P=db584cd6d46c92f209a44c0f1c829460d327499d, current Mathlib H=71a80585ee495fc24472fd0eaffc89d94e4fd8d6, then current/open/indexed services, packages/Reservoir, broad GitHub Lean search, and local mapped/reference corpora.
Result: 0 positive routes and 24 dated unmatched rows.
P/H has substantial generic elliptic-curve, finite-group, quotient, and étale infrastructure, but no algebraic surface-fibration theory or the chapter’s classification/invariant packages. Targeted searches also found no compatible external Lean implementation of those missing statements.
Strict whole-row semantics apply uniformly; generic ingredients are not promoted across missing surface-level interfaces.

Lemma VI.1

FC12-C06-U001 · Chapter VI, source L1681-L1683 · after FC12-C02-U018, FC12-C03-U020 · not formalized

Lemma VI.1 (a) Let \(\boldsymbol { S }\) be a surface with \(p _ { g } = 0\) \(q \geqslant 1\) . Then \(K ^ { 2 } \leqslant 0\) ，and \(K ^ { 2 } < 0\) unless \(q = 1\) and \(b _ { 2 } = 2\) (b) Let \(s\) be a minimal surface with \(K ^ { 2 } < 0\) ; then \({ \pmb p } _ { \pmb g } = 0\) and \(q \geqslant 1\)

Not formalized. none; no complete checked declaration under strict bundle semantics — No complete checked Lean owner was found for this chapter-level surface/fibration/classification statement after project, pinned/current Mathlib, package/indexed, broad GitHub, and local-reference search. The available generic scheme, elliptic-curve, finite-group, quotient, cohomology, and étale ingredients realize only proper subsets of the source row; strict whole-row semantics therefore keep it unmatched.

Proposition VI.2

FC12-C06-U002 · Chapter VI, source L1695 · after FC12-C02-U018, FC12-C03-U001 · not formalized

Proposition VI.2 Let \(s\) be minimal with \(K ^ { 2 } < 0\) . Then \(s\) is ruled.

Lemma VI.3

FC12-C06-U003 · Chapter VI, source L1775 · after FC12-C03-U020 · not formalized

Lemma VI.3 Let \(\pi : S ^ { \prime } \to S\) be an étale map of surfaces, deg \({ \pmb { \pi } } = { \pmb { n } }\) ，Then \(K _ { S ^ { \prime } } ^ { 2 } = n K ^ { 2 }\) ， \(\chi _ { \sf t o p } ( S ^ { \prime } ) = n \chi _ { \sf t o p } ( S )\) and \(\chi ( \mathcal { O } _ { S ^ { \prime } } ) = n \chi ( \mathcal { O } _ { S } )\) ：

Lemma VI.4

FC12-C06-U004 · Chapter VI, source L1781-L1785 · not formalized

Lemma VI.4 Let \(\boldsymbol { S }\) be a surface, \(B\) a smooth curve and \(p : S B\) a surjective morphism. Let \(\Sigma \subset B\) be the (finite) set of points over which \(\pmb { p }\) is not smooth,and let \(\eta \in B - \Sigma\) .Let \(F _ { b }\) denote \(p ^ { - 1 } ( b ) , b \in B\) . Then \[ \chi _ { \mathrm { t o p } } ( S ) = \chi _ { \mathrm { t o p } } ( B ) \chi _ { \mathrm { t o p } } ( F _ { \eta } ) + \sum _ { s \in \Sigma } ( \chi _ { \mathrm { t o p } } ( F _ { s } ) - \chi _ { \mathrm { t o p } } ( F _ { \eta } ) ) \ . \]

Lemma VI.5

FC12-C06-U005 · Chapter VI, source L1815 · not formalized

Lemma VI.5 Let \(C\) be a reduced (but possibly reducible) curve. Then \(\chi _ { \mathrm { t o p } } ( C ) \geqslant 2 \chi ( \mathcal { O } _ { C } )\) ； equality holds if and only if \(C\) is smooth.

Proposition VI.6

FC12-C06-U006 · Chapter VI, source L1835 · after FC12-C02-U018, FC12-C03-U020, FC12-C05-U011 · not formalized

Proposition VI.6 Let \(s\) be a minimal surface with \({ \pmb p } _ { \pmb g } = { \pmb 0 }\) ， \({ \pmb q } = 1\) and \(K ^ { 2 } = 0\) ， \(p : S B\) the Albanese map ( \(\mathbfcal { B }\) is an elliptic curve) and \(\pmb { g }\) the genus of a generic fibre of \(\pmb { p }\) Then if \({ \textbf { \textit { g } } } \geqslant { \textbf { \textit { 2 } } }\) \(\pmb { p }\) is smooth,and if \(g = 1\) ， then the singular fibres of \(\pmb { p }\) are of the form \(F _ { \delta } = n E\) ， where \(\pmb { { \cal E } }\) is a smooth elliptic curve.

Lemma VI.7

FC12-C06-U007 · Chapter VI, source L1851-L1857 · not formalized

Lemma VI.7 Let \(p : S B\) be a morphism from a surface onto a smooth curve whose fibres are either smooth or multiples of smooth curves. Then there is a ramified Galois cover \(q : B ^ { \prime } \to B\) with Galois group \(G\) ， say，a surface \(S ^ { \prime }\) and a commutative diagram \[ \begin{array} { r l } { S ^ { \prime } } & { { } \xrightarrow { q ^ { \prime } } \quad S } \\ { p ^ { \prime } { \downarrow } } & { } \begin{array} { r l } { \begin{array} { r l } { \underline { p ^ { \prime } } } & { { } } \end{array} } & { \begin{array} { r l } { p ^ { \prime } } & { { } } \\ { B ^ { \prime } } & { { } \xrightarrow { q ^ { \prime } } } & { { } B } \end{array} } \end{array} \end{array} \] such that the action of \(G\) on \(\pmb { B ^ { \prime } }\) lifts to \(S ^ { \prime }\) ， \(\pmb q ^ { \prime }\) induces an isomorphism \(S ^ { \prime } / G \tilde { } S\) and \(\pmb { p ^ { \prime } }\) is smooth.

Lemma VI.7’

FC12-C06-U008 · Chapter VI, source L1861 · after FC12-C06-U007 · not formalized

Lemma VI.7’. After the indicated cyclic base change \(z\mapsto z^n\) of a smooth multiple fibre \(nC\), normalization removes the fibre multiplicity and produces an étale neighbourhood of the reduced fibre.

Proposition VI.8

FC12-C06-U009 · Chapter VI, source L1875 · not formalized

Proposition VI.8 Let \(p : S B\) be a smooth morphism from a surface to a curve, and \(\pmb { F }\) a fibre of \(\pmb { p }\) . Assume either that \(g ( B ) = 1\) and \(g ( F ) \geqslant 1\) ，or that \(g ( F ) = 1\) . Then there erists an etale cover \(B ^ { \prime }\) such that the fibration \(p ^ { \prime } : S ^ { \prime } = S \times _ { B } B ^ { \prime } \to B ^ { \prime }\) is trivial, i.e. \(S ^ { \prime } \cong B ^ { \prime } \times F\) ： Furthermore, we can take the cover \(B ^ { \prime } B\) to be Galois with group \(G\) ， say,so that \(S \cong ( B ^ { \prime } \times F ) / G\)

Corollary VI.9

FC12-C06-U010 · Chapter VI, source L1895-L1897 · after FC12-C02-U018, FC12-C03-U001, FC12-C03-U020 · not formalized

Corollary VI.9. A minimal non-ruled surface with \(p_g=0\), \(q=1\), and \(K^2=0\) is a quotient \((B\times F)/G\) with \(B/G\) elliptic; if \(g(F)\ge2\), then \(B\) is elliptic and \(G\) acts on it by translations.

Lemma VI.10

FC12-C06-U011 · Chapter VI, source L1899-L1902 · not formalized

Lemma VI.10 Let \(B\) ， \(\pmb { F }\) be curves of genus \(\geqslant 1\) and \(G\) a group of automorphisms of \(B\) acting on \(B \times F\) compatibly with its action on \(B\) ： (i)If \(g ( F ) \geqslant 2\) ,then \(\pmb { G }\) acts on \(\pmb { F }\) and \(g ( b , f ) = ( g b , g f )\) for \({ \pmb g } \in G\) ， \(b \in B , f \in F\) (ii)If \(g ( F ) = 1\) , there is an etale cover \(\tilde { B }\) of \(B\) and a group \(H\) acting on \(\tilde { B }\) and \(\pmb { F }\) such that \({ \tilde { B } } / H \cong B / G\) and \(( \tilde { B } \times F ) / H \cong ( B \times F ) / G\)

Lemma VI.11

FC12-C06-U012 · Chapter VI, source L1966 · not formalized

Lemma VI.11 Let \(X\) be a smooth variety and \(G\) a finite subgroup of Aut \(X\) Let \(\pi : X \to Y = X / G\) denote the natural projection， and assume that \(Y\) is smooth. Then the \(G\) -invariant \(\pmb { k }\) -fold \(\pmb { p }\) -forms \({ \pmb { \alpha } } \in\) \(H ^ { 0 } ( X , ( \Omega _ { X } ^ { p } ) ^ { \otimes { \bf k } } )\) are the forms \(\pi ^ { * } \omega\) ， where \(\omega\) isa \(\pmb { k }\) -fold rational \(\pmb { p }\) -form on \(Y\) such that \(\pi ^ { * } \omega\) is regular on \(X\) ：

Example VI.12(1)

FC12-C06-U013 · Chapter VI, source L1970-L1974 · not formalized

For an étale quotient \(\pi:X\to Y=X/G\), pullback identifies tensor differential forms on \(Y\) with the \(G\)-invariant forms on \(X\).

Example VI.12(2)

FC12-C06-U014 · Chapter VI, source L1976-L1992 · not formalized

For a quotient of smooth curves, a meromorphic differential downstairs is regular exactly when its pullback is regular upstairs; the local ramification formula gives the precise pole-order criterion.

Example VI.12(3)

FC12-C06-U015 · Chapter VI, source L1994-L2002 · not formalized

A \(G\)-invariant holomorphic \(p\)-form on a smooth quotient descends; averaging/trace provides the inverse to pullback on invariant forms.

Theorem VI.13

FC12-C06-U016 · Chapter VI, source L2006-L2010 · after FC12-C02-U018, FC12-C03-U001, FC12-C03-U020 · not formalized

Theorem VI.13 Let \(s\) be a minimal non-ruled surface with \({ \pmb p } _ { \pmb g } = { \pmb 0 }\) \(q \geqslant 1\) . Then \(S \cong ( B \times F ) / G\) ,where \(B\) ， \(\pmb { F }\) are smooth irrational curves, \(\pmb { G }\) is a finite group acting faithfully on \(B\) and \(\pmb { F }\) ， \(B / G\) is elliptic, \(F / G\) is rational and one of the following conditions holds: I: \(B\) is elliptic, and so \(\pmb { G }\) is a group of translations of \(B\) II: \(\pmb { F }\) is elliptic, and \(\pmb { G }\) acts freely on \(B \times F\) Conversely, every surface with these properties is minimal with \({ \pmb p } _ { \pmb g } = 0\) ， \(q = 1\) ， \(K ^ { 2 } = 0\) and is non-ruled.

Example VI.14(1)

FC12-C06-U017 · Chapter VI, source L2048-L2050 · after FC12-C06-U016 · not formalized

Case I surfaces in Theorem VI.13 are constructed from a product \(B\times F\) by a finite group acting freely diagonally, with \(B/G\) elliptic and \(F/G\) rational.

Example VI.14(2)

FC12-C06-U018 · Chapter VI, source L2052-L2054 · after FC12-C06-U016 · not formalized

Case II occurs via a \((\mathbf Z/2)^2\)-quotient of a product of curves with the indicated free diagonal action and prescribed quotient genera.

Proposition VI.15

FC12-C06-U019 · Chapter VI, source L2058-L2062 · after FC12-C03-U020, FC12-C06-U016 · not formalized

Proposition VI.15 Let \(S = ( B \times F ) / G\) be a surface satisfying the conditions of Theorem VI.13. (1) \(P _ { 4 } \neq 0\) or \(P _ { 6 } \neq 0\) ; in particular \(P _ { 1 2 } \neq 0\) (2）If \(B\) or \(\pmb { F }\) is not elliptic, then there is an infinite increasing sequence \(\{ n _ { i } \}\) of integers such that the sequence \(\{ P _ { n _ { i } } \}\) tends to infinity. (3）If \(B\) and \(\pmb { F }\) are elliptic, then \(4 K \equiv 0\) or \(6 K \equiv 0\) ; in particular, \(1 2 K \equiv 0\) ：

Theorem VI.16

FC12-C06-U020 · Chapter VI, source L2111-L2127 · not formalized

Theorem VI.16. Every automorphism of an elliptic curve is a translation followed by a group automorphism; the possible nontrivial group automorphisms have orders \(2,3,4,\) or \(6\), with the extra orders occurring only for the special \(j\)-invariants.

Theorem VI.17

FC12-C06-U021 · Chapter VI, source L2129 · after FC12-C03-U001, FC12-C03-U020 · not formalized

Theorem VI.17 (Enriques） Let \(s\) be a surface with \(P _ { 4 } = P _ { 6 } = 0\) (or \(P _ { 1 2 } = 0\) .Then \(s\) is ruled.

Corollary V1.18

FC12-C06-U022 · Chapter VI, source L2133-L2138 · after FC12-C02-U020, FC12-C03-U001 · not formalized

Corollary V1.18 The following conditions on a surface \(s\) are equivalent: (1) \(s\) is ruled; (2) there is a non-exceptional curve \(c\) on \(s\) such that \(K . C < 0\) (3) for every divisor \(D\) on \(s\) \(\vert D + n K \vert = \emptyset\) for \(n \gg 0\) (adjunction terminates’); (4) \(P _ { n } = 0\) for all \(\pmb { n }\) (5) \(P _ { 1 2 } = 0\)

Definition VI.19

FC12-C06-U023 · Chapter VI, source L2148-L2159 · not formalized

Definition VI.19. A bielliptic surface is a quotient \((E\times F)/G\) with \(E,F\) elliptic, \(G\) acting by translations on \(E\), and \(F/G\simeq\mathbf P^1\).

List VI.20

FC12-C06-U024 · Chapter VI, source L2161-L2169 · after FC12-C06-U023 · not formalized

List VI.20 (Bagnera–de Franchis). Every bielliptic surface is one of seven quotient types, with \(G\) equal to \(\mathbf Z/2\), \((\mathbf Z/2)^2\), \(\mathbf Z/4\), \(\mathbf Z/4\oplus\mathbf Z/2\), \(\mathbf Z/3\), \((\mathbf Z/3)^2\), or \(\mathbf Z/6\) acting as specified; the canonical class has order \(2,3,4,\) or \(6\) accordingly.