Hartshorne, Algebraic Geometry — Chapter IV: Curves
FC06 — Hartshorne, Algebraic Geometry.
This chapter contains 18 definitions, 14 theorems, 19 propositions, 7 lemmas, 12 corollaries, 42 examples, 9 constructions, 20 remarks, 5 conventions, 1 notation and 1 other statements.
Of the 148 statements checked against Lean, 2 are formalized somewhere and 146 are not.
| Status | Statements | Share | What it means |
|---|---|---|---|
| not formalized | 146 | 99% | A documented search found no Lean statement of it anywhere. |
| in Mathlib | 2 | 1% | Mathlib states and proves it. |
| checked in total | 148 |
- Canonical source block: FC06 Hartshorne, Chapter IV,
FC06-C04-U001–FC06-C04-U148, in canonical source-ID order. The live master mapping was checked first: C01–C03 were already complete, C04 was active, and concurrently owned C02 work was not touched. - Project-first inspection is recorded against repository
A=3b2239e161592472b34e02ad3b7da308f9ce7280. Pinned Mathlib isP=db584cd6d46c92f209a44c0f1c829460d327499d, Lean 4.33.0, Apache-2.0. Current Mathlib was refreshed atH=5aedf732b6987e8c26ab3c9ebc855314f82b045f; the two pinned positive routes were also checked at H and remain present there. - The C03 generator/audit pattern was reused: canonical rows are parsed and contiguity-checked, every positive Mathlib path/declaration is verified at P, and exactly one route is emitted per source ID.
- Strict bundle semantics govern every row. A route must own the complete source statement. Partial clauses, a theorem only for a special model without the required comparison bridge, a nearby algebraic primitive, a statement using
sorry, or an open/conditional work item does not count as a route. - Project source searches covered the Hartshorne/curve/elliptic/Riemann–Roch/Hurwitz/Jacobian/canonical-curve vocabulary. The only nearby project implementation is
LeanCategories/Lattices/Valued/ComplexTorus.lean; it does not prove the Hartshorne analytic/algebraic comparison rows and is therefore not promoted. - Pinned Mathlib was searched for algebraic curves, divisors/Picard, Riemann–Roch, finite morphisms/ramification/differentials, Frobenius, ample/very ample divisors, Weierstrass elliptic curves, group schemes, modular forms, CM/Hasse/supersingularity, rational points, hyperelliptic/canonical curves, gonality, Severi and Castelnuovo theory. Generic Kähler/different/ramification and Weierstrass-model infrastructure is retained only as near-miss evidence where it does not own the complete row.
- U086 has a direct pinned owner:
CategoryTheory.GrpObjis the internal-group structure in a Cartesian monoidal category, andOver Shas its Cartesian structure from pullbacks. This is exactly the group-scheme datum over S. Mathlib’s algebraic-geometry group files useGrpObj (Over.mk f)/GrpObj ((Spec A).asOver (Spec R)), confirming the intended scheme specialization. - U094 has a direct pinned owner in
Mathlib/Analysis/SpecialFunctions/Elliptic/Weierstrass.lean: the standard ℘ lattice sum and derivative, lattice periodicity, meromorphicity, and order-two poles are all proved. The same file proves the differential equation, but the field-generation half of U095 is absent, so U095 remains unmatched. - Pinned
RatFunc.Luroth.algEquivproves the field-theoretic part of U037 but not Hartshorne’s geometric consequence; pinnedfermatLastTheoremThreesupports the Diophantine obstruction behind U125 but not the exact projective rational-point set/group law. Both are rejected as proper subsets of bundled rows. - Current/open Mathlib searches found no landed algebraic-curve Riemann–Roch or Jacobian bridge. Relevant open work includes conditional Riemann–Roch (#41621), divisor/class-group groundwork (#41729/#41732), Jacobian blueprint statements (#40616), division-polynomial scalar-multiplication work (#41197), and universal Weierstrass-model work (#41300); none realizes a complete additional C04 row under this contract.
- External checks included
mrdouglasny/jacobian-challengeatJAC=8ce1ec28aed1c78b3b39d0bae26e2858c82f5143(analytic complex-curve/Jacobian development; torus uniformization is assumed axiomatically) andMichaelStollBayreuth/EllipticCurvesatEC=449c7b936813254c8718db5c204aa71e9c3c44f6(Apache-2.0; proved Mordell–Weil for Weierstrass models over number fields). The latter supplies a strong implementation of Mordell–Weil in a model representation, but no checked abstract-curve-to-Weierstrass bridge closes Hartshorne U124; its explicit rank-oneE(Q)≅Zexample is a different curve from U126. - No checked P/H/open/external route was found for the algebraic-curve Riemann–Roch/Hurwitz programme, ample/canonical embeddings, relative Picard/Jacobian theory, complex elliptic uniformization/classification, CM and supersingularity theory, or the canonical-curve/moduli/space-curve bounds in U127–U148.
N=2026-09-06marks a dated unmatched decision after project-first, pinned/current Mathlib, recorded open/current work, indexed search services, and relevant external Lean checks.
Convention — curve in Chapter IV
Throughout Chapter IV, a curve is a complete nonsingular curve over the fixed algebraically closed field k; it is integral, one-dimensional, proper, regular, and hence projective. “Point” means closed point unless the generic point is specified.
Not formalized. none; no complete checked declaration under strict bundle semantics — Mathlib has schemes, properness, regularity and dimension infrastructure, but no checked pinned/current declaration bundles Hartshorne’s complete-nonsingular-integral one-dimensional curve convention with the stated proper/projective/regular equivalences.
Construction/convention — arithmetic, geometric, and cohomological genus
For a curve X, p_a(X)=1−P_X(0) and p_g(X)=dim_k Γ(X,ω_X); both will be identified with h^1(X,O_X) and denoted g.
Not formalized. none; no complete checked declaration under strict bundle semantics — Arithmetic genus and several cohomological primitives exist separately, but no checked curve-level genus package owns every equality/definition in this source row.
Proposition 1.1 — equality of curve genera
For a curve X, p_a(X)=p_g(X)=dim_k H^1(X,O_X); this common nonnegative integer is the genus g(X).
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked P/H theorem identifies the arithmetic, geometric and cohomological genera for Hartshorne curves under the source interface.
Remark 1.1.1 — existence in every genus
The genus is nonnegative and every integer g≥0 occurs; for example, a nonsingular divisor of type (g+1,2) on a smooth quadric has genus g.
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked construction realizes existence of a smooth projective curve of every genus.
Convention/construction — divisors, degree, class group, and Picard group on a curve
On a curve every divisor is a finite sum of closed points, degree is the coefficient sum, principal divisors have degree zero, and Cl X≅Pic X; Pic^0 X is the subgroup of degree-zero invertible sheaves.
Not formalized. none; no complete checked declaration under strict bundle semantics — Divisors, Picard groups and degree-like constructions exist in several algebraic APIs, but no checked algebraic-curve interface bundles Div X, degree, Cl X ≅ Pic X, and Pic^0 X as stated.
Construction — l(D) and dimension of a complete linear system
For a divisor D, l(D)=dim_k H^0(X,L(D)); if l(D)>0 then |D| is the projective space of nonzero sections modulo scalars and dim|D|=l(D)−1.
Not formalized. none; no complete checked declaration under strict bundle semantics — As of 2026-09-06, no checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: For a divisor D, l(D)=dim_k H^0(X,L(D)); if l(D)>0 then |D| is the projective space of nonzero sections modulo scalars and dim|D|=l(D)−1. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, an incomplete proof, or a proper subset as the route for this ID.
Lemma 1.2 — nonempty degree-zero linear systems
If l(D)≠0 then deg D≥0; if moreover deg D=0, then D is linearly equivalent to zero.
Not formalized. none; no complete checked declaration under strict bundle semantics — As of 2026-09-06, no checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: If l(D)≠0 then deg D≥0; if moreover deg D=0, then D is linearly equivalent to zero. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, an incomplete proof, or a proper subset as the route for this ID.
Definition/construction — canonical divisor on a curve
Since ω_X=Ω_X is invertible, any divisor K with L(K)≅ω_X is a canonical divisor; canonical divisors form the canonical linear-equivalence class.
Not formalized. none; no complete checked declaration under strict bundle semantics — As of 2026-09-06, no checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: Since ω_X=Ω_X is invertible, any divisor K with L(K)≅ω_X is a canonical divisor; canonical divisors form the canonical linear-equivalence class. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, an incomplete proof, or a proper subset as the route for this ID.
Theorem 1.3 — Riemann–Roch
For every divisor D on a genus-g curve with canonical divisor K, l(D)−l(K−D)=deg D+1−g.
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked pinned/current algebraic-curve Riemann–Roch theorem owns l(D)-l(K-D)=deg D+1-g. Open Mathlib PR #41621 is conditional Euler-characteristic Riemann–Roch work and does not close this row.
Remark 1.3.1 — Riemann–Roch recovers the curve Hilbert polynomial
If X⊂P^n has degree d and D is a hyperplane section, then for n≫0 Riemann–Roch gives χ(L(nD))=nd+1−g, identifying the constant term with 1−p_a.
Not formalized. none; no complete checked declaration under strict bundle semantics — As of 2026-09-06, no checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: If X⊂P^n has degree d and D is a hyperplane section, then for n≫0 Riemann–Roch gives χ(L(nD))=nd+1−g, identifying the constant term with 1−p_a. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, an incomplete proof, or a proper subset as the route for this ID.
Remark 1.3.2 — asymptotic dimensions of |nD|
If deg D>0, then nD is nonspecial for n≫0 and dim|nD|=n deg D−g; if deg D<0 no positive multiple is effective, while degree zero is governed by torsion/triviality in Pic^0.
Not formalized. none; no complete checked declaration under strict bundle semantics — As of 2026-09-06, no checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: If deg D>0, then nD is nonspecial for n≫0 and dim|nD|=n deg D−g; if deg D<0 no positive multiple is effective, while degree zero is governed by torsion/triviality in Pic^0. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, an incomplete proof, or a proper subset as the route for this ID.
Example 1.3.3 — degree of the canonical divisor
For a genus-g curve, deg K=2g−2.
Not formalized. none; no complete checked declaration under strict bundle semantics — As of 2026-09-06, no checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: For a genus-g curve, deg K=2g−2. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, an incomplete proof, or a proper subset as the route for this ID.
Example 1.3.4 — special divisors and index of speciality
D is special when l(K−D)>0; its index of speciality is l(K−D). Every divisor of degree >2g−2 is nonspecial.
Not formalized. none; no complete checked declaration under strict bundle semantics — As of 2026-09-06, no checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: D is special when l(K−D)>0; its index of speciality is l(K−D). Every divisor of degree >2g−2 is nonspecial. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, an incomplete proof, or a proper subset as the route for this ID.
Example 1.3.5 — genus zero iff rational
A curve has genus 0 iff it is isomorphic to P^1.
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked theorem gives the genus-zero iff projective-line classification for Hartshorne curves.
Example 1.3.6 — elliptic curves
A curve has genus 1 iff its canonical class is trivial; a genus-one curve is called an elliptic curve.
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked algebraic-curve theorem gives the genus-one/canonical-triviality characterization and its elliptic-curve consequence in this representation.
Example 1.3.7 — elliptic curve group law via Pic^0
For elliptic X and chosen P_0, P↦L(P−P_0) is a bijection from closed points of X to Pic^0 X, transporting the Picard-group law to a group law on X with identity P_0.
Not formalized. none; no complete checked declaration under strict bundle semantics — Mathlib has Weierstrass point-group implementations, but no checked Picard-based identification X ≅ Pic^0 X for an abstract genus-one curve.
Convention — degree of a finite curve morphism
For a finite morphism f:X→Y of curves, deg f=[K(X):K(Y)].
Not formalized. none; no complete checked declaration under strict bundle semantics — Function-field finite extensions and finite scheme morphisms are formalized separately, but no checked curve theorem identifies the degree of a finite morphism with the function-field extension degree under this complete row.
Definition/construction — ramification and branch points
For P∈X, Q=f(P), and a local parameter t at Q, e_P=v_P(t) is the ramification index; P is ramified if e_P>1 and Q is then a branch point.
Not formalized. none; no complete checked declaration under strict bundle semantics — Ramification indices exist algebraically, but no checked finite-morphism-of-curves branch/ramification package realizes this row.
Definition — tame and wild ramification
Ramification at P is tame when char k does not divide e_P, and wild otherwise.
Not formalized. none; no complete checked declaration under strict bundle semantics — As of 2026-09-06, no checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: Ramification at P is tame when char k does not divide e_P, and wild otherwise. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, an incomplete proof, or a proper subset as the route for this ID.
Construction — pullback of divisors along finite curve maps
For a closed point Q of Y, f^*Q=Σ_{P↦Q}e_P P; this extends linearly to divisors, is compatible with principal divisors, and hence with pullback on Picard groups.
Not formalized. none; no complete checked declaration under strict bundle semantics — As of 2026-09-06, no checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: For a closed point Q of Y, f^*Q=Σ_{P↦Q}e_P P; this extends linearly to divisors, is compatible with principal divisors, and hence with pullback on Picard groups. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, an incomplete proof, or a proper subset as the route for this ID.
Definition — separable morphism of curves
A finite curve morphism is separable when the induced extension K(X)/K(Y) is separable.
Not formalized. none; no complete checked declaration under strict bundle semantics — As of 2026-09-06, no checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: A finite curve morphism is separable when the induced extension K(X)/K(Y) is separable. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, an incomplete proof, or a proper subset as the route for this ID.
Proposition 2.1 — differential exact sequence for separable finite curve maps
If f:X→Y is finite and separable, then 0→f^*Ω_Y→Ω_X→Ω_{X/Y}→0 is exact.
Not formalized. none; no complete checked declaration under strict bundle semantics — Kähler differentials are formalized, but no checked curve-morphism exact differential sequence owns all clauses in this row.
Notation/construction — derivative dt/du
For local parameters t at Q=f(P) and u at P, write f^*dt=(dt/du)du in Ω_{X,P}.
Not formalized. none; no complete checked declaration under strict bundle semantics — As of 2026-09-06, no checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: For local parameters t at Q=f(P) and u at P, write f^*dt=(dt/du)du in Ω_{X,P}. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, an incomplete proof, or a proper subset as the route for this ID.
Proposition 2.2 — relative differentials measure ramification
For finite separable f:X→Y, Ω_{X/Y} is torsion supported at finitely many ramification points; its stalk at P has length v_P(dt/du). In tame ramification this length is e_P−1, while in wild ramification it is >e_P−1.
Not formalized. none; no complete checked declaration under strict bundle semantics — Kähler differentials/different ideals supply nearby algebra, but not the stated curve-local relative-differential length formula with tame/wild comparison.
Definition — ramification divisor
For finite separable f:X→Y, R=Σ_P length_{O_P}(Ω_{X/Y,P})P is the effective ramification divisor.
Not formalized. none; no complete checked declaration under strict bundle semantics — As of 2026-09-06, no checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: For finite separable f:X→Y, R=Σ_P length_{O_P}(Ω_{X/Y,P})P is the effective ramification divisor. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, an incomplete proof, or a proper subset as the route for this ID.
Proposition 2.3 — canonical divisor under a finite separable map
For finite separable f:X→Y, K_X is linearly equivalent to f^*K_Y+R.
Not formalized. none; no complete checked declaration under strict bundle semantics — As of 2026-09-06, no checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: For finite separable f:X→Y, K_X is linearly equivalent to f^*K_Y+R. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, an incomplete proof, or a proper subset as the route for this ID.
Corollary 2.4 — Hurwitz formula
If f:X→Y is finite separable of degree n, then 2g(X)−2=n(2g(Y)−2)+deg R. In the tame case deg R=Σ_P(e_P−1).
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked P/H Hurwitz theorem for finite separable morphisms of smooth projective curves was found.
Definition — absolute Frobenius
In characteristic p>0, the Frobenius morphism F:X→X is the identity on the underlying space and sends local functions to their pth powers.
Not formalized. none; no complete checked declaration under strict bundle semantics — Ring Frobenius exists, but no checked absolute-Frobenius morphism of schemes at P/H was found under the source interface.
Remark 2.4.1 — k-linear Frobenius twist
Absolute Frobenius need not be a k-morphism. Giving X the structure map composed with Frobenius of Spec k produces X_p and a k-linear Frobenius F′:X_p→X.
Not formalized. none; no complete checked declaration under strict bundle semantics — As of 2026-09-06, no checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: Absolute Frobenius need not be a k-morphism. Giving X the structure map composed with Frobenius of Spec k produces X_p and a k-linear Frobenius F′:X_p→X. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, an incomplete proof, or a proper subset as the route for this ID.
Example 2.4.2 — Frobenius twists
X_p need not be k-isomorphic to X in general; over perfect k, standard affine-space examples are isomorphic after twisting coefficients.
Not formalized. none; no complete checked declaration under strict bundle semantics — As of 2026-09-06, no checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: X_p need not be k-isomorphic to X in general; over perfect k, standard affine-space examples are isomorphic after twisting coefficients. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, an incomplete proof, or a proper subset as the route for this ID.
Example 2.4.3 — Frobenius of a curve
For a curve over algebraically closed characteristic-p k, the k-linear Frobenius is finite of degree p and induces the purely inseparable extension K(X) over K(X)^p.
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked theorem packages Frobenius of a curve as finite, purely inseparable, and degree p.
Proposition 2.5 — purely inseparable maps factor through Frobenius
Every finite purely inseparable morphism of curves factors as a composition of k-linear Frobenius morphisms; source and target are abstractly isomorphic and have the same genus.
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked factorization theorem says every finite purely inseparable curve morphism factors through an iterate of Frobenius.
Example 2.5.1 — Frobenius is everywhere ramified
The k-linear Frobenius on a curve has e_P=p everywhere; its differential pullback is zero and Ω_{X/X_p} identifies with Ω_X.
Not formalized. none; no complete checked declaration under strict bundle semantics — As of 2026-09-06, no checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: The k-linear Frobenius on a curve has e_P=p everywhere; its differential pullback is zero and Ω_{X/X_p} identifies with Ω_X. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, an incomplete proof, or a proper subset as the route for this ID.
Example 2.5.2 — even ramification degree
For any finite separable morphism of curves, deg R is even by Hurwitz.
Not formalized. none; no complete checked declaration under strict bundle semantics — As of 2026-09-06, no checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: For any finite separable morphism of curves, deg R is even by Hurwitz. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, an incomplete proof, or a proper subset as the route for this ID.
Example 2.5.3 — étale coverings and simple connectedness
A finite separable curve morphism is étale when unramified. Trivial covers are disjoint unions of copies; a curve is simply connected if it has no nontrivial connected étale cover. P^1 is simply connected.
Not formalized. none; no complete checked declaration under strict bundle semantics — As of 2026-09-06, no checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: A finite separable curve morphism is étale when unramified. Trivial covers are disjoint unions of copies; a curve is simply connected if it has no nontrivial connected étale cover. P^1 is simply connected. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, an incomplete proof, or a proper subset as the route for this ID.
Example 2.5.4 — genus under finite maps
For any finite morphism X→Y of curves, g(X)≥g(Y). In the separable case equality can occur only for degree one, or for g(Y)=1 with an unramified map.
Not formalized. none; no complete checked declaration under strict bundle semantics — As of 2026-09-06, no checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: For any finite morphism X→Y of curves, g(X)≥g(Y). In the separable case equality can occur only for degree one, or for g(Y)=1 with an unramified map. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, an incomplete proof, or a proper subset as the route for this ID.
Example 2.5.5 — Lüroth theorem
If k⊂L⊂k(t) with trdeg_k L=1, then L≅k(u): the corresponding finite map P^1→Y forces g(Y)=0.
Not formalized. none; no complete checked declaration under strict bundle semantics — Mathlib/FieldTheory/RatFunc/Luroth.lean::RatFunc.Luroth.algEquiv proves the field-theoretic Lüroth theorem, but the source row also requires the geometric consequence for dominant maps from P^1; no checked bridge owns that whole bundle.
Convention — ample and very ample divisors on curves
A divisor D is ample or very ample when L(D) has that property; |D| is the complete linear system and a base point is a point common to every effective divisor in |D|.
Not formalized. none; no complete checked declaration under strict bundle semantics — No pinned algebraic-geometry ample/very ample divisor interface was found that realizes this curve convention.
Proposition 3.1 — linear-system criteria for basepoint freeness and very ampleness
For a divisor D: |D| is basepoint-free iff dim|D−P|=dim|D|−1 for every P; D is very ample iff dim|D−P−Q|=dim|D|−2 for all P,Q, including P=Q.
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked curve theorem gives Hartshorne’s base-point-free/very-ample divisor criteria.
Corollary 3.2 — degree bounds for global generation and very ampleness
On a genus-g curve, deg D≥2g implies |D| is basepoint-free, and deg D≥2g+1 implies D is very ample.
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked curve theorem gives the degree ≥2g and ≥2g+1 base-point-free/very-ample bounds.
Corollary 3.3 — ampleness is positive degree
A divisor on a curve is ample iff it has positive degree.
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked theorem proves ampleness iff positive degree for divisors on a complete nonsingular curve.
Example 3.3.1 — positivity on P^1
On a genus-zero curve, D is ample iff very ample iff deg D>0.
Not formalized. none; no complete checked declaration under strict bundle semantics — As of 2026-09-06, no checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: On a genus-zero curve, D is ample iff very ample iff deg D>0. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, an incomplete proof, or a proper subset as the route for this ID.
Example 3.3.2 — degree of an embedding
If a very ample divisor D embeds X into projective space by its complete system, the degree of the embedded curve is deg D.
Not formalized. none; no complete checked declaration under strict bundle semantics — As of 2026-09-06, no checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: If a very ample divisor D embeds X into projective space by its complete system, the degree of the embedded curve is deg D. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, an incomplete proof, or a proper subset as the route for this ID.
Example 3.3.3 — elliptic plane cubics
Every degree-three divisor on an elliptic curve is very ample and embeds it as a plane cubic; on an elliptic curve, very ample is equivalent to degree at least three.
Not formalized. none; no complete checked declaration under strict bundle semantics — Mathlib has Weierstrass cubic models, but no checked theorem realizes the degree-three divisor/plane-cubic/very-ampleness classification for an abstract elliptic curve.
Example 3.3.4 — genus-two degree-five embedding
Every degree-five divisor on a genus-two curve is very ample, giving a degree-five embedding in P^3.
Not formalized. none; no complete checked declaration under strict bundle semantics — As of 2026-09-06, no checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: Every degree-five divisor on a genus-two curve is very ample, giving a degree-five embedding in P^3. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, an incomplete proof, or a proper subset as the route for this ID.
Example 3.3.5 — the 2g+1 bound need not be sharp
A nonsingular plane quartic has genus three and its degree-four hyperplane divisor is already very ample.
Not formalized. none; no complete checked declaration under strict bundle semantics — As of 2026-09-06, no checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: A nonsingular plane quartic has genus three and its degree-four hyperplane divisor is already very ample. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, an incomplete proof, or a proper subset as the route for this ID.
Definition/construction — secant and tangent lines
For X⊂P^n, a secant line contains two distinct points of X; a tangent line meets X with multiplicity at least two at a point.
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked secant/tangent-line curve interface was found that owns this geometric row.
Proposition 3.4 — projection from a point preserves an embedding
For O∉X, projection from O gives a closed immersion X→P^{n−1} iff O lies on neither a secant nor a tangent line of X.
Not formalized. none; no complete checked declaration under strict bundle semantics — As of 2026-09-06, no checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: For O∉X, projection from O gives a closed immersion X→P^{n−1} iff O lies on neither a secant nor a tangent line of X. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, an incomplete proof, or a proper subset as the route for this ID.
Proposition 3.5 — project curves down from P^n
If X⊂P^n with n≥4, there exists O∉X such that projection from O is a closed immersion into P^{n−1}; the secant and tangent loci have dimension at most 3 and 2 respectively.
Not formalized. none; no complete checked declaration under strict bundle semantics — As of 2026-09-06, no checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: If X⊂P^n with n≥4, there exists O∉X such that projection from O is a closed immersion into P^{n−1}; the secant and tangent loci have dimension at most 3 and 2 respectively. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, an incomplete proof, or a proper subset as the route for this ID.
Corollary 3.6 — every curve embeds in P^3
Every curve admits a closed immersion into P^3.
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked theorem proves every curve embeds in projective 3-space.
Definition/construction — multisecants and coplanar tangent secants
A multisecant meets X in at least three points; a secant through P,Q has coplanar tangents when the tangent lines at P and Q lie in one plane.
Not formalized. none; no complete checked declaration under strict bundle semantics — As of 2026-09-06, no checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: A multisecant meets X in at least three points; a secant through P,Q has coplanar tangents when the tangent lines at P and Q lie in one plane. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, an incomplete proof, or a proper subset as the route for this ID.
Proposition 3.7 — projection to a nodal plane curve
For X⊂P^3 and O∉X, projection to P^2 is birational with image having only nodes iff only finitely many secants pass through O, O lies on no tangent or multisecant, and no secant through O has coplanar tangents.
Not formalized. none; no complete checked declaration under strict bundle semantics — As of 2026-09-06, no checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: For X⊂P^3 and O∉X, projection to P^2 is birational with image having only nodes iff only finitely many secants pass through O, O lies on no tangent or multisecant, and no secant through O has coplanar tangents. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, an incomplete proof, or a proper subset as the route for this ID.
Proposition 3.8 — degeneracy of secants forces a common tangent point
If every secant of a projective curve is a multisecant, or if every secant has coplanar tangent lines, then there is a point A lying on every tangent line to X.
Not formalized. none; no complete checked declaration under strict bundle semantics — As of 2026-09-06, no checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: If every secant of a projective curve is a multisecant, or if every secant has coplanar tangent lines, then there is a point A lying on every tangent line to X. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, an incomplete proof, or a proper subset as the route for this ID.
Definition — strange curve
A projective curve is strange if all its tangent lines pass through one point A.
Not formalized. none; no complete checked declaration under strict bundle semantics — As of 2026-09-06, no checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: A projective curve is strange if all its tangent lines pass through one point A. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, an incomplete proof, or a proper subset as the route for this ID.
Example 3.8.1 — lines are strange
A line is strange.
Not formalized. none; no complete checked declaration under strict bundle semantics — As of 2026-09-06, no checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: A line is strange. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, an incomplete proof, or a proper subset as the route for this ID.
Example 3.8.2 — characteristic-two conics are strange
In characteristic two, a nonsingular plane conic is strange.
Not formalized. none; no complete checked declaration under strict bundle semantics — As of 2026-09-06, no checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: In characteristic two, a nonsingular plane conic is strange. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, an incomplete proof, or a proper subset as the route for this ID.
Theorem 3.9 — Samuel classification of strange curves
The only strange curves are lines and, in characteristic two, nonsingular conics.
Not formalized. none; no complete checked declaration under strict bundle semantics — As of 2026-09-06, no checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: The only strange curves are lines and, in characteristic two, nonsingular conics. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, an incomplete proof, or a proper subset as the route for this ID.
Theorem 3.10 — nodal plane model
Every curve embedded in P^3 admits projection from a suitable point to a plane curve such that the projection is birational and the only singularities of the image are nodes.
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked theorem constructs Hartshorne’s nodal plane model of an arbitrary curve.
Corollary 3.11 — every curve is birational to a nodal plane curve
Every curve is birationally equivalent to a plane curve having at most nodes.
Not formalized. none; no complete checked declaration under strict bundle semantics — As of 2026-09-06, no checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: Every curve is birationally equivalent to a plane curve having at most nodes. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, an incomplete proof, or a proper subset as the route for this ID.
Remark 3.11.1 — Severi varieties of nodal plane curves
A degree-d plane curve with r nodes has normalization genus g=(d−1)(d−2)/2−r. Thus 0≤r≤(d−1)(d−2)/2; both extremes occur, and the corresponding Severi loci organize plane curves by geometric genus.
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked Severi/node-genus/range/locus theorem was found.
Convention — characteristic in the elliptic-curve section
Except where stated otherwise, §4 omits characteristic 2; most results persist there with additional care.
Not formalized. none; no complete checked declaration under strict bundle semantics — As of 2026-09-06, no checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: Except where stated otherwise, §4 omits characteristic 2; most results persist there with additional care. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, an incomplete proof, or a proper subset as the route for this ID.
Definition/construction — Legendre parameter and j-invariant
For elliptic X and P_0 in characteristic ≠2, |2P_0| gives a separable degree-two map to P^1 ramified over four points. After moving them to 0,1,λ,∞ with λ≠0,1, define j=28(λ2−λ+1)3/(λ2(λ−1)^2).
Not formalized. none; no complete checked declaration under strict bundle semantics — As of 2026-09-06, no checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: For elliptic X and P_0 in characteristic ≠2, |2P_0| gives a separable degree-two map to P^1 ramified over four points. After moving them to 0,1,λ,∞ with λ≠0,1, define j=28(λ2−λ+1)3/(λ2(λ−1)^2). Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, an incomplete proof, or a proper subset as the route for this ID.
Theorem 4.1 — j classifies elliptic curves
Over an algebraically closed field of characteristic ≠2, j depends only on X; two elliptic curves are isomorphic iff their j-invariants agree; and every j∈k occurs.
Not formalized. none; no complete checked declaration under strict bundle semantics — Pinned Mathlib proves WeierstrassCurve.exists_variableChange_of_j_eq and variableChange_j, and constructs models with prescribed j. These are Weierstrass-model statements; no checked bridge identifies them with Hartshorne’s abstract smooth projective elliptic curves, so strict interface semantics reject them as the route for this row.
Lemma 4.2 — involution associated to two points
For any P,Q on an elliptic curve, there is an involution σ with σ(P)=Q and R+σ(R)∼P+Q for every R.
Not formalized. none; no complete checked declaration under strict bundle semantics — As of 2026-09-06, no checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: For any P,Q on an elliptic curve, there is an involution σ with σ(P)=Q and R+σ(R)∼P+Q for every R. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, an incomplete proof, or a proper subset as the route for this ID.
Corollary 4.3 — automorphisms act transitively
The automorphism group of an elliptic curve acts transitively on its points.
Not formalized. none; no complete checked declaration under strict bundle semantics — As of 2026-09-06, no checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: The automorphism group of an elliptic curve acts transitively on its points. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, an incomplete proof, or a proper subset as the route for this ID.
Lemma 4.4 — uniqueness of degree-two maps up to automorphisms
Any two degree-two morphisms X→P^1 from an elliptic curve differ by an automorphism of X and an automorphism of P^1.
Not formalized. none; no complete checked declaration under strict bundle semantics — As of 2026-09-06, no checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: Any two degree-two morphisms X→P^1 from an elliptic curve differ by an automorphism of X and an automorphism of P^1. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, an incomplete proof, or a proper subset as the route for this ID.
Lemma 4.5 — six cross-ratio values
Permuting four points on P^1 sends the Legendre parameter λ through the six values λ,1/λ,1−λ,1/(1−λ),λ/(λ−1),(λ−1)/λ, with coincidences only in the exceptional cases described by characteristic and λ.
Not formalized. none; no complete checked declaration under strict bundle semantics — As of 2026-09-06, no checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: Permuting four points on P^1 sends the Legendre parameter λ through the six values λ,1/λ,1−λ,1/(1−λ),λ/(λ−1),(λ−1)/λ, with coincidences only in the exceptional cases described by characteristic and λ. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, an incomplete proof, or a proper subset as the route for this ID.
Proposition 4.6 — Legendre normal form
For elliptic X over algebraically closed char≠2 with chosen P_0, there is a closed immersion X→P^2 taking P_0 to (0,1,0) and giving an equation y^2z=x(x−z)(x−λz) for some λ≠0,1.
Not formalized. none; no complete checked declaration under strict bundle semantics — As of 2026-09-06, no checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: For elliptic X over algebraically closed char≠2 with chosen P_0, there is a closed immersion X→P^2 taking P_0 to (0,1,0) and giving an equation y^2z=x(x−z)(x−λz) for some λ≠0,1. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, an incomplete proof, or a proper subset as the route for this ID.
Example 4.6.1 — y²=x³−x has j=1728
The nonsingular curve y²=x³−x has λ=−1 and j=26·33=1728 in characteristic ≠2.
Not formalized. none; no complete checked declaration under strict bundle semantics — As of 2026-09-06, no checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: The nonsingular curve y²=x³−x has λ=−1 and j=26·33=1728 in characteristic ≠2. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, an incomplete proof, or a proper subset as the route for this ID.
Example 4.6.2 — Fermat cubic has j=0
The Fermat cubic x³+y³=z³ is nonsingular in characteristic ≠3; after a change to Legendre/Weierstrass form its parameter is −ω or −ω², so j=0.
Not formalized. none; no complete checked declaration under strict bundle semantics — As of 2026-09-06, no checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: The Fermat cubic x³+y³=z³ is nonsingular in characteristic ≠3; after a change to Legendre/Weierstrass form its parameter is −ω or −ω², so j=0. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, an incomplete proof, or a proper subset as the route for this ID.
Corollary 4.7 — automorphisms fixing the origin
For char k≠2 and G=Aut(X,P_0): |G|=2 if j≠0,1728; 4 if j=1728 and char≠3; 6 if j=0 and char≠3; and 12 when char=3 and j=0=1728.
Not formalized. none; no complete checked declaration under strict bundle semantics — As of 2026-09-06, no checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: For char k≠2 and G=Aut(X,P_0): |G|=2 if j≠0,1728; 4 if j=1728 and char≠3; 6 if j=0 and char≠3; and 12 when char=3 and j=0=1728. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, an incomplete proof, or a proper subset as the route for this ID.
Construction — group law from Pic^0
With base point P_0, the bijection P↦L(P−P_0) transports Pic^0X to a group law characterized by P+Q=R iff P+Q∼R+P_0; in the |3P_0| plane embedding, three collinear points sum to zero.
Not formalized. none; no complete checked declaration under strict bundle semantics — Pinned Weierstrass point types carry explicit abelian group laws, but no checked construction transports Pic^0 X along P ↦ O(P-P_0) and proves the collinearity characterization for Hartshorne’s abstract plane embedding.
Proposition 4.8 — elliptic group operations are morphisms
For the group law on (X,P_0), inversion ρ:P↦−P and addition μ:X×X→X are morphisms, so X is a group variety.
Not formalized. none; no complete checked declaration under strict bundle semantics — Pinned Weierstrass point addition is formalized as an operation on points, not as the required scheme morphism X×X→X for the abstract elliptic curve; the group-variety row therefore remains unmatched.
Example 4.8.1 — multiplication-by-n morphisms
For every integer n, iterated group addition gives [n]:X→X. For n≠0 it will be finite of degree n²; prime-to-characteristic n-torsion is (Z/nZ)^2, while p-torsion depends on the Hasse invariant.
Not formalized. none; no complete checked declaration under strict bundle semantics — Pinned Weierstrass point APIs have integer scalar multiplication and division-polynomial infrastructure, but this row additionally bundles scheme-morphism finiteness/degree and characteristic-dependent torsion; no complete checked route owns all clauses.
Example 4.8.2 — two-torsion
[2] is finite; in characteristic ≠2 it has degree four and kernel Z/2Z×Z/2Z, the four ramification points of |2P_0|.
Not formalized. none; no complete checked declaration under strict bundle semantics — Pinned two-torsion polynomial/point infrastructure is substantial but does not own the whole source bundle: [2] as a finite curve morphism of degree four, kernel structure, and identification with the four ramification points of |2P_0|.
Example 4.8.3 — three-torsion and flexes
In characteristic ≠2,3, [3] has degree nine and kernel (Z/3Z)^2; its points are exactly the nine inflection points of the |3P_0| cubic embedding.
Not formalized. none; no complete checked declaration under strict bundle semantics — Division-polynomial and point-group infrastructure does not prove the full [3] degree-nine/kernel/flex-point bundle in Hartshorne’s curve representation.
Lemma 4.9 — basepoint-preserving maps are homomorphisms
A morphism f:(X,P_0)→(X′,P′_0) of elliptic curves sending P_0 to P′_0 is automatically a homomorphism of the group structures.
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked theorem states that every basepoint-preserving morphism of Hartshorne elliptic curves is a homomorphism of the Picard-induced group structures.
Definition — endomorphism ring of a pointed elliptic curve
End(X,P_0) consists of self-morphisms fixing P_0, with pointwise addition via μ and multiplication by composition; zero is the constant P_0 map and one is the identity.
Not formalized. none; no complete checked declaration under strict bundle semantics — Generic endomorphism rings and Weierstrass point operations do not supply Hartshorne’s ring of basepoint-preserving elliptic-curve morphisms with pointwise addition as a complete geometric interface.
Proposition 4.10 — integers embed in the endomorphism ring
If char k≠2, n↦[n] is an injective ring homomorphism Z→End(X,P_0); in particular [n] is finite for every n≠0.
Not formalized. none; no complete checked declaration under strict bundle semantics — Integer scalar multiplication exists for Weierstrass point groups, but no checked curve-morphism theorem proves the injective ring map Z→End(X,P_0) together with finiteness of nonzero [n] under the source interface.
Remark 4.10.1 — units and exceptional j-values
The unit group of End(X,P_0) is Aut(X,P_0); for j=0 or 1728 it is larger than {±1}, so the endomorphism ring is strictly larger than Z.
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked theorem identifies the unit group of Hartshorne’s elliptic endomorphism ring with based automorphisms and proves the exceptional j consequences.
Construction — relative degree-zero Picard functor
For a curve X and finite-type k-scheme T, Pic^0(X/T) is the subgroup of Pic(X×T) restricting to degree zero on fibres, modulo line bundles pulled back from T.
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked relative degree-zero Picard functor for algebraic curves owns the source quotient-by-base-line-bundles definition.
Definition — Jacobian variety
A Jacobian of X is a finite-type k-scheme J with a universal class L∈Pic^0(X/J) representing the functor T↦Pic^0(X/T).
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked representable relative-Picard/Jacobian construction at P/H owns this definition.
Remark 4.10.2 — representable-functor formulation
The Jacobian is precisely a representing object for the relative Picard functor T↦Pic^0(X/T).
Not formalized. none; no complete checked declaration under strict bundle semantics — Representable-functor category theory exists generically, but the relative Picard functor required by this row is not implemented as the checked represented functor.
Remark 4.10.3 — uniqueness and existence
The universal property makes J unique when it exists; for elliptic X one can take J=X, while higher-genus existence is substantially deeper.
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked Jacobian existence theorem for higher-genus algebraic curves or elliptic self-Jacobian bridge was found.
Remark 4.10.4 — closed points of J are Pic^0 classes
Assuming J exists, its closed points are naturally in bijection with Pic^0X.
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked algebraic Jacobian gives the stated closed-point/Pic^0 identification.
Definition — group scheme
A group scheme X/S has identity section e, inverse ρ, and multiplication μ:X×_S X→X satisfying the unit/inverse and associativity identities as morphisms.
Formalized. Mathlib/CategoryTheory/Monoidal/Grp.lean::CategoryTheory.GrpObj; Mathlib/CategoryTheory/Monoidal/Cartesian/Over.lean::CategoryTheory.Over.cartesianMonoidalCategory — Pinned Mathlib defines a group object in any Cartesian monoidal category by multiplication/unit/inverse and the associativity/unit/inverse identities. The Cartesian structure on Over S is built from pullbacks, so taking the ambient category to be schemes and the object in Over S gives exactly the identity section, inverse, and multiplication over the fibre product required by the source definition.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d; H=5aedf732b6987e8c26ab3c9ebc855314f82b045f
Remark 4.10.5 — group schemes generalize group varieties
Over Spec k, a group scheme whose total space is a variety recovers the earlier notion of group variety; the morphism identities induce the usual pointwise group axioms.
Not formalized. none; no complete checked declaration under strict bundle semantics — GrpObj supplies internal group axioms, but no checked theorem identifies a group scheme over Spec k whose total space is a variety with Hartshorne’s earlier group-variety notion and its pointwise group law as the complete comparison row.
Remark 4.10.6 — the Jacobian is canonically a group scheme
The representing property defines identity, inverse, and addition on J from 0, inverse line bundles, and tensor product, making the Jacobian a group scheme.
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked algebraic Jacobian representing object exists from which the canonical group-scheme structure in this row can be derived.
Remark 4.10.7 — tangent space of the Jacobian
The Zariski tangent space T_0J is naturally H^1(X,O_X), via degree-zero line bundles over k[ε]/(ε²).
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked theorem identifies the tangent space at zero of an algebraic Jacobian with H^1(X,O_X).
Remark 4.10.8 — the Jacobian is proper
The valuative criterion shows J is proper: an invertible sheaf on X×Spec K over a DVR extends uniquely across X×Spec R.
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked properness theorem for algebraic Jacobians via extension of line bundles over a DVR was found.
Remark 4.10.9 — Abel–Jacobi maps and dimension of J
Fixing P_0 defines φ_n:X^n→J by (P_1,…,P_n)↦L(P_1+⋯+P_n−nP_0). It is surjective for n≥g; general fibres of φ_g are finite, so J is irreducible of dimension g and nonsingular.
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked Abel–Jacobi X^n→J theorem owns the surjectivity, generic-finiteness, dimension, irreducibility and smoothness bundle.
Theorem 4.11 — an elliptic curve is its own Jacobian
For elliptic X with P_0, take J=X and the universal class L(Δ)⊗p_1^*L(−P_0) on X×J, where Δ is the diagonal. This represents Pic^0(X/−), and its induced group structure agrees with the earlier elliptic group law.
Not formalized. none; no complete checked declaration under strict bundle semantics — The external jacobian-challenge contains analytic Jacobian work, but no checked Hartshorne algebraic relative-Picard representation theorem with the Poincaré divisor owns this row.
Definition — elliptic function
For a lattice Λ=Z+Zτ⊂C with τ∉R, an elliptic function is a meromorphic f(z) satisfying f(z+ω)=f(z) for all ω∈Λ.
Not formalized. none; no complete checked declaration under strict bundle semantics — Pinned Mathlib has MeromorphicOn and periodicity predicates and constructs specific elliptic functions, but no named checked interface defines an elliptic function as exactly a meromorphic Λ-periodic function, so this source definition is not assigned to a partial conjunction of generic predicates.
Construction — Weierstrass ℘ and derivative
The lattice sum ℘(z)=1/z²+Σ_{ω∈Λ{0}}((z−ω){-2}−ω{-2}) defines an elliptic function with double poles at Λ; its derivative ℘′ is also elliptic.
Formalized. Mathlib/Analysis/SpecialFunctions/Elliptic/Weierstrass.lean::PeriodPair.weierstrassP, PeriodPair.derivWeierstrassP, PeriodPair.weierstrassP_add_coe, PeriodPair.derivWeierstrassP_add_coe, PeriodPair.meromorphic_weierstrassP, PeriodPair.order_weierstrassP — Pinned Mathlib defines ℘ by the standard lattice sum, proves lattice-periodicity of ℘ and ℘′, global meromorphicity of ℘, and order −2 at every lattice point. This owns the whole construction row; the later differential equation is also present as PeriodPair.derivWeierstrassP_sq but is not needed to close U094.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d; H=5aedf732b6987e8c26ab3c9ebc855314f82b045f
Theorem 4.12B — field of elliptic functions
The field of elliptic functions for Λ is C(℘,℘′), with relation (℘′)²=4℘³−g_2℘−g_3 where g_2=60Σω^{-4} and g_3=140Σω^{-6}.
Not formalized. none; no complete checked declaration under strict bundle semantics — Pinned PeriodPair.derivWeierstrassP_sq proves the differential equation, including the g2/g3 invariants, but no checked theorem says every elliptic function lies in C(℘,℘′); strict bundle semantics therefore leave the row unmatched.
Construction/comparison — C/Λ as an elliptic curve
z↦(℘(z),℘′(z)) identifies C/Λ biholomorphically with the nonsingular cubic y²=4x³−g_2x−g_3, and identifies elliptic functions with its rational function field.
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked theorem identifies C/Λ biholomorphically with the Weierstrass cubic and simultaneously identifies elliptic functions with its rational function field.
Theorem 4.13B — divisor criterion for elliptic functions
For distinct a_i∈C/Λ and integers n_i, there is an elliptic function with divisor Σn_i(a_i) iff Σn_i=0 and Σn_i a_i=0 in C/Λ.
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked divisor criterion for elliptic functions on C/Λ was found.
Comparison — analytic and algebraic group laws agree
Under C/Λ≅X, addition modulo Λ agrees with the Picard/divisor group law on the elliptic curve.
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked theorem compares the analytic quotient-group law with the Picard/divisor group law on the algebraic elliptic curve.
Theorem 4.14B — existence of a uniformizing lattice
For c_2,c_3∈C with Δ=c_2^3−27c_3²≠0, there exist τ∉R and α≠0 such that the lattice Z+Zτ has g_2=α^4c_2 and g_3=α^6c_3; hence every complex elliptic curve is uniformized by a lattice.
Not formalized. none; no complete checked declaration under strict bundle semantics — The local jacobian-challenge analytic development assumes a torus-uniformization axiom; it is not a proof route for Hartshorne’s uniformization theorem. No P/H proof of the stated g2/g3 existence/uniformization bundle was found.
Theorem 4.15B — modular equivalence of lattices
For τ,τ′∈C, J(τ)=J(τ′) iff τ′=(aτ+b)/(cτ+d) for integers a,b,c,d with ad−bc=±1; here j=1728J.
Not formalized. none; no complete checked declaration under strict bundle semantics — Pinned Mathlib formalizes the SL_2(Z) action and its fundamental domain, but no checked classical modular j-function theorem gives J(τ)=J(τ′) iff the lattices are GL2(Z)-equivalent.
Theorem 4.16 — topology/group structure of a complex elliptic curve
As an abstract group, a complex elliptic curve is R/Z×R/Z; in particular its n-torsion is (Z/nZ)^2.
Not formalized. none; no complete checked declaration under strict bundle semantics — The project has a complex-torus quotient/Lie-group implementation, but no checked equivalence of every complex elliptic curve with (R/Z)^2 as an abstract group, hence no complete n-torsion conclusion under this row.
Corollary 4.17 — degree of multiplication-by-n over C
For a complex elliptic curve, [n]:X→X is finite of degree n².
Not formalized. none; no complete checked declaration under strict bundle semantics — Integer scalar multiplication on model points exists, but the source requires the geometric degree theorem for [n] on a complex elliptic curve; no checked route owns it.
Proposition 4.18 — analytic description of endomorphisms
For X=C/Λ, End(X,P_0) corresponds bijectively to complex α with αΛ⊆Λ; this identifies the endomorphism ring with a subring of C.
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked theorem identifies analytic endomorphisms of C/Λ with scalars α satisfying αΛ⊆Λ.
Remark 4.18.1 — [n] corresponds to scalar n
Under the analytic endomorphism description, [n] is multiplication by n on C, giving another proof of Z↪End(X,P_0) over C.
Not formalized. none; no complete checked declaration under strict bundle semantics — As of 2026-09-06, no checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: Under the analytic endomorphism description, [n] is multiplication by n on C, giving another proof of Z↪End(X,P_0) over C. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, an incomplete proof, or a proper subset as the route for this ID.
Definition — complex multiplication
A complex elliptic curve has complex multiplication when End(X,P_0) is strictly larger than Z.
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked P/H named complex-multiplication predicate for elliptic curves was found.
Theorem 4.19 — complex multiplication and imaginary quadratic lattices
X=C/(Z+Zτ) has complex multiplication iff τ lies in an imaginary quadratic field. Then End(X) is an order in that field; for τ=r+s√−d with r,s∈Q, Hartshorne gives the explicit order {a+bτ: a,b∈Z, 2br and b(r²+ds²) integral}.
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked theorem classifies CM complex elliptic curves by imaginary-quadratic τ and computes the stated order.
Corollary 4.20 — CM j-invariants are countable
Only countably many j∈C correspond to elliptic curves with complex multiplication.
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked theorem derives countability of CM j-invariants from such a CM classification.
Example 4.20.1 — Gaussian CM
For τ=i, End X=Z[i], its unit group has order four, and j=1728.
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked elliptic-curve theorem packages the Gaussian lattice endomorphism ring, unit group and j=1728.
Example 4.20.2 — Eisenstein CM
For τ=ω with ω³=1, End X=Z[ω], its unit group has order six, and j=0.
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked elliptic-curve theorem packages the Eisenstein lattice endomorphism ring, unit group and j=0.
Example 4.20.3 — nonmaximal CM order
For τ=2i, End X=Z[2i], the order of conductor two in Q(i), strictly smaller than Z[i].
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked elliptic-curve theorem identifies the τ=2i endomorphism order as Z[2i] of conductor two.
Remark 4.20.4 — class-field-theoretic CM data
If End X=R has quotient field K imaginary quadratic and j=j(X), then j is an algebraic integer, K(j)/K is abelian of degree the class number of R, and j∈Z exactly when that class number is one; there are thirteen such integral j-values.
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked CM class-field theorem owns the algebraic-integrality, ring-class-field degree, and thirteen integral-j bundle.
Construction — Frobenius on H¹(OX)
In characteristic p, Frobenius induces a p-linear map F^*:H1(X,O_X)→H1(X,O_X); for elliptic X this one-dimensional map is either zero or bijective.
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked scheme/coherent-cohomology Frobenius action on H^1(O_X) for elliptic curves was found.
Definition — Hasse invariant and supersingularity
An elliptic curve has Hasse invariant 0, or is supersingular, when F^*=0 on H^1(O_X); otherwise its Hasse invariant is 1.
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked Hasse-invariant/supersingular elliptic-curve definition under Hartshorne’s cohomological interface was found.
Proposition 4.21 — Hasse invariant from a plane cubic equation
For a plane cubic f(x,y,z)=0 in characteristic p, the Hasse invariant is zero iff the coefficient of (xyz)^{p−1} in f^{p−1} is zero.
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked theorem identifies supersingularity of a plane cubic with the (xyz)^(p-1) coefficient in f^(p-1).
Corollary 4.22 — Hasse polynomial for a Legendre curve
For p≠2 and y²=x(x−1)(x−λ), supersingularity is equivalent to h_p(λ)=0, where h_p(λ)=Σ_{i=0}^k binom(k,i)^2 λ^i and k=(p−1)/2.
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked Legendre Hasse-polynomial supersingularity theorem was found.
Corollary 4.23 — finiteness of supersingular elliptic curves
For fixed p there are finitely many supersingular elliptic curves over the algebraic closure, at most ⌊p/12⌋+2 isomorphism classes.
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked theorem proves finiteness and the stated bound for supersingular j-isomorphism classes.
Example 4.23.1 — supersingular j in characteristic 3
For p=3, h_p(λ)=λ+1, whose only root gives j=0=1728.
Not formalized. none; no complete checked declaration under strict bundle semantics — As of 2026-09-06, no checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: For p=3, h_p(λ)=λ+1, whose only root gives j=0=1728. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, an incomplete proof, or a proper subset as the route for this ID.
Example 4.23.2 — supersingular j in characteristic 5
For p=5, h_p(λ)=λ²−λ+1; its two roots correspond to j=0.
Not formalized. none; no complete checked declaration under strict bundle semantics — As of 2026-09-06, no checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: For p=5, h_p(λ)=λ²−λ+1; its two roots correspond to j=0. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, an incomplete proof, or a proper subset as the route for this ID.
Example 4.23.3 — supersingular j in characteristic 7
For p=7, h_p(λ)=λ³+9λ²+9λ+1 has roots −1,2,4, all corresponding to j=1728.
Not formalized. none; no complete checked declaration under strict bundle semantics — As of 2026-09-06, no checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: For p=7, h_p(λ)=λ³+9λ²+9λ+1 has roots −1,2,4, all corresponding to j=1728. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, an incomplete proof, or a proper subset as the route for this ID.
Remark 4.23.4 — supersingular primes of a fixed elliptic curve
For an elliptic curve over Q reduced modulo good primes: in the CM case supersingular primes have density 1/2 and are characterized by ramified/inert behavior in the CM field; in the non-CM case they have density 0 but are infinite (Elkies), with Lang–Trotter predicting ~c√x/log x.
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked theorem owns the CM/non-CM supersingular-prime density, Elkies infinitude, and Lang–Trotter prediction bundle.
Example 4.23.5 — supersingular primes for y²=x³−x
For y²=x³−x with j=1728 and CM by i, good primes p≡1 mod4 have Hasse invariant 1 and p≡3 mod4 have Hasse invariant 0; the supersingular primes have density 1/2.
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked supersingular-prime classification for y^2=x^3-x by p mod 4 was found.
Example 4.23.6 — sparse supersingular primes in a non-CM example
For y²=x(x−1)(x+2), j=26·3{-2}·7^3 is nonintegral and the curve has no CM; among p≤73 only p=23 is supersingular.
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked theorem owns the non-CM j calculation and finite supersingular-prime example in the source row.
Construction — rational points over a field of definition
If a pointed plane elliptic curve (X,P_0) is defined over k_0⊆k, then the k_0-rational points form a subgroup X(k_0) of X(k).
Not formalized. none; no complete checked declaration under strict bundle semantics — WeierstrassCurve.Affine.Point.map is an injective additive homomorphism under a field embedding (map_injective), so model rational points do embed as a subgroup after base change. The source row is for an arbitrary pointed plane elliptic curve in Hartshorne’s geometric representation; no checked conversion/compatibility bridge makes this model API a complete route.
Theorem/comparison — Mordell finite generation
For an elliptic curve over Q, Mordell’s theorem states that X(Q) is a finitely generated abelian group.
Not formalized. none; no complete checked declaration under strict bundle semantics — MichaelStollBayreuth/EllipticCurves at 449c7b936813254c8718db5c204aa71e9c3c44f6 proves WeierstrassCurve.Affine.fg_point_of_numberField, a Mordell–Weil theorem for Weierstrass models over number fields. No checked bridge from Hartshorne’s abstract elliptic curve over Q to that model is part of the implementation, so it is recorded as a strong external near miss rather than a whole-row route.
Example 4.23.7 — rational points on the Fermat cubic
The Fermat cubic x³+y³=z³ has exactly three Q-rational points; with any one as origin they form Z/3Z.
Not formalized. none; no complete checked declaration under strict bundle semantics — Pinned Mathlib/NumberTheory/FLT/Three.lean::fermatLastTheoremThree proves the exponent-three Fermat equation obstruction, but it does not package the projective Fermat cubic’s exact three rational points or their Z/3Z group structure.
Example 4.23.8 — a rank-one elliptic curve over Q
For y²+y=x³−x with the point at infinity as origin, X(Q) is infinite cyclic generated by (0,0).
Not formalized. none; no complete checked declaration under strict bundle semantics — MichaelStollBayreuth/EllipticCurves at 449c7b936813254c8718db5c204aa71e9c3c44f6 contains a proved E(Q) ≅ Z example, but for y^2=x^3-x+1, not Hartshorne’s y^2+y=x^3-x; no checked source was found for the stated curve and generator (0,0).
Lemma 5.1 — canonical system is basepoint-free
If X has genus g≥2, the canonical linear system |K| has no base points.
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked theorem proves base-point-freeness of the canonical system for every genus ≥2 curve.
Definition — hyperelliptic curve
A genus-g curve with g≥2 is hyperelliptic if it admits a degree-two morphism to P^1, equivalently if it has a g^1_2.
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked hyperelliptic-curve interface/definition matching this row was found.
Proposition 5.2 — canonical system and hyperellipticity
For g≥2, the canonical divisor is very ample iff X is not hyperelliptic.
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked theorem proves the canonical divisor is very ample iff the curve is nonhyperelliptic.
Definition — canonical embedding and canonical curve
For a nonhyperelliptic curve of genus g≥3, the closed immersion given by |K| into P^{g−1} is the canonical embedding; its image is the canonical curve.
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked canonical-embedding construction for nonhyperelliptic algebraic curves was found.
Example 5.2.1 — genus-three canonical curves
A nonhyperelliptic genus-three curve is canonically embedded as a nonsingular plane quartic, and conversely every nonsingular plane quartic is such a canonical curve.
Not formalized. none; no complete checked declaration under strict bundle semantics — As of 2026-09-06, no checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: A nonhyperelliptic genus-three curve is canonically embedded as a nonsingular plane quartic, and conversely every nonsingular plane quartic is such a canonical curve. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, an incomplete proof, or a proper subset as the route for this ID.
Example 5.2.2 — genus-four canonical curves
A nonhyperelliptic genus-four canonical curve is a degree-six curve in P^3 lying on a unique irreducible quadric and is a complete intersection of that quadric with a cubic; conversely such smooth intersections are canonical genus-four curves.
Not formalized. none; no complete checked declaration under strict bundle semantics — As of 2026-09-06, no checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: A nonhyperelliptic genus-four canonical curve is a degree-six curve in P^3 lying on a unique irreducible quadric and is a complete intersection of that quadric with a cubic; conversely such smooth intersections are canonical genus-four curves. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, an incomplete proof, or a proper subset as the route for this ID.
Proposition 5.3 — canonical map of a hyperelliptic curve
For hyperelliptic X of genus g≥2, the g^1_2 is unique. The canonical morphism factors through the degree-two map X→P^1 followed by the (g−1)-uple embedding P1→P{g−1}; every effective canonical divisor is a sum of g−1 fibres of the g^1_2.
Not formalized. none; no complete checked declaration under strict bundle semantics — As of 2026-09-06, no checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: For hyperelliptic X of genus g≥2, the g^1_2 is unique. The canonical morphism factors through the degree-two map X→P^1 followed by the (g−1)-uple embedding P1→P{g−1}; every effective canonical divisor is a sum of g−1 fibres of the g^1_2. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, an incomplete proof, or a proper subset as the route for this ID.
Theorem 5.4 — Clifford theorem
If D is an effective special divisor on a curve, then dim|D|≤(1/2)deg D. Equality occurs for D=0 or K, or on a hyperelliptic curve for a multiple of the unique g^1_2.
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked Clifford theorem for divisors on algebraic curves, including the equality characterization, was found.
Lemma 5.5 — dimension under addition of effective divisors
For effective divisors D,E with complete linear systems of dimensions r,s, the complete system |D+E| has dimension at least r+s; Hartshorne uses this repeatedly to build g^r_d systems.
Not formalized. none; no complete checked declaration under strict bundle semantics — As of 2026-09-06, no checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: For effective divisors D,E with complete linear systems of dimensions r,s, the complete system |D+E| has dimension at least r+s; Hartshorne uses this repeatedly to build g^r_d systems. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, an incomplete proof, or a proper subset as the route for this ID.
Remark 5.5.1 — existence range for pencils
Every genus-g curve has a g^1_d for every d≥g/2+1 (with the integer interpretation implicit), while general curves need not have pencils of smaller degree; this motivates gonality.
Not formalized. none; no complete checked declaration under strict bundle semantics — As of 2026-09-06, no checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: Every genus-g curve has a g^1_d for every d≥g/2+1 (with the integer interpretation implicit), while general curves need not have pencils of smaller degree; this motivates gonality. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, an incomplete proof, or a proper subset as the route for this ID.
Example 5.5.2 — genus three and four curves have g^13
Every curve of genus 3 or 4 has a g^1_3; for a nonhyperelliptic genus-three plane quartic it arises by projection from a point of the curve.
Not formalized. none; no complete checked declaration under strict bundle semantics — As of 2026-09-06, no checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: Every curve of genus 3 or 4 has a g^1_3; for a nonhyperelliptic genus-three plane quartic it arises by projection from a point of the curve. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, an incomplete proof, or a proper subset as the route for this ID.
Example 5.5.3 — trigonal genus-five canonical curves
For a nonhyperelliptic genus-five canonical curve X⊂P^4, a g^1_3 yields trisecant lines. If X has no trisecants, it is the complete intersection of three quadrics; if it is trigonal, the trisecants sweep a rational surface containing X.
Not formalized. none; no complete checked declaration under strict bundle semantics — As of 2026-09-06, no checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: For a nonhyperelliptic genus-five canonical curve X⊂P^4, a g^1_3 yields trisecant lines. If X has no trisecants, it is the complete intersection of three quadrics; if it is trigonal, the trisecants sweep a rational surface containing X. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, an incomplete proof, or a proper subset as the route for this ID.
Remark 5.5.4 — moduli space of curves
For g≥2, isomorphism classes of nonsingular projective genus-g curves form an irreducible quasi-projective coarse moduli space M_g of dimension 3g−3.
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked construction/theorem for the coarse moduli space M_g with irreducibility, quasiprojectivity and dimension 3g-3 was found.
Example 5.5.5 — hyperelliptic locus in moduli
The hyperelliptic locus is irreducible of dimension 2g−1 inside M_g; for g=2 every curve is hyperelliptic.
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked theorem for the hyperelliptic locus in M_g was found.
Example 5.5.6 — genus-three moduli strata
In M_3 the hyperelliptic locus has dimension five, while nonhyperelliptic curves are plane quartics and fill the six-dimensional moduli space.
Not formalized. none; no complete checked declaration under strict bundle semantics — As of 2026-09-06, no checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: In M_3 the hyperelliptic locus has dimension five, while nonhyperelliptic curves are plane quartics and fill the six-dimensional moduli space. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, an incomplete proof, or a proper subset as the route for this ID.
Proposition 6.1 — Halphen bound for nonspecial very ample divisors
For a curve of genus g≥2, there exists a nonspecial very ample divisor of degree d iff d≥g+3.
Not formalized. none; no complete checked declaration under strict bundle semantics — As of 2026-09-06, no checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: For a curve of genus g≥2, there exists a nonspecial very ample divisor of degree d iff d≥g+3. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, an incomplete proof, or a proper subset as the route for this ID.
Corollary 6.2 — nonspecial curves in P^3
There exists a nonsingular nonplanar curve of degree d and genus g in P^3 whose hyperplane divisor is nonspecial iff d≥g+3.
Not formalized. none; no complete checked declaration under strict bundle semantics — As of 2026-09-06, no checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: There exists a nonsingular nonplanar curve of degree d and genus g in P^3 whose hyperplane divisor is nonspecial iff d≥g+3. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, an incomplete proof, or a proper subset as the route for this ID.
Proposition 6.3 — lower bounds in the special-hyperplane case
If a nonsingular nonplanar curve X⊂P^3 has special hyperplane divisor, then d≥6 and g≥d/2+1.
Not formalized. none; no complete checked declaration under strict bundle semantics — As of 2026-09-06, no checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: If a nonsingular nonplanar curve X⊂P^3 has special hyperplane divisor, then d≥6 and g≥d/2+1. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, an incomplete proof, or a proper subset as the route for this ID.
Theorem 6.4 — Castelnuovo bound in P^3
For a nonsingular nonplanar curve of degree d and genus g in P^3: if d is even, g≤d²/4−d+1; if d is odd, g≤(d²−1)/4−d+1. Equality can hold only when the curve lies on a quadric surface.
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked Castelnuovo genus bound for nondegenerate curves in projective 3-space was found.
Remark 6.4.1 — existence region for degree and genus in P^3
Combining the nonspecial existence theorem with Castelnuovo gives the basic allowed region for (d,g) of smooth nonplanar space curves; the remaining intermediate special cases require further constructions.
Not formalized. none; no complete checked declaration under strict bundle semantics — As of 2026-09-06, no checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: Combining the nonspecial existence theorem with Castelnuovo gives the basic allowed region for (d,g) of smooth nonplanar space curves; the remaining intermediate special cases require further constructions. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, an incomplete proof, or a proper subset as the route for this ID.
Example 6.4.2 — smooth space curves of degree at most seven
Hartshorne lists the possible genera for smooth nonplanar curves of degrees 3–7: d=3 gives g=0; d=4 gives g=0,1; d=5 gives g=0,1,2; d=6 gives g=0,1,2,3,4; d=7 gives g=0,…,6, with the extremal special cases described on quadrics or as complete intersections.
Not formalized. none; no complete checked declaration under strict bundle semantics — As of 2026-09-06, no checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: Hartshorne lists the possible genera for smooth nonplanar curves of degrees 3–7: d=3 gives g=0; d=4 gives g=0,1; d=5 gives g=0,1,2; d=6 gives g=0,1,2,3,4; d=7 gives g=0,…,6, with the extremal special cases described on quadrics or as complete intersections. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, an incomplete proof, or a proper subset as the route for this ID.
Example 6.4.3 — two families of degree-nine genus-ten curves
Degree-nine genus-ten smooth curves in P^3 occur in at least two distinct families: complete intersections of two cubics, and curves of type (3,6) on a smooth quadric. Their dimensions differ, illustrating reducibility phenomena in Hilbert schemes of space curves.
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked theorem formalizes the two degree-nine genus-ten space-curve families or the resulting Hilbert-scheme reducibility assertion.