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

FC12 — Beauville, Complex Algebraic Surfaces.

This chapter contains 2 definitions, 5 theorems, 3 propositions, 3 lemmas, 1 corollary, 2 remarks and 2 other statements.

Of the 18 statements checked against Lean, 0 are formalized somewhere and 18 are not.

Status	Statements	Share	What it means
not formalized	18	100%	A documented search found no Lean statement of it anywhere.
checked in total	18

Which versions of Lean and Mathlib were searched

Canonical source block: FC12 Beauville, Chapter V, FC12-C05-U001–FC12-C05-U018, exactly 18 unique contiguous rows.
Search order: project A=12618f8abc2b4852b3da9ab65c3bc547ac4c1f19, P=db584cd6d46c92f209a44c0f1c829460d327499d, H=71a80585ee495fc24472fd0eaffc89d94e4fd8d6, then current/open/indexed Mathlib, Reservoir/packages, broad GitHub Lean, and local mapped-source/reference corpora.
C05 has 0 positive routes and 18 dated unmatched rows.
P/H has rational maps/birationality but no plurigenera/Kodaira/minimal-surface rationality criteria, so Castelnuovo/Lüroth surface consequences and minimal rational-surface classification remain unmatched.
The project does contain LeanCategories/Lattices/Valued/ComplexTorus.lean, providing a genuine complex-torus object and an abelian-variety predicate. Beauville’s U009/U010 rows bundle substantially more: projectivity equivalence, translation-trivialized tangent/cotangent bundles, H₁, and classification of torus morphisms. Those missing clauses prevent a partial project-existing route.
No Albanese variety/morphism, Stein factorization, or Albanese fibration package was found. Broad GitHub search found an axiom-free analytic Albanese/Jacobian universal property for curves in mrdouglasny/jacobian-challenge, but it is not an implementation of the algebraic Albanese of an arbitrary smooth projective variety and therefore is not a reference route for U011–U015.
N=2026-09-07 marks dated unmatched decisions. Strict whole-row semantics apply uniformly.

Theorem V.1

FC12-C05-U001 · Chapter V, source L1375 · after FC12-C03-U020 · not formalized

Theorem V.1 (Castelnuovo’s Rationality Criterion) Let \(s\) be a surface with \(q = P _ { 2 } = 0\) . Then \(s\) is rational.

Not formalized. none; no complete checked declaration under strict bundle semantics — This is a surface rationality/minimal-model/intersection theorem depending on plurigenera, canonical divisors, blow-ups, or ruled-surface classification; the required surface layer is absent in P/H. Strict whole-row semantics reject proper subsets and reconstruction from rational maps, generic quotients/Lie groups, or abstract universal properties.

Remark V.2

FC12-C05-U002 · Chapter V, source L1377-L1379 · after FC12-C03-U020 · not formalized

Remark V.2. Castelnuovo’s hypothesis \(P_2=0\) implies \(p_g=0\), but the weaker condition \(q=p_g=0\) does not imply rationality.

Definition V.3

FC12-C05-U003 · Chapter V, source L1381-L1387 · after FC12-C02-U004 · not formalized

Definition V.3. An \(n\)-dimensional variety is unirational if it admits a dominant rational map \(\mathbf P^n\dashrightarrow V\), and rational if it is birational to \(\mathbf P^n\).

Not formalized. none; no complete checked declaration under strict bundle semantics — Mathlib has dominant/birational rational maps of schemes, but no projective-space variety/rationality package at the exact Beauville interface and no Lüroth/unirational-surface theorem. The generic rational-map predicates do not own the full definition/theorem row. Strict whole-row semantics reject proper subsets and reconstruction from rational maps, generic quotients/Lie groups, or abstract universal properties.

Theorem V.4

FC12-C05-U004 · Chapter V, source L1389 · after FC12-C05-U003 · not formalized

Theorem V.4 (Liroth) Every unirational curve is rational.

Corollary V.5

FC12-C05-U005 · Chapter V, source L1395 · after FC12-C05-U003 · not formalized

Corollary V.5. Every unirational surface is rational.

Proposition V.6

FC12-C05-U006 · Chapter V, source L1405 · after FC12-C02-U018, FC12-C03-U020 · not formalized

Proposition V.6 Let \(s\) be a minimal surface with \(q = P _ { 2 } = 0\) . Then there exists a smooth rational curve \(c\) on \(s\) such that \(C ^ { 2 } \geqslant 0\)

Lemma V.8

FC12-C05-U007 · Chapter V, source L1419 · after FC12-C02-U018 · not formalized

Lemma V.8 Let \(s\) be a minimal surface with \(K ^ { 2 } < 0\) . For all \({ \pmb a } > { \bf 0 }\) ， there exists an effective divisor \(D\) on \(s\) such that \(K . D \leqslant - a\) \(| K + D | =\) \(\emptyset\) ：

Theorem V.10

FC12-C05-U008 · Chapter V, source L1497 · after FC12-C02-U018, FC12-C04-U002 · not formalized

Theorem V.10 Let \(S\) be a minimal rational surface. Then \(s\) is isomorphic to \(\mathbb { P } ^ { 2 }\) or to one of the surfaces \(\mathbb { F } _ { n }\) (IV.1) for \(n \neq 1\) ：

Reminder V.11

FC12-C05-U009 · Chapter V, source L1523-L1531 · not formalized

Reminder V.11. A complex torus is \(V/\Gamma\) for a complex vector space \(V\) and a lattice \(\Gamma\); a projective complex torus is an Abelian variety. Its tangent and cotangent bundles are translation-trivialized and \(H_1(V/\Gamma,\mathbf Z)=\Gamma\).

Not formalized. none; no complete checked declaration under strict bundle semantics — The project has a bundled analytic ComplexTorus and an IsAbelianVariety predicate, but this row additionally identifies projective complex tori with abelian varieties, trivializes tangent/cotangent bundles by translations, and computes integral H₁; those clauses are not formalized together. Strict whole-row semantics reject proper subsets and reconstruction from rational maps, generic quotients/Lie groups, or abstract universal properties.

Proposition V.12

FC12-C05-U010 · Chapter V, source L1533 · after FC12-C05-U009 · not formalized

Proposition V.12 Let \(T _ { 1 } = V _ { 1 } / \Gamma _ { 1 }\) ， \(T _ { 2 } = V _ { 2 } / \Gamma _ { 2 }\) be two complex tori, \(u : T _ { 1 } \to T _ { 2 }\) a morphism. Then \(\pmb { u }\) is composed of a translation and \(\pmb { a }\) morphism \(a : T _ { 1 } T _ { 2 }\) which is a group homomorphism; \(\mathbf { a }\) is induced by a linear map \(\overline { { a } } : V _ { 1 } V _ { 2 }\) such that \(\overline { { { a } } } ( \Gamma _ { 1 } ) \subset \Gamma _ { 2 }\) . In particular a is determined by \(u ^ { * } : H ^ { 0 } ( T _ { 2 } , \Omega _ { T _ { 2 } } ^ { 1 } ) H ^ { 0 } ( T _ { 1 } , \Omega _ { T _ { 1 } } ^ { 1 } )\)

Not formalized. none; no complete checked declaration under strict bundle semantics — No checked theorem was found classifying morphisms of complex tori as translation plus a lattice-compatible complex-linear homomorphism and identifying them from pullback on holomorphic 1-forms. Strict whole-row semantics reject proper subsets and reconstruction from rational maps, generic quotients/Lie groups, or abstract universal properties.

Theorem V.13

FC12-C05-U011 · Chapter V, source L1537-L1541 · after FC12-C05-U009 · not formalized

Theorem V.13 Let \(X\) be a smooth projective variety. There erists an Abelian variety \(A\) and a morphism \(\alpha : X A\) with the following universal property: for any complex torus \(_ T\) and any morphism \(f : X \to T\) ， there exists a unique morphism \({ \tilde { f } } : A \to T\) such that \(\tilde { f } \circ \alpha = f\) ： The Abelian variety \(A\) ， determined up to isomorphism by this condition，is called the Albanese variety of \(X\) ，and written Alb \(( X )\) .The morphism \(\pmb { \alpha }\) induces an isomorphism \(\alpha ^ { * } : H ^ { 0 } ( A , \Omega _ { A } ^ { 1 } ) H ^ { 0 } ( X , \Omega _ { X } ^ { 1 } )\) ：

Not formalized. none; no complete checked declaration under strict bundle semantics — No algebraic Albanese variety/functor or Albanese morphism of smooth projective varieties/surfaces is formalized in P/H or the project. A current external Jacobian project formalizes an analytic Albanese-type universal property only for curves/Jacobians, not this arbitrary-variety row. Strict whole-row semantics reject proper subsets and reconstruction from rational maps, generic quotients/Lie groups, or abstract universal properties.

Remarks V.14

FC12-C05-U012 · Chapter V, source L1583-L1593 · after FC12-C05-U011 · not formalized

Remarks V.14. The Albanese variety satisfies \(\dim\operatorname{Alb}(X)=h^0(X,\Omega_X^1)\), is functorial for morphisms, is generated by the image of \(X\), agrees with the Jacobian for curves, and the Albanese map induces the expected quotient on \(H_1\).

Proposition V.15

FC12-C05-U013 · Chapter V, source L1595-L1597 · after FC12-C03-U020, FC12-C05-U011 · not formalized

Proposition V.15. If the Albanese image of a surface \(S\) is a curve \(C\), then \(C\) is smooth of genus \(q(S)\) and the fibres of the Albanese map are connected.

Definition / convention

FC12-C05-U014 · Chapter V, source L1597 · after FC12-C05-U011 · not formalized

When the image of the Albanese map of a surface is a curve, the induced map to that curve is called the Albanese fibration.

Lemma V.16

FC12-C05-U015 · Chapter V, source L1599 · after FC12-C05-U011 · not formalized

Lemma V.16 Suppose that \(\pmb { \alpha }\) factorizes as \(S \ { \stackrel { f } { \to } } \ T \ { \stackrel { j } { \to } } \ \mathbf { A l b } ( S )\) ，with \(\pmb { f }\) surjective. Then \({ \tilde { \pmb { j } } } : \mathbf { A l b } ( T ) \mathbf { A l b } ( S )\) is an isomorphism.

Fact V.17

FC12-C05-U016 · Chapter V, source L1613 · not formalized

Fact V.17 (Stein factorization)

Not formalized. none; no complete checked declaration under strict bundle semantics — Targeted P/H search found no Stein factorization theorem for morphisms of schemes/varieties at Beauville’s interface. Strict whole-row semantics reject proper subsets and reconstruction from rational maps, generic quotients/Lie groups, or abstract universal properties.

Lemma V.18

FC12-C05-U017 · Chapter V, source L1621 · after FC12-C03-U020, FC12-C05-U011 · not formalized

Lemma V.18 Let \(s\) be a surface with \(\pmb { p _ { g } } = 0\) \(q \geqslant 1\) \(\pmb { \alpha } : S \mathbf { A l b } ( S )\) its Albanese map. Then \(\alpha ( S )\) is a curve.

Theorem V.19

FC12-C05-U018 · Chapter V, source L1625 · after FC12-C02-U018, FC12-C03-U001 · not formalized

Theorem V.19 Let \(s\) \(S ^ { \prime }\) be two non-ruled minimal surfaces. Then every birational map from \(S ^ { \prime }\) to \(\boldsymbol { s }\) is an isomorphism. In particular, every non-ruled surface admits a unique minimal model (up to isomorphism); the group of birational maps from a non-ruled minimal surface to itself coincides with the group of automorphisms of the surface.