FC12 — Beauville, Complex Algebraic Surfaces, 2nd ed.
FC12 — Beauville, Complex Algebraic Surfaces.
This chapter contains 6 definitions, 3 theorems, 3 propositions, 4 lemmas, 1 corollary, 3 examples, 1 construction and 1 remark.
Of the 22 statements checked against Lean, 0 are formalized somewhere and 22 are not.
| Status | Statements | Share | What it means |
|---|---|---|---|
| not formalized | 22 | 100% | A documented search found no Lean statement of it anywhere. |
| checked in total | 22 |
- Canonical source block: FC12 Beauville, Chapter II,
FC12-C02-U001–FC12-C02-U022, exactly 22 unique contiguous rows from FC12 — Beauville, Complex Algebraic Surfaces, 2nd ed.. - Search order: project at
A=12618f8abc2b4852b3da9ab65c3bc547ac4c1f19, pinned MathlibP=db584cd6d46c92f209a44c0f1c829460d327499d, currentH=71a80585ee495fc24472fd0eaffc89d94e4fd8d6, then current/open Mathlib, indexed services, package/Reservoir discovery, broad GitHub Lean search, and local mapped-source/reference corpora. - C02 has 0 positive routes and 22 dated
unmatchedrows. - P and H contain a mature
Scheme.RationalMap/birational layer, including dense domains and composition. This does not promote U004 because Beauville’s row bundles the rational-map definition with surface-specific finiteness of indeterminacy and divisor/linear-system pullback/image operations that are absent. - No scheme blow-up exists at P/H.
Mathlib/RingTheory/ReesAlgebra.leanmentions blow-ups only as future motivation; targeted source search found no geometric blow-up, exceptional divisor, strict transform, Castelnuovo contraction, or factorization of surface birational morphisms. Consequently the blow-up/minimal-model rows are genuine unmatched mappings, not aliases to Rees algebra. - No divisor linear-system package or Cremona transformation formalization was found in the project, P/H, packages, or broad GitHub search.
- U022 is topology-only but still unmatched: no checked theorem with its compact restriction plus local-homeomorphism hypotheses and uniform neighborhood conclusion was found; the generic local-homeomorphism and compactness ingredients would require a nontrivial finite-subcover argument.
N=2026-09-07marks dated unmatched decisions. Strict whole-row semantics apply uniformly.
Definition / construction II.1
II.1 (blow-ups). The blow-up \(\epsilon:\widehat S\to S\) of a smooth surface at \(p\) is an isomorphism off \(p\), with exceptional curve \(E\simeq\mathbf P^1\) parametrizing tangent directions at \(p\); the closure of the inverse image of \(C\setminus\{p\}\) is the strict transform of a curve \(C\).
Not formalized. none; no complete checked declaration under strict bundle semantics — Pinned/current Mathlib has no scheme blow-up construction (the Rees algebra file explicitly leaves geometric blow-ups to future work), hence no exceptional divisor/strict-transform, blow-up intersection/Picard formulas, factorization, elimination of indeterminacy, minimal-surface, or Castelnuovo package needed for this row. Strict whole-row semantics reject proper subsets and substantive reconstruction from rational-map, Rees-algebra, projective-space, or topological ingredients.
Lemma I1.2
Lemma I1.2 \(\epsilon ^ { * } C = \hat { C } + m E\) ：
Not formalized. none; no complete checked declaration under strict bundle semantics — Pinned/current Mathlib has no scheme blow-up construction (the Rees algebra file explicitly leaves geometric blow-ups to future work), hence no exceptional divisor/strict-transform, blow-up intersection/Picard formulas, factorization, elimination of indeterminacy, minimal-surface, or Castelnuovo package needed for this row. Strict whole-row semantics reject proper subsets and substantive reconstruction from rational-map, Rees-algebra, projective-space, or topological ingredients.
Proposition I1.3
Proposition I1.3 Let \(s\) be a surface, \(\epsilon : \hat { S } S\) the blow-up of a point \({ \pmb { p } } \in S\) and \(\pmb { { \cal E } } \subset \hat { S }\) the exceptional curve. (i) There is an isomorphism Pic \(S \oplus \mathbb { Z } \xrightarrow { \sim } \operatorname { P i c } \hat { S }\) defned \(b y \left( D , n \right) \mapsto\) \(\epsilon ^ { * } D + n E\) ： (ii） Let \(D\) ， \(D ^ { \prime }\) be divisors on \(s\) .Then \(\left( \epsilon ^ { * } D \right) . ( \epsilon ^ { * } D ^ { \prime } ) ~ = ~ D . D ^ { \prime }\) \(E . ( \epsilon ^ { * } D ) = 0\) ， \(E ^ { 2 } = - 1\) ： (ii） \(N S ( { \hat { S } } ) \cong N S ( S ) \oplus \mathbb { Z } [ E ]\) ， (iv) \(K _ { \hat { S } } = \epsilon ^ { * } K _ { S } + E\) ，
Not formalized. none; no complete checked declaration under strict bundle semantics — Pinned/current Mathlib has no scheme blow-up construction (the Rees algebra file explicitly leaves geometric blow-ups to future work), hence no exceptional divisor/strict-transform, blow-up intersection/Picard formulas, factorization, elimination of indeterminacy, minimal-surface, or Castelnuovo package needed for this row. Strict whole-row semantics reject proper subsets and substantive reconstruction from rational-map, Rees-algebra, projective-space, or topological ingredients.
Definition / construction II.4
II.4 (rational maps). A rational map \(X\dashrightarrow Y\) is a morphism on a maximal dense open subset. For a smooth surface its indeterminacy set is finite, so images of curves and pullbacks of divisors, linear systems, and line bundles are well defined.
Not formalized. none; no complete checked declaration under strict bundle semantics — Mathlib has Scheme.RationalMap, a quotient of morphisms on dense open subschemes, and constructs its maximal dense domain. However the source row additionally asserts finiteness of the indeterminacy locus for smooth surfaces and well-defined images/pullbacks of curves, divisors, linear systems, and line bundles. Those interfaces are absent, so the bundled row is incomplete. Strict whole-row semantics reject proper subsets and substantive reconstruction from rational-map, Rees-algebra, projective-space, or topological ingredients.
Definition / construction II.5
II.5 (linear systems). \(|D|\) is the complete linear system of effective divisors linearly equivalent to \(D\); a projective linear subspace is a linear system, a one-dimensional system is a pencil, and fixed components, fixed part, and base points are defined by containment in every member.
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked Lean formalization of complete/partial linear systems of divisors on a projective variety, fixed parts/base points, or the correspondence with rational maps to projective space was found. Rational maps and projective spaces alone are proper subsets. Strict whole-row semantics reject proper subsets and substantive reconstruction from rational-map, Rees-algebra, projective-space, or topological ingredients.
Construction / correspondence II.6
II.6. Rational maps \(S\dashrightarrow\mathbf P^n\) with nondegenerate image correspond bijectively to \(n\)-dimensional linear systems on \(S\) without fixed part.
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked Lean formalization of complete/partial linear systems of divisors on a projective variety, fixed parts/base points, or the correspondence with rational maps to projective space was found. Rational maps and projective spaces alone are proper subsets. Strict whole-row semantics reject proper subsets and substantive reconstruction from rational-map, Rees-algebra, projective-space, or topological ingredients.
Theorem II.7
Theorem II.7 (elimination of indeterminacy） Let \(\phi : S \to X\) be \(^ { a }\) Tational map from a surface to a projective variety. Then there exists a surface \(S ^ { \prime }\) ，a morphism \(\eta : S ^ { \prime } \to S\) which is the composite of a finite number of blow-ups， and a morphism \(\pmb { f } : S ^ { \prime } X\) such that the diagram \[ \sum _ { j = \cdots + X } ^ { S ^ { j } } f _ { j } \]
Not formalized. none; no complete checked declaration under strict bundle semantics — Pinned/current Mathlib has no scheme blow-up construction (the Rees algebra file explicitly leaves geometric blow-ups to future work), hence no exceptional divisor/strict-transform, blow-up intersection/Picard formulas, factorization, elimination of indeterminacy, minimal-surface, or Castelnuovo package needed for this row. Strict whole-row semantics reject proper subsets and substantive reconstruction from rational-map, Rees-algebra, projective-space, or topological ingredients.
Proposition II.8
Proposition II.8 (universal property of blowing-up) Let \(f : X \to S ^ { \prime }\) be a birational morphism of surfaces, and suppose that the rational map \(f ^ { - 1 }\) is undefined at a point \(\pmb { p }\) of \(s\) . Then \(f\) factorizes as \[ f : X { \overset { \ g } { \to } } \hat { S } \ { \overset { \epsilon } { \to } } \ S \] where \(\pmb { g }\) is a birational morphism and E is the blow-up at \(\pmb { p }\)
Not formalized. none; no complete checked declaration under strict bundle semantics — Pinned/current Mathlib has no scheme blow-up construction (the Rees algebra file explicitly leaves geometric blow-ups to future work), hence no exceptional divisor/strict-transform, blow-up intersection/Picard formulas, factorization, elimination of indeterminacy, minimal-surface, or Castelnuovo package needed for this row. Strict whole-row semantics reject proper subsets and substantive reconstruction from rational-map, Rees-algebra, projective-space, or topological ingredients.
Lemma I1.9
Lemma I1.9 Let \(s\) be an irreducible,but possibly singular, surface, \(S ^ { \prime }\) a smooth surface and \(\pmb { f } : S S ^ { \prime }\) a birational morphism. Suppose that the rational map \(f ^ { - 1 }\) is undefined at a point \(\pmb { p } \in S ^ { \prime }\) . Then \(f ^ { - 1 } ( \boldsymbol { p } )\) is \(^ { a }\) curve on \(s\)
Not formalized. none; no complete checked declaration under strict bundle semantics — Mathlib has birational rational maps, but no surface theorem forcing an inverse-image curve when the birational inverse is undefined at a point, nor the associated curve-contraction statement. Strict whole-row semantics reject proper subsets and substantive reconstruction from rational-map, Rees-algebra, projective-space, or topological ingredients.
Lemma II.10
Lemma II.10 Let \(\phi : S S ^ { \prime }\) be a rational map of surfaces such that \(\phi ^ { - 1 }\) is undefined at a point \({ \pmb p } \in S ^ { \prime }\) . Then there is a curve \(C\) on \(s\) such that \(\phi ( C ) = \{ p \}\) ，
Not formalized. none; no complete checked declaration under strict bundle semantics — Mathlib has birational rational maps, but no surface theorem forcing an inverse-image curve when the birational inverse is undefined at a point, nor the associated curve-contraction statement. Strict whole-row semantics reject proper subsets and substantive reconstruction from rational-map, Rees-algebra, projective-space, or topological ingredients.
Theorem II.11
Theorem II.11 Let \(\pmb { f } : S S _ { 0 }\) be a birational morphism of surfaces. Then there is a sequence of blow-ups \(\epsilon _ { k } : S _ { k } \to S _ { k - 1 }\) \(( k = 1 , \ldots , n )\) and an isomorphism \(u : S \tilde { \to } S _ { n }\) such that \(f = \epsilon _ { 1 } \circ \cdot \cdot \cdot \circ \epsilon _ { n } \circ u\) ：
Not formalized. none; no complete checked declaration under strict bundle semantics — Pinned/current Mathlib has no scheme blow-up construction (the Rees algebra file explicitly leaves geometric blow-ups to future work), hence no exceptional divisor/strict-transform, blow-up intersection/Picard formulas, factorization, elimination of indeterminacy, minimal-surface, or Castelnuovo package needed for this row. Strict whole-row semantics reject proper subsets and substantive reconstruction from rational-map, Rees-algebra, projective-space, or topological ingredients.
Corollary II.12
Corollary II.12 Let \(\phi : S S ^ { \prime }\) be a birational map of surfaces. Then there is a surface \(\hat { S }\) and a commutative diagram where the morphisms \({ f , g }\) are composites of blow-ups and isomorphisms.
Not formalized. none; no complete checked declaration under strict bundle semantics — Pinned/current Mathlib has no scheme blow-up construction (the Rees algebra file explicitly leaves geometric blow-ups to future work), hence no exceptional divisor/strict-transform, blow-up intersection/Picard formulas, factorization, elimination of indeterminacy, minimal-surface, or Castelnuovo package needed for this row. Strict whole-row semantics reject proper subsets and substantive reconstruction from rational-map, Rees-algebra, projective-space, or topological ingredients.
Remarks I1.13
Remarks II.13. A birational morphism that is a composite of \(n\) blow-ups changes the Néron–Severi group by a free rank-\(n\) summand; the factorization theorem therefore has finite length and controls the partial order by domination among birational models.
Not formalized. none; no complete checked declaration under strict bundle semantics — Pinned/current Mathlib has no scheme blow-up construction (the Rees algebra file explicitly leaves geometric blow-ups to future work), hence no exceptional divisor/strict-transform, blow-up intersection/Picard formulas, factorization, elimination of indeterminacy, minimal-surface, or Castelnuovo package needed for this row. Strict whole-row semantics reject proper subsets and substantive reconstruction from rational-map, Rees-algebra, projective-space, or topological ingredients.
Example II.14(1)
Projection of a surface \(S\subset\mathbf P^n\) from a point \(p\in S\) becomes a morphism after blowing up \(p\).
Not formalized. none; no complete checked declaration under strict bundle semantics — Pinned/current Mathlib has no scheme blow-up construction (the Rees algebra file explicitly leaves geometric blow-ups to future work), hence no exceptional divisor/strict-transform, blow-up intersection/Picard formulas, factorization, elimination of indeterminacy, minimal-surface, or Castelnuovo package needed for this row. Strict whole-row semantics reject proper subsets and substantive reconstruction from rational-map, Rees-algebra, projective-space, or topological ingredients.
Example II.14(2)
Blowing up a point on a smooth quadric and projecting from that point gives a birational morphism to \(\mathbf P^2\) contracting the two generators through the point.
Not formalized. none; no complete checked declaration under strict bundle semantics — Pinned/current Mathlib has no scheme blow-up construction (the Rees algebra file explicitly leaves geometric blow-ups to future work), hence no exceptional divisor/strict-transform, blow-up intersection/Picard formulas, factorization, elimination of indeterminacy, minimal-surface, or Castelnuovo package needed for this row. Strict whole-row semantics reject proper subsets and substantive reconstruction from rational-map, Rees-algebra, projective-space, or topological ingredients.
Example II.14(3)
The conics through three non-collinear points define the quadratic Cremona transformation of \(\mathbf P^2\); after blowing up the three base points, the map is a birational morphism contracting the three joining lines.
Not formalized. none; no complete checked declaration under strict bundle semantics — Pinned/current Mathlib has no scheme blow-up construction (the Rees algebra file explicitly leaves geometric blow-ups to future work), hence no exceptional divisor/strict-transform, blow-up intersection/Picard formulas, factorization, elimination of indeterminacy, minimal-surface, or Castelnuovo package needed for this row. Strict whole-row semantics reject proper subsets and substantive reconstruction from rational-map, Rees-algebra, projective-space, or topological ingredients.
Definition / convention
Among surfaces birational to \(S\), \(S_1\) dominates \(S_2\) when there is a birational morphism \(S_1\to S_2\); this defines the domination order on birational models.
Not formalized. none; no complete checked declaration under strict bundle semantics — Birational maps/morphisms exist in Mathlib, but no object of smooth birational surface models with Beauville’s domination order or minimality predicate is formalized. Strict whole-row semantics reject proper subsets and substantive reconstruction from rational-map, Rees-algebra, projective-space, or topological ingredients.
Definition I.15
Definition I.15 A surface \(s\) is minimal if its class in \(B ( S )\) is minimal, so that every birational morphism \(S \to S ^ { \prime }\) is an isomorphism.
Not formalized. none; no complete checked declaration under strict bundle semantics — Birational maps/morphisms exist in Mathlib, but no object of smooth birational surface models with Beauville’s domination order or minimality predicate is formalized. Strict whole-row semantics reject proper subsets and substantive reconstruction from rational-map, Rees-algebra, projective-space, or topological ingredients.
Proposition II.16
Proposition II.16 Every surface dominates a minimal surface.
Not formalized. none; no complete checked declaration under strict bundle semantics — Pinned/current Mathlib has no scheme blow-up construction (the Rees algebra file explicitly leaves geometric blow-ups to future work), hence no exceptional divisor/strict-transform, blow-up intersection/Picard formulas, factorization, elimination of indeterminacy, minimal-surface, or Castelnuovo package needed for this row. Strict whole-row semantics reject proper subsets and substantive reconstruction from rational-map, Rees-algebra, projective-space, or topological ingredients.
Definition / criterion
An exceptional curve on a smooth surface is a curve that is the exceptional divisor of a blow-up to another smooth surface; a surface is minimal iff it contains no exceptional curve.
Not formalized. none; no complete checked declaration under strict bundle semantics — Pinned/current Mathlib has no scheme blow-up construction (the Rees algebra file explicitly leaves geometric blow-ups to future work), hence no exceptional divisor/strict-transform, blow-up intersection/Picard formulas, factorization, elimination of indeterminacy, minimal-surface, or Castelnuovo package needed for this row. Strict whole-row semantics reject proper subsets and substantive reconstruction from rational-map, Rees-algebra, projective-space, or topological ingredients.
Theorem I1.17
Theorem I1.17 (Castelnuovo’s contractibility criterion） Let \(s\) be a surface and \(E \subset S\) a curve isomorphic to \(\mathbb { P } ^ { 1 }\) with \(E ^ { 2 } = - 1\) . Then \(\pmb { { \cal E } }\) is an exceptional curve on \(\boldsymbol { S }\)
Not formalized. none; no complete checked declaration under strict bundle semantics — Pinned/current Mathlib has no scheme blow-up construction (the Rees algebra file explicitly leaves geometric blow-ups to future work), hence no exceptional divisor/strict-transform, blow-up intersection/Picard formulas, factorization, elimination of indeterminacy, minimal-surface, or Castelnuovo package needed for this row. Strict whole-row semantics reject proper subsets and substantive reconstruction from rational-map, Rees-algebra, projective-space, or topological ingredients.
Lemma I1.18
Lemma I1.18 Let \(f : X \to Y\) be a continuous map of Hausdorff spaces and \(K \subset X\) a compact subset. Suppose that (i) \(f _ { | K }\) is a homeomorphism;(ii) for all \(k \in K\) ， \(\pmb { f }\) is a local homeomorphism near \(\pmb { k }\) ： Then there is a neighbourhood \(\boldsymbol { U }\) in \(X\) of \(\kappa\) and an open subset \(V\) of \(Y\) such that \(\pmb { f }\) induces a homeomorphism \(\tau \xrightarrow { \sim } V\)
Not formalized. none; no complete checked declaration under strict bundle semantics — Mathlib has local homeomorphisms, compact/Hausdorff spaces, and restriction machinery, but targeted P/H search found no theorem with this exact compact-set-plus-local-homeomorphism hypothesis producing one neighborhood on which f is a homeomorphism onto an open subset. Reconstructing the finite subcover/gluing argument would be substantive. Strict whole-row semantics reject proper subsets and substantive reconstruction from rational-map, Rees-algebra, projective-space, or topological ingredients.