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

FC12 — Beauville, Complex Algebraic Surfaces.

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

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

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

Which versions of Lean and Mathlib were searched

Canonical block FC12-C09-U001–FC12-C09-U010, exactly 10 contiguous units.
Search order: project A=12618f8abc2b4852b3da9ab65c3bc547ac4c1f19, P=db584cd6d46c92f209a44c0f1c829460d327499d, H=71a80585ee495fc24472fd0eaffc89d94e4fd8d6, current/open/indexed, Reservoir/packages, broad GitHub Lean and local references.
Result: 0 positive routes, 10 dated unmatched rows.
Targeted P/H search found no elliptic-surface/fibration object, canonical bundle formula for an elliptic surface, Kodaira-dimension-one pluricanonical theorem, or compatible external Lean implementation. Existing elliptic-curve and scheme infrastructure realizes only proper subsets.

Lemma IX.1

FC12-C09-U001 · Chapter IX, source L2674-L2682 · after FC12-C02-U018, FC12-C03-U001, FC12-C03-U020, FC12-C07-U001 · not formalized

Lemma IX.1 Let \(s\) be a non-ruled minimal surface. (a)f \(K ^ { 2 } > 0\) ， there exists an integer \(\pmb { n _ { 0 } }\) such that \(\phi _ { n K }\) maps \(s\) birationally onto its image for al \(n \geqslant n _ { 0 }\) (b)If \(K ^ { 2 } = 0\) and \(P _ { r } \geqslant 2\) ，write \(r K \equiv Z + M\) ，where \(z\) is the fired part of the system \(\vert r K \vert\) and \(M\) is the mobile part. Then \[ K . Z = K . M = Z ^ { 2 } = Z . M = M ^ { 2 } = 0 \ . \]

Not formalized. none; no complete checked declaration under strict bundle semantics — No complete checked Lean owner was found for this elliptic-surface/Kodaira-dimension-one statement. P/H has elliptic curves, rational maps, products, finite-group and scheme machinery, but no elliptic fibration of surfaces, canonical bundle/pluricanonical linear-system formulas, or the K3/Enriques/bielliptic/Abelian-surface interfaces used by the examples; strict whole-row semantics reject these proper subsets.

Proposition IX.2

FC12-C09-U002 · Chapter IX, source L2696-L2700 · after FC12-C02-U018, FC12-C07-U001 · not formalized

Proposition IX.2 Let \(s\) be a minimal surface with \(\kappa = 1\) (a) We have \(K ^ { 2 } = 0\) ： (b) There is a smooth curve \(B\) and a surjective morphism \(p : S B\) whose generic fibre is an elliptic curve.

Definition: An elliptic surface is a surface admitting a fibration over a curve whose…

FC12-C09-U003 · Chapter IX, source L2704 · not formalized

An elliptic surface is a surface admitting a fibration over a curve whose generic fibre is a smooth curve of genus \(1\).

Proposition IX.3

FC12-C09-U004 · Chapter IX, source L2706-L2716 · after FC12-C02-U005, FC12-C03-U001, FC12-C07-U001, FC12-C09-U003 · not formalized

Proposition IX.3 Let \(s\) be a minimal elliptic surface, \(p : S B\) theelliptic fibration; for \(\boldsymbol { b } \in B\) ，put \(F _ { b } = p ^ { * } [ b ]\) ： (a) We have \(K _ { S } ^ { 2 } = 0\) ： (b） \(s\) is either ruled over an elliptic curve, or a surface with \(\kappa = 0\) ， or a surface with \(\kappa = 1\) (c）If \(\kappa ( S ) = 1\) ， there exists an integer \(d > 0\) such that \[ d K \equiv \sum _ { i } n _ { i } F _ { b _ { i } } \ , n _ { i } \in \mathbb { N } , \ b _ { i } \in B \ . \] For r sufficiently large, the system \(\{ r d K \vert\) is without base points and defines a morphism from \(s\) to \(\mathbb { P } ^ { N }\) which factorizes as \(\boldsymbol { \mathscr { f } } : \mathcal { S } \overset { \mathcal { P } } { \longrightarrow } \boldsymbol { B } \overset { \mathcal { j } } { \longrightarrow } \mathbb { P } ^ { N }\) where \(j\) is an embedding of \(B\) in \(\mathbb { P } ^ { N }\)

Example IX.4(1)

FC12-C09-U005 · Chapter IX, source L2746-L2748 · after FC12-C03-U001, FC12-C09-U003 · not formalized

Products \(E\times\mathbf P^1\), and more generally suitable quotients \((E\times\mathbf P^1)/G\), are ruled elliptic surfaces.

Example IX.4(2)

FC12-C09-U006 · Chapter IX, source L2749 · after FC12-C06-U023, FC12-C09-U003 · not formalized

A bielliptic surface is elliptic and carries the two natural fibrations induced by its two elliptic factors.

Example IX.4(3)

FC12-C09-U007 · Chapter IX, source L2750 · after FC12-C05-U009, FC12-C09-U003 · not formalized

An Abelian surface is elliptic exactly when it fits into an exact sequence \(0\to E\to A\to F\to0\) of elliptic curves.

Example IX.4(4)

FC12-C09-U008 · Chapter IX, source L2751 · after FC12-C08-U004, FC12-C09-U003 · not formalized

K3 surfaces occur in elliptic families, including Weierstrass models with prescribed singular fibres.

Example IX.4(5)

FC12-C09-U009 · Chapter IX, source L2752-L2766 · after FC12-C02-U005, FC12-C08-U003, FC12-C08-U004, FC12-C09-U003 · not formalized

An Enriques surface can carry an elliptic pencil; the exhibited construction descends an invariant genus-one pencil from its K3 cover.

Example IX.5

FC12-C09-U010 · Chapter IX, source L2770 · after FC12-C02-U005, FC12-C07-U001, FC12-C09-U003 · not formalized

Example IX.5 Let \(B\) be a smooth curve, \(\pmb { p } , \pmb { q }\) the two projections of \(B \times \mathbb { P } ^ { 2 }\) onto \(B\) and \(\mathbb { P } ^ { 2 }\) \(| D |\) a base-point free linear system on \(B\) A general divisor \(S \in | p ^ { * } \mathcal { O } _ { B } ( D ) \otimes q ^ { * } \mathcal { O } _ { \mathbb { P } } ( 3 ) |\) is smooth； the restriction \(p : S B\) is a fibration by plane cubics,hence elliptic curves. We have \(K _ { S } \equiv p ^ { * } ( K _ { B } + D )\) ,and when \(\deg ( D ) > 2 - 2 g ( B )\) we have \(\kappa ( S ) = 1\) ：