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

FC12 — Beauville, Complex Algebraic Surfaces.

This chapter contains 1 theorem, 3 propositions, 2 lemmas, 1 corollary, 4 examples, 2 remarks and 1 other statements.

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

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

Which versions of Lean and Mathlib were searched

Canonical block FC12-C10-U001–FC12-C10-U014, exactly 14 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, 14 dated unmatched rows.
No general-type surface/canonical-model, Hodge-theoretic surface invariant, Castelnuovo–de Franchis, Godeaux, or Bogomolov–Miyaoka–Yau formalization was found.
U010 was separately audited against Mathlib’s exterior-power API. Exterior powers and their finrank exist, but the dimension-bound theorem requires a decomposable element in a linear kernel; no Grassmannian/projective-dimension theorem or direct declaration giving Beauville X.7 was found in P/H or broad GitHub Lean search.
N=2026-09-07 marks dated unmatched decisions. Strict whole-row semantics apply uniformly.

Proposition X.1

FC12-C10-U001 · Chapter X, source L2800-L2806 · after FC12-C02-U018, FC12-C07-U001 · not formalized

Proposition X.1. For a minimal surface \(S\), the following are equivalent: \(\kappa(S)=2\); \(K_S^2>0\) and \(S\) is irrational; and \(|nK_S|\) is birational for all sufficiently large \(n\). Such a surface is called a surface of general type.

Not formalized. none; no complete checked declaration under strict bundle semantics — No complete Lean owner was found for this general-type surface/Hodge/cohomological/fibration statement. P/H has generic scheme, differential-form, cohomology-adjacent, exterior-algebra, or rational-map ingredients, but no surface-of-general-type/Kodaira/canonical-model, coherent Hodge-number, Castelnuovo–de Franchis, or Bogomolov–Miyaoka–Yau package. Strict whole-row semantics reject proper subsets and substantive reconstruction.

Remark X.2

FC12-C10-U002 · Chapter X, source L2810 · after FC12-C02-U005, FC12-C08-U021, FC12-C10-U001 · not formalized

Remark X.2 The statement in (ii) can be substantially improved: in fact, \(\vert n K \vert\) is base-point free for \(n \geqslant 4\) ; as soon as \(\pmb { n } \geqslant \pmb { 5 }\) , the morphism \(\phi _ { n K }\) is an isomorphism outside certain rational curves,contracted onto a very simple type of singularity (rational double points). We refer to [Bo] for a detailed analysis.

Example X.3(1)

FC12-C10-U003 · Chapter X, source L2812-L2814 · after FC12-C10-U001 · not formalized

Every smooth complete-intersection surface is of general type except \(S_2,S_3,S_4,S_{2,2},S_{2,3},S_{2,2,2}\).

Example X.3(2)

FC12-C10-U004 · Chapter X, source L2815 · after FC12-C10-U001 · not formalized

A product of curves of genus at least \(2\), and more generally a surface fibred over such a curve with generic fibre of genus at least \(2\), is of general type.

Example X.3(3)

FC12-C10-U005 · Chapter X, source L2817 · after FC12-C10-U001 · not formalized

If \(S\prime\to S\) is surjective and \(S\) is of general type, then \(S\prime\) is of general type.

Example X.3(4)

FC12-C10-U006 · Chapter X, source L2819 · after FC12-C03-U020, FC12-C10-U001 · not formalized

The Godeaux quotient of the Fermat quintic by the displayed free \(\mathbf Z/5\)-action is a surface of general type with \(p_g=q=0\) and \(K^2=1\).

Theorem X.4

FC12-C10-U007 · Chapter X, source L2825 · after FC12-C03-U001, FC12-C03-U020, FC12-C10-U001 · not formalized

Theorem X.4. If \(S\) is non-ruled then \(\chi_{\rm top}(S)\ge0\) and \(\chi(\mathcal O_S)\ge0\); if \(S\) is of general type then \(\chi(\mathcal O_S)>0\).

Fact X.5

FC12-C10-U008 · Chapter X, source L2831-L2841 · after FC12-C03-U020 · not formalized

Fact X.5 Let \(s\) be a surface; then(i) \(b _ { 2 } \geqslant 2 p _ { g }\) ：，(ii）f \(\omega\) is a holomorphic 1-form on \(S , d \omega = 0\) ： The first statement comes from Hodge theory，which gives the more precise formula \(b _ { 2 } = 2 p _ { g } + h ^ { 1 } ( S , \Omega _ { S } ^ { 1 } )\) . The second is much more elemen tary:Stokes’ formula shows that \[ \int _ { S } d \omega \wedge ( \overline { { d \omega } } ) = \int _ { S } d ( \omega \wedge \overline { { d \omega } } ) = 0 . \] As \(d \omega\) isa \(( 2 , 0 )\) -form,this implies \(d \omega = 0\)

Lemma X.6

FC12-C10-U009 · Chapter X, source L2843 · after FC12-C03-U020 · not formalized

Lemma X.6 Let \(s\) be a surface with \(\chi _ { \mathsf { t o p } } ( S ) < 0\) ; then \(s\) has an étale cover \(S ^ { \prime } \to S\) such that \(p _ { g } ( S ^ { \prime } ) \leqslant 2 q ( S ^ { \prime } ) - 4\)

Lemma X.7

FC12-C10-U010 · Chapter X, source L2851 · not formalized

Lemma X.7 Let \(V\) ， W be two finite dimensional complex vector spaces, and \(\phi : \wedge ^ { 2 } V \to W\) a homomorphism. Then ifdim \(W \leqslant 2 \dim V { - } 4 .\) there exist two linearly independent vectors \(\pmb { v }\) \(\pmb { v } ^ { \prime } \in V\) such that \(\phi ( v \wedge v ^ { \prime } ) = 0\)

Not formalized. none; no complete checked declaration under strict bundle semantics — Mathlib has exterior powers and proves finrank (⋀² V)=choose (finrank V) 2, but no checked theorem was found that the stated codomain-dimension bound forces the kernel of φ : ⋀²V → W to contain a nonzero decomposable wedge of two linearly independent vectors. Establishing that requires the missing Grassmannian/projective-dimension argument, so generic exterior-algebra ingredients are only proper subsets. Strict whole-row semantics reject proper subsets and substantive reconstruction.

Corollary X.8

FC12-C10-U011 · Chapter X, source L2863 · after FC12-C03-U020 · not formalized

Corollary X.8. If \(q(S)>0\), then \(\chi(\mathcal O_S)\ge0\); equivalently \(p_g(S)\ge q(S)-1\).

Proposition X.9

FC12-C10-U012 · Chapter X, source L2867 · not formalized

Proposition X.9 Let \(s\) be a surface having two linearly independent 1-forms \(\omega _ { 1 }\) ， \(\omega _ { 2 } \in H ^ { 0 } ( S , \Omega _ { S } ^ { 1 } )\) such that \(\omega _ { 1 } \wedge \omega _ { 2 } = 0\) . Then there is \({ \pmb a }\) smooth curve \(B\) of genus \({ \textbf { \textit { g } } } \geqslant { \textbf { \textit { 2 } } }\) ， a surjective morphism \(p : S B\) with connected fibres，and two 1-forms \(\alpha _ { 1 }\) ， \(\alpha _ { 2 } \in H ^ { 0 } ( B , \Omega _ { B } ^ { 1 } )\) such that \(\omega _ { 1 } = p ^ { * } \alpha _ { 1 }\) ， \(\omega _ { 2 } = p ^ { * } \alpha _ { 2 }\) ：

Proposition X.10

FC12-C10-U013 · Chapter X, source L2877 · after FC12-C03-U020 · not formalized

Proposition X.10 Let \(s\) be a surface, and \(p : S B\) a surjective morphism of \(s\) to a smooth curve; suppose that \(\pmb { p }\) has connected fibres, and \(F _ { \eta }\) is the generic fibre. Then \(\chi _ { \mathsf { t o p } } ( S ) \geqslant \chi _ { \mathsf { t o p } } ( B ) \chi _ { \mathsf { t o p } } ( F _ { \eta } )\)

Remark X.11

FC12-C10-U014 · Chapter X, source L2911 · after FC12-C01-U017, FC12-C03-U001 · not formalized

Remark X.11 In view of Noether’s formula, \(\chi _ { \mathsf { t o p } } ( S ) \geqslant 0\) is equivalent to the inequality \(K _ { S } ^ { 2 } \leqslant 1 2 \chi ( \mathcal { O } _ { S } )\) . For a non-ruled surface,the very much deeper inequality \(K ^ { 2 } \leqslant 9 \chi ( \mathcal { O } _ { S } )\) was proved by Bogomolov and Miyaoka, and independently by S.T.Yau.