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

FC12 — Beauville, Complex Algebraic Surfaces.

This chapter contains 4 definitions, 1 criterion and 4 other statements.

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

Status Statements Share What it means
not formalized 9 100% A documented search found no Lean statement of it anywhere.
checked in total 9
  • Canonical block FC12-A-U001–FC12-A-U009, exactly 9 contiguous units.
  • Search order: project A=12618f8abc2b4852b3da9ab65c3bc547ac4c1f19, P=db584cd6d46c92f209a44c0f1c829460d327499d, H=71a80585ee495fc24472fd0eaffc89d94e4fd8d6, current/open/indexed, Reservoir/packages, broad GitHub Lean, and local references/mappings.
  • Result: 0 positive routes and 9 dated unmatched rows.
  • Targeted searches found no compatible Lean implementation of the appendix’s algebraic/compact-complex surface classification layer. Generic algebra, topology, Frobenius, group-action, manifold, or bilinear-form infrastructure is only partial.
  • N=2026-09-07 marks dated unmatched decisions; strict whole-row semantics apply uniformly.

Comparison

FC12-A-U001 · Appendix A, source L2930 · not formalized

For algebraically closed fields of characteristic different from \(2,3\), the classification agrees with characteristic \(0\); extra non-classical classes occur in characteristics \(2,3\).

Not formalized. none; no complete checked declaration under strict bundle semantics — No complete Lean owner was found for this positive-characteristic algebraic-surface classification/criterion. P/H has characteristic-p algebra, Frobenius, elliptic curves, group schemes, rational maps and generic scheme infrastructure, but no K3/Enriques/bielliptic/quasi-elliptic surface objects, Kodaira dimension, plurigenus/canonical-class surface invariants, or the characteristic-2/3 classification statements; strict whole-row semantics reject those proper subsets.

Comparison / criterion

FC12-A-U002 · Appendix A, source L2932 · after FC12-C02-U020, FC12-C03-U001, FC12-C03-U020 · not formalized

Ruled and rational surface theory is characteristic-independent; ruled surfaces are characterized by \(P_{12}=0\), termination of adjunction, or the existence of a non-exceptional curve \(C\) with \(C\cdot K<0\).

Not formalized. none; no complete checked declaration under strict bundle semantics — No complete Lean owner was found for this positive-characteristic algebraic-surface classification/criterion. P/H has characteristic-p algebra, Frobenius, elliptic curves, group schemes, rational maps and generic scheme infrastructure, but no K3/Enriques/bielliptic/quasi-elliptic surface objects, Kodaira dimension, plurigenus/canonical-class surface invariants, or the characteristic-2/3 classification statements; strict whole-row semantics reject those proper subsets.

Definition / comparison

FC12-A-U003 · Appendix A, source L2936 · after FC12-C03-U020, FC12-C08-U004 · not formalized

In characteristic \(p\), a K3 surface has \(K\equiv0\) and \(q=0\); these retain the characteristic-zero numerical properties and lift to characteristic \(0\).

Not formalized. none; no complete checked declaration under strict bundle semantics — No complete Lean owner was found for this positive-characteristic algebraic-surface classification/criterion. P/H has characteristic-p algebra, Frobenius, elliptic curves, group schemes, rational maps and generic scheme infrastructure, but no K3/Enriques/bielliptic/quasi-elliptic surface objects, Kodaira dimension, plurigenus/canonical-class surface invariants, or the characteristic-2/3 classification statements; strict whole-row semantics reject those proper subsets.

Definition / comparison

FC12-A-U004 · Appendix A, source L2940 · after FC12-C08-U003, FC12-C09-U003 · not formalized

In characteristic \(2\), a classical Enriques surface has an inseparable canonical double cover with group \(\mu_2\) and is elliptic or quasi-elliptic; quasi-elliptic means that the generic fibre is a cuspidal cubic.

Not formalized. none; no complete checked declaration under strict bundle semantics — No complete Lean owner was found for this positive-characteristic algebraic-surface classification/criterion. P/H has characteristic-p algebra, Frobenius, elliptic curves, group schemes, rational maps and generic scheme infrastructure, but no K3/Enriques/bielliptic/quasi-elliptic surface objects, Kodaira dimension, plurigenus/canonical-class surface invariants, or the characteristic-2/3 classification statements; strict whole-row semantics reject those proper subsets.

Comparison

FC12-A-U005 · Appendix A, source L2942 · after FC12-C06-U023 · not formalized

Bielliptic surface quotient types change in characteristics \(2\) and \(3\): some characteristic-zero Bagnera–de Franchis types disappear or acquire nonreduced group schemes.

Not formalized. none; no complete checked declaration under strict bundle semantics — No complete Lean owner was found for this positive-characteristic algebraic-surface classification/criterion. P/H has characteristic-p algebra, Frobenius, elliptic curves, group schemes, rational maps and generic scheme infrastructure, but no K3/Enriques/bielliptic/quasi-elliptic surface objects, Kodaira dimension, plurigenus/canonical-class surface invariants, or the characteristic-2/3 classification statements; strict whole-row semantics reject those proper subsets.

Definition: In characteristic \(2\), a non-classical Enriques surface has \(K\equiv0\) and…

FC12-A-U006 · Appendix A, source L2944 · after FC12-C03-U020, FC12-C08-U003 · not formalized

In characteristic \(2\), a non-classical Enriques surface has \(K\equiv0\) and \(q=1\); it is singular when Frobenius on \(H^1(\mathcal O_S)\) is bijective and supersingular when Frobenius is zero.

Not formalized. none; no complete checked declaration under strict bundle semantics — No complete Lean owner was found for this positive-characteristic algebraic-surface classification/criterion. P/H has characteristic-p algebra, Frobenius, elliptic curves, group schemes, rational maps and generic scheme infrastructure, but no K3/Enriques/bielliptic/quasi-elliptic surface objects, Kodaira dimension, plurigenus/canonical-class surface invariants, or the characteristic-2/3 classification statements; strict whole-row semantics reject those proper subsets.

Definition: In characteristics \(2\) or \(3\), a quasi-bielliptic surface is a quotient…

FC12-A-U007 · Appendix A, source L2946 · after FC12-C06-U023 · not formalized

In characteristics \(2\) or \(3\), a quasi-bielliptic surface is a quotient \((E\times C)/G\) with \(E\) elliptic and \(C\) a cuspidal cubic; its canonical class has order dividing \(4\) or \(6\).

Not formalized. none; no complete checked declaration under strict bundle semantics — No complete Lean owner was found for this positive-characteristic algebraic-surface classification/criterion. P/H has characteristic-p algebra, Frobenius, elliptic curves, group schemes, rational maps and generic scheme infrastructure, but no K3/Enriques/bielliptic/quasi-elliptic surface objects, Kodaira dimension, plurigenus/canonical-class surface invariants, or the characteristic-2/3 classification statements; strict whole-row semantics reject those proper subsets.

Comparison

FC12-A-U008 · Appendix A, source L2948 · after FC12-C07-U001, FC12-C09-U003 · not formalized

In positive characteristic, surfaces with \(\kappa=1\) are elliptic or, in characteristics \(2,3\), possibly quasi-elliptic.

Not formalized. none; no complete checked declaration under strict bundle semantics — No complete Lean owner was found for this positive-characteristic algebraic-surface classification/criterion. P/H has characteristic-p algebra, Frobenius, elliptic curves, group schemes, rational maps and generic scheme infrastructure, but no K3/Enriques/bielliptic/quasi-elliptic surface objects, Kodaira dimension, plurigenus/canonical-class surface invariants, or the characteristic-2/3 classification statements; strict whole-row semantics reject those proper subsets.

Criterion / comparison

FC12-A-U009 · Appendix A, source L2950 · after FC12-C07-U001 · not formalized

Among irrational surfaces in positive characteristic, \(\kappa=2\) is characterized by \(K^2>0\); pluricanonical behavior largely persists although Castelnuovo's inequality can fail.

Not formalized. none; no complete checked declaration under strict bundle semantics — No complete Lean owner was found for this positive-characteristic algebraic-surface classification/criterion. P/H has characteristic-p algebra, Frobenius, elliptic curves, group schemes, rational maps and generic scheme infrastructure, but no K3/Enriques/bielliptic/quasi-elliptic surface objects, Kodaira dimension, plurigenus/canonical-class surface invariants, or the characteristic-2/3 classification statements; strict whole-row semantics reject those proper subsets.