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

FC12 — Beauville, Complex Algebraic Surfaces.

This chapter contains 1 definition, 2 propositions and 2 examples.

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

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

Which versions of Lean and Mathlib were searched

Canonical block FC12-C07-U001–FC12-C07-U005, five contiguous units.
Search order: project A=12618f8abc2b4852b3da9ab65c3bc547ac4c1f19, P=db584cd6d46c92f209a44c0f1c829460d327499d, H=71a80585ee495fc24472fd0eaffc89d94e4fd8d6, current/open/indexed, packages/Reservoir, broad GitHub Lean and local references.
Result: 0 positive routes, 5 dated unmatched rows. No Kodaira dimension or pluricanonical-map formalization was found; projective/rational-map/complete-intersection ingredients are only proper subsets.

Definition VII.1

FC12-C07-U001 · Chapter VII, source L2195-L2197 · after FC12-C02-U004 · not formalized

Definition VII.1. The Kodaira dimension \(\kappa(V)\) of a smooth projective variety is the maximum of the dimensions of the images of the pluricanonical maps \(\phi_{nK}\); if every \(|nK|\) is empty, then \(\kappa(V)=-\infty\).

Not formalized. none; no complete checked declaration under strict bundle semantics — No complete Lean owner was found for the Kodaira-dimension/pluricanonical statement. P/H has rational maps, projective schemes and canonical generic algebraic infrastructure, but no canonical divisors with pluricanonical linear systems/maps or Kodaira-dimension API; strict whole-row semantics reject reconstruction from those proper subsets.

Example VII.2

FC12-C07-U002 · Chapter VII, source L2199-L2205 · after FC12-C07-U001 · not formalized

Example VII.2. For a smooth curve \(C\) of genus \(g\), \(\kappa(C)=-\infty,0,1\) according as \(g=0,1,\ge2\).

Example VII.3

FC12-C07-U003 · Chapter VII, source L2207-L2213 · after FC12-C03-U001, FC12-C03-U020, FC12-C07-U001 · not formalized

Example VII.3 Let \(s\) be a surface. Then \(\kappa ( S ) = - \infty \Leftrightarrow P _ { n } = 0\) for all \(n \geqslant 1 \Leftrightarrow S\) is ruled (Enriques’ theorem). \(\kappa ( S ) = 0 \Leftrightarrow P _ { n } = 0\) or 1,and there exists \(N\) such that \(P _ { N } = 1\) ： \(\kappa ( S ) = 1 \Leftrightarrow\) there exists \(N\) such that \(P _ { N } \geqslant 2\) ，and for all \(\pmb { n }\) ， \(\phi _ { n K } ( S )\) is at most a curve. \(\kappa ( S ) = 2 \Leftrightarrow\) for some \(N\) ， \(\phi _ { N K } ( S )\) is a surface. In the coming chapters we are going to classify the surfaces with \(\kappa =\) 0,1,2.For the moment we willcontent ourselves with a few examples.

Proposition VII.4

FC12-C07-U004 · Chapter VII, source L2215-L2219 · after FC12-C03-U001, FC12-C07-U001 · not formalized

Proposition VII.4 Let \(c\) ， \(_ D\) be two smooth curves, \(S = C \times D\) . Then If \(\pmb { C }\) or \(D\) is rational, then \(s\) is ruled (i.e. \(\kappa ( S ) = - \infty )\) \(_ { I f C }\) and \(D\) are elliptic, \(\kappa ( S ) = 0\) ： \(_ { I f C }\) is elliptic and \({ \pmb g } ( D ) \geq { \bf 2 }\) \(\kappa ( S ) = 1\) ： \(_ { I f C }\) and \(_ D\) are of genus \(\geqslant 2\) ， then \(\kappa ( S ) = 2\)

Proposition VII.5

FC12-C07-U005 · Chapter VII, source L2235-L2237 · after FC12-C07-U001 · not formalized

Proposition VII.5 Let \(S _ { d _ { 1 } , \dots , d _ { r } }\) denote a surface in \(\mathbb { P } ^ { r + 2 }\) which is the complete intersection of \(\pmb { r }\) hypersurfaces of degrees \(d _ { 1 } , \ldots , d _ { r }\) . Then: The surfaces \(S _ { 2 } , S _ { 3 } , S _ { 2 , 2 }\) are rational (so have \(\kappa = - \infty\) ） The surfaces \(S _ { 4 }\) \(_ { 4 } , S _ { 2 , 3 } , S _ { 2 , 2 , 2 }\) have \(K \equiv 0\) and \(\kappa = 0\) All other surfaces \(S _ { d _ { 1 } , \dots , d _ { \tau } }\) have \(\kappa = 2\) ：