Hartshorne, Algebraic Geometry — Chapter I: Varieties
FC06 — Hartshorne, Algebraic Geometry.
This chapter contains 42 definitions, 22 theorems, 22 propositions, 6 lemmas, 11 corollaries, 15 examples, 12 constructions, 5 remarks, 3 conventions and 9 other statements.
Of the 147 statements checked against Lean, 32 are formalized somewhere and 115 are not.
| Status | Statements | Share | What it means |
|---|---|---|---|
| not formalized | 115 | 78% | A documented search found no Lean statement of it anywhere. |
| in Mathlib | 31 | 21% | Mathlib states and proves it. |
| in lean-categories | 1 | 1% | This repository states and proves it. |
| checked in total | 147 |
- Canonical source block: FC06 Hartshorne, Chapter I,
FC06-C01-U001–FC06-C01-U147, in canonical source-ID order. The canonical unit extraction was preserved; no completed FC05 block was touched. - Project-first inspection was refreshed at repository HEAD
A=cd74b69e97f743cd7318a9fe130ed2a749860b3f. The only complete project-owned C01 row promoted here is U138,LeanCategories/Algebra/DimensionTheory.lean::LeanCategories.Algebra.HilbertFunction. Project-local reuse crosses no external import/license boundary; no standalone repository license file was present in the checked tree. - Pinned Mathlib is
P=db584cd6d46c92f209a44c0f1c829460d327499d, Lean 4.33.0, Apache-2.0 and directly project-compatible. Every P declaration promoted in the table was inspected at that exact revision. - Current Mathlib was refreshed on 2026-09-06 at
H=5aedf732b6987e8c26ab3c9ebc855314f82b045f, Apache-2.0, Lean 4.34.0-rc2. H/current searches were used only as negative/current evidence here; no C01 row is silently credited to post-pin code. - The substantial FC06-C01 probes already recorded by the concurrent lean-categories audit were reused rather than rerun. Fresh searches in this pass were restricted to gaps left by those recordings (notably exact pinned declaration boundaries for Nullstellensatz, separable generation, DVR/Dedekind, cotangent dimension, and the numerical-polynomial/binomial-basis family).
- Strict bundle semantics govern every row. A route must own the complete stable-ID statement. A theorem for one clause, one example, a specialization, an unbridged classical/scheme analogue, or a result with stronger hypotheses than the source is recorded as adjacent evidence but is not promoted as the row.
- In particular, scheme-theoretic affine/projective/rational-map infrastructure is not used indiscriminately as a replacement for Hartshorne’s classical point-set variety interfaces. U071, U072 and U074 are credited because the pinned scheme interfaces are the direct general constructions/theorems and specialize to the integral schemes attached to varieties; broader bundled classical dictionaries (U057–U068, U075–U077) remain unmatched without the missing bridge/equivalence theorem.
- U019 remains unmatched even though
MvPolynomial.eq_vanishingIdeal_singleton_of_isMaximalproves existence of a representing affine point: the audited pinned interface does not package the source’s full unique-point correspondence as the row states it. - U034 is credited from the pinned principal-ideal-height theorems under precisely the source noetherian/non-zero-divisor hypotheses. U035 is the exact pinned height-one-prime characterization of UFDs.
- U078 remains unmatched despite
Field.exists_primitive_element: the source additionally requires the primitive element to be chosen as a linear combination of an arbitrary finite generating set.primitive_element_inf_auxconstructsα+cβinternally but does not expose the full finite-set strengthening as a stable declaration. U079 is represented exactly byIsTranscendenceBasisplusAlgebra.IsSeparable, and U081 is the direct perfect-field theorem inSeparablyGenerated.lean. - U099 is the direct
AdicCompletionconstruction, but U100 remains unmatched because the source bundles locality/injectivity, finite-module tensor completion, dimension preservation and regularity preservation/reflection; only a proper subset is present in the checked pinned completion API. Indexed Lean search on 2026-09-06 found no Cohen structure theorem for U101; the only relevant FLT search hit explicitly stated its absence. - U109–U116 are covered by pinned valuation/DVR/Dedekind interfaces. Mathlib uses an equivalent multiplicative/cyclic-value-group presentation in parts of the API and includes fields in
IsDedekindDomainvia dimension ≤ 1; the source’s additive valuation convention and dimension-one/nonfield hypotheses identify the intended special cases. U117 is deliberately not promoted because the pinned integral-closure Dedekind theorem requires separability while Hartshorne states arbitrary finite extension. - U133–U134 were searched separately in P, H and indexed GitHub Lean sources on 2026-09-06. P/H contain binomial-ring material and bibliographic references to integer-valued polynomials but no Hartshorne numerical-polynomial predicate or its binomial-basis/discrete-integration theorem. Indexed exact-phrase Lean search returned no match.
- U138 is project-existing. U139–U140 are not inferred from
Mathlib/RingTheory/Polynomial/HilbertPoly.lean: that file’s object is rational-power-series data and its documentation leaves graded-module Hilbert polynomials for future work. U141–U147 therefore remain unmatched as complete Hartshorne projective-degree/intersection bundles. Historical Atlas/TauCeti analogues found by the recorded audit are not promoted because the required exact semantics/package compatibility/license/toolchain route was not established; narrower plane-curve material also does not own U143–U144. - Open Mathlib PR searches recorded on 2026-09-06 for Hilbert polynomial graded module, Hartshorne variety, Bézout/intersection multiplicity, function-field curves and separating transcendence bases returned no route completing the missing rows. Targeted indexed Lean searches likewise found no algebraic-geometric blowup implementation matching U083–U091; Mathlib’s Rees-algebra source only contains a future-facing blowup comment.
N=2026-09-06marks a dated unmatched decision after project-first, P, H/current, recorded open/current work, indexed search services and relevant external Lean checks. Each unmatched row records the exact A/P/H revisions checked andnoneas its Lean target because no complete path/declaration exists.
Convention/construction — affine space
Fix an algebraically closed field k. Affine n-space A^n_k is k^n; its elements are points with affine coordinates.
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: Fix an algebraically closed field k. Affine n-space A^n_k is k^n; its elements are points with affine coordinates. Strict bundle semantics reject a specialization, a scheme-only analogue without the required bridge, one clause/example of a bundled row, or a proper subset as the route for this ID.
Construction — polynomial zero sets
For A=k[x_1,…,x_n], polynomials are functions on A^n; for T⊆A, Z(T) is their common zero set, depending only on the ideal generated by T.
Formalized. Mathlib/RingTheory/Nullstellensatz.lean::MvPolynomial.zeroLocus, MvPolynomial.zeroLocus_span — Pinned Mathlib defines common zero loci in the affine point type σ → K by polynomial evaluation and proves that replacing a set of equations by its generated ideal leaves the zero locus unchanged, exactly the source construction.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d
Definition — affine algebraic set
Y⊆A^n is algebraic when Y=Z(T) for some T⊆k[x_1,…,x_n].
Formalized. Mathlib/RingTheory/Nullstellensatz.lean::MvPolynomial.zeroLocus, MvPolynomial.zeroLocus_span — The source definition is represented extensionally: algebraic subsets of affine point space are precisely sets presented as MvPolynomial.zeroLocus K I; zeroLocus_span passes from an arbitrary family of equations to its generated ideal. Mathlib does not introduce a redundant separate AffineAlgebraicSet predicate.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d
Proposition 1.1 — algebraic sets are closed-set data
Algebraic sets are closed under arbitrary intersections and finite unions, and include ∅ and A^n.
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: Algebraic sets are closed under arbitrary intersections and finite unions, and include ∅ and A^n. Strict bundle semantics reject a specialization, a scheme-only analogue without the required bridge, one clause/example of a bundled row, or a proper subset as the route for this ID.
Definition — Zariski topology on affine space
The closed sets of A^n are the algebraic sets; equivalently opens are their complements.
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 closed sets of A^n are the algebraic sets; equivalently opens are their complements. Strict bundle semantics reject a specialization, a scheme-only analogue without the required bridge, one clause/example of a bundled row, or a proper subset as the route for this ID.
Example 1.1.1 — Zariski topology on A^1
Over algebraically closed k, proper closed subsets of A^1 are finite, so nonempty opens are complements of finite sets; the topology is not Hausdorff.
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: Over algebraically closed k, proper closed subsets of A^1 are finite, so nonempty opens are complements of finite sets; the topology is not Hausdorff. Strict bundle semantics reject a specialization, a scheme-only analogue without the required bridge, one clause/example of a bundled row, or a proper subset as the route for this ID.
Definition — irreducible subset
A nonempty subspace Y is irreducible when it is not the union of two proper closed subsets of Y.
Formalized. Mathlib/Topology/Irreducible.lean::IsIrreducible — Pinned Mathlib defines an irreducible set as nonempty and preirreducible, equivalently excluding a decomposition into two proper relatively closed pieces, matching Hartshorne’s topological definition.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d
Example 1.1.2 — A^1 is irreducible
A^1 is irreducible because every proper closed subset is finite whereas A^1 is infinite.
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^1 is irreducible because every proper closed subset is finite whereas A^1 is infinite. Strict bundle semantics reject a specialization, a scheme-only analogue without the required bridge, one clause/example of a bundled row, or a proper subset as the route for this ID.
Example 1.1.3 — open subsets of irreducible spaces
Every nonempty open subset of an irreducible space is irreducible and dense.
Formalized. Mathlib/Topology/Irreducible.lean::IsPreirreducible.open_subset, IsOpen.dense — The generic topology API proves that nonempty open subsets of an irreducible space remain irreducible and that nonempty opens are dense, exactly the two source assertions.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d
Example 1.1.4 — closure preserves irreducibility
The closure of an irreducible subset is irreducible.
Formalized. Mathlib/Topology/Irreducible.lean::IsIrreducible.closure, isIrreducible_iff_closure — Pinned Mathlib proves irreducibility is preserved and reflected by closure, directly containing the source statement.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d
Definition — affine and quasi-affine varieties
An affine variety is an irreducible closed subset of A^n; a quasi-affine variety is an open subset of an affine variety.
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: An affine variety is an irreducible closed subset of A^n; a quasi-affine variety is an open subset of an affine variety. Strict bundle semantics reject a specialization, a scheme-only analogue without the required bridge, one clause/example of a bundled row, or a proper subset as the route for this ID.
Construction — ideal of a subset
For Y⊆A^n, I(Y) is the ideal of polynomials vanishing at every point of Y.
Formalized. Mathlib/RingTheory/Nullstellensatz.lean::MvPolynomial.vanishingIdeal — Pinned Mathlib defines the ideal of all multivariable polynomials vanishing on a subset of affine point space, exactly I(Y).
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d
Proposition 1.2 — zero-set/vanishing-ideal calculus
Z and I reverse inclusion; I(Y_1∪Y_2)=I(Y_1)∩I(Y_2), I(Z(a))=√a, and Z(I(Y)) is the closure of Y.
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: Z and I reverse inclusion; I(Y_1∪Y_2)=I(Y_1)∩I(Y_2), I(Z(a))=√a, and Z(I(Y)) is the closure of Y. Strict bundle semantics reject a specialization, a scheme-only analogue without the required bridge, one clause/example of a bundled row, or a proper subset as the route for this ID.
Theorem 1.3A — Hilbert Nullstellensatz
If k is algebraically closed, a⊆k[x_1,…,x_n], and f vanishes on Z(a), then f^r∈a for some r>0.
Formalized. Mathlib/RingTheory/Nullstellensatz.lean::MvPolynomial.vanishingIdeal_zeroLocus_eq_radical — For algebraically closed K and finitely many variables, the pinned theorem states I(Z(a)) = radical(a). Membership in the radical is exactly existence of a positive power in a, so this is Hartshorne’s Nullstellensatz statement.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d
Corollary 1.4 — algebraic sets versus radical ideals
Y↦I(Y) and a↦Z(a) give an inclusion-reversing bijection between algebraic sets and radical ideals; irreducible algebraic sets correspond to prime ideals.
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: Y↦I(Y) and a↦Z(a) give an inclusion-reversing bijection between algebraic sets and radical ideals; irreducible algebraic sets correspond to prime ideals. Strict bundle semantics reject a specialization, a scheme-only analogue without the required bridge, one clause/example of a bundled row, or a proper subset as the route for this ID.
Example 1.4.1 — affine space is irreducible
A^n is irreducible because its ideal is (0), which is prime.
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^n is irreducible because its ideal is (0), which is prime. Strict bundle semantics reject a specialization, a scheme-only analogue without the required bridge, one clause/example of a bundled row, or a proper subset as the route for this ID.
Example 1.4.2 — irreducible plane curves
An irreducible f∈k[x,y] defines an irreducible affine curve Z(f); its degree is deg f.
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: An irreducible f∈k[x,y] defines an irreducible affine curve Z(f); its degree is deg f. Strict bundle semantics reject a specialization, a scheme-only analogue without the required bridge, one clause/example of a bundled row, or a proper subset as the route for this ID.
Example 1.4.3 — affine hypersurfaces
An irreducible polynomial in k[x_1,…,x_n] defines an affine hypersurface; for n=3 Hartshorne calls it a surface.
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: An irreducible polynomial in k[x_1,…,x_n] defines an affine hypersurface; for n=3 Hartshorne calls it a surface. Strict bundle semantics reject a specialization, a scheme-only analogue without the required bridge, one clause/example of a bundled row, or a proper subset as the route for this ID.
Example 1.4.4 — maximal ideals are points
Every maximal ideal of k[x_1,…,x_n] has the form (x_1-a_1,…,x_n-a_n) for a unique point (a_1,…,a_n)∈A^n.
Not formalized. none; no complete checked declaration under strict bundle semantics — Pinned Mathlib proves existence of a point representing each maximal ideal (MvPolynomial.eq_vanishingIdeal_singleton_of_isMaximal), but the audited interface does not package Hartshorne’s full existence-and-uniqueness point correspondence as one route; strict bundle semantics therefore leave the row unmatched.
Example 1.4.5 — algebraic closure is essential
Over a non-algebraically-closed field, the affine Nullstellensatz correspondence can fail; Hartshorne gives a real plane curve with no real 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: Over a non-algebraically-closed field, the affine Nullstellensatz correspondence can fail; Hartshorne gives a real plane curve with no real points. Strict bundle semantics reject a specialization, a scheme-only analogue without the required bridge, one clause/example of a bundled row, or a proper subset as the route for this ID.
Definition — affine coordinate ring
For affine algebraic Y⊆A^n, its affine coordinate ring is A(Y)=k[x_1,…,x_n]/I(Y).
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 affine algebraic Y⊆A^n, its affine coordinate ring is A(Y)=k[x_1,…,x_n]/I(Y). Strict bundle semantics reject a specialization, a scheme-only analogue without the required bridge, one clause/example of a bundled row, or a proper subset as the route for this ID.
Remark 1.4.6 — affine varieties and finitely generated domains
A(Y) is a finitely generated k-domain for an affine variety Y; conversely every finitely generated k-domain is an affine coordinate ring.
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(Y) is a finitely generated k-domain for an affine variety Y; conversely every finitely generated k-domain is an affine coordinate ring. Strict bundle semantics reject a specialization, a scheme-only analogue without the required bridge, one clause/example of a bundled row, or a proper subset as the route for this ID.
Definition — noetherian topological space
X is noetherian when every descending chain of closed subsets stabilizes.
Formalized. Mathlib/Topology/NoetherianSpace.lean::TopologicalSpace.NoetherianSpace — Pinned Mathlib packages the noetherian condition on a topological space and develops the equivalent finiteness consequences; it is the source descending-chain condition on closed subsets.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d
Example 1.4.7 — affine space is noetherian
A^n is noetherian because descending chains of closed sets give ascending chains of vanishing ideals in the noetherian polynomial ring.
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^n is noetherian because descending chains of closed sets give ascending chains of vanishing ideals in the noetherian polynomial ring. Strict bundle semantics reject a specialization, a scheme-only analogue without the required bridge, one clause/example of a bundled row, or a proper subset as the route for this ID.
Proposition 1.5 — irreducible components in noetherian spaces
Every nonempty closed subset of a noetherian space is a finite union of irreducible closed subsets; after removing inclusions, the components are unique.
Formalized. Mathlib/Topology/NoetherianSpace.lean::TopologicalSpace.NoetherianSpace.exists_finite_set_isClosed_irreducible, NoetherianSpace.exists_finset_irreducible, NoetherianSpace.finite_irreducibleComponents — Pinned Mathlib proves finite decomposition of closed sets into irreducible closed sets and finiteness of the canonical maximal irreducible components. The canonical irreducibleComponents construction supplies the inclusion-maximal/unique component set, matching the source proposition.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d
Corollary 1.6 — decomposition of affine algebraic sets
Every affine algebraic set decomposes uniquely as a finite union of varieties, none containing another.
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 affine algebraic set decomposes uniquely as a finite union of varieties, none containing another. Strict bundle semantics reject a specialization, a scheme-only analogue without the required bridge, one clause/example of a bundled row, or a proper subset as the route for this ID.
Definition — dimension of a topological space/variety
dim X is the supremum of lengths n of strict chains Z_0⊊⋯⊊Z_n of irreducible closed subsets; varieties inherit this dimension.
Formalized. Mathlib/Topology/KrullDimension.lean::topologicalKrullDim — Pinned Mathlib defines topological dimension as the Krull dimension of the poset of irreducible closed subsets, i.e. by lengths of strict chains of irreducible closed sets, exactly Hartshorne’s definition.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d
Example 1.6.1 — dim A^1=1
The only irreducible closed subsets of A^1 are points and A^1, hence dim A^1=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: The only irreducible closed subsets of A^1 are points and A^1, hence dim A^1=1. Strict bundle semantics reject a specialization, a scheme-only analogue without the required bridge, one clause/example of a bundled row, or a proper subset as the route for this ID.
Definition — height and Krull dimension
The height of a prime is the supremum of lengths of prime chains ending there; dim A is the supremum of prime heights.
Formalized. Mathlib/RingTheory/Ideal/Height.lean::Ideal.height, Mathlib/RingTheory/KrullDimension/Basic.lean::ringKrullDim — Pinned Mathlib defines prime-ideal height and ring Krull dimension from chains in the prime spectrum, matching the source definitions.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d
Proposition 1.7 — geometric and ring dimension agree
For an affine algebraic set Y, dim Y=dim A(Y).
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 an affine algebraic set Y, dim Y=dim A(Y). Strict bundle semantics reject a specialization, a scheme-only analogue without the required bridge, one clause/example of a bundled row, or a proper subset as the route for this ID.
Theorem 1.8A — dimension theorem for finitely generated domains
If B is a finitely generated k-domain, dim B=trdeg_k Frac(B), and for every prime p, ht p+dim(B/p)=dim B.
Not formalized. none; no complete checked declaration under strict bundle semantics — Pinned/current Mathlib has extensive Krull-dimension, transcendence-degree, quotient, and height infrastructure, but the audit found no declaration giving the complete finitely-generated-domain bundle dim B = trdeg_k Frac(B) together with ht p + dim(B/p)=dim B.
Proposition 1.9 — dimension of affine space
dim A^n=n.
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: dim A^n=n. Strict bundle semantics reject a specialization, a scheme-only analogue without the required bridge, one clause/example of a bundled row, or a proper subset as the route for this ID.
Proposition 1.10 — quasi-affine dimension equals closure dimension
If Y is quasi-affine, then dim Y=dim Y.
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 Y is quasi-affine, then dim Y=dim Y. Strict bundle semantics reject a specialization, a scheme-only analogue without the required bridge, one clause/example of a bundled row, or a proper subset as the route for this ID.
Theorem 1.11A — Krull Hauptidealsatz
In a noetherian ring, every minimal prime over a nonzerodivisor nonunit f has height 1.
Formalized. Mathlib/RingTheory/Ideal/KrullsHeightTheorem.lean::Ideal.height_le_one_of_isPrincipal_of_mem_minimalPrimes, Ideal.height_span_singleton_eq_one_of_mem_nonZeroDivisors — Pinned Mathlib gives Krull’s principal ideal theorem for primes minimal over a principal ideal and proves height one for a principal ideal generated by a nonunit non-zero-divisor. Under Hartshorne’s noetherian/non-zero-divisor hypotheses these are the standard two inequalities yielding height one for a minimal prime over (f).
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d
Proposition 1.12A — height-one criterion for UFDs
A noetherian domain is a UFD iff every height-one prime ideal is principal.
Formalized. Mathlib/RingTheory/Ideal/UFD.lean::UniqueFactorizationMonoid.iff_forall_isPrincipal_of_height_eq_one — Pinned Mathlib proves that a domain is a unique factorization domain exactly when every height-one prime ideal is principal; Hartshorne’s noetherian-domain hypotheses are a specialization.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d
Proposition 1.13 — codimension-one affine varieties are hypersurfaces
A variety Y⊆A^n has dimension n−1 iff Y=Z(f) for a nonconstant irreducible polynomial f.
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 variety Y⊆A^n has dimension n−1 iff Y=Z(f) for a nonconstant irreducible polynomial f. Strict bundle semantics reject a specialization, a scheme-only analogue without the required bridge, one clause/example of a bundled row, or a proper subset as the route for this ID.
Remark 1.13.1 — height two need not be two-generated
A height-two prime ideal in a polynomial ring need not be generated by two elements.
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 height-two prime ideal in a polynomial ring need not be generated by two elements. Strict bundle semantics reject a specialization, a scheme-only analogue without the required bridge, one clause/example of a bundled row, or a proper subset as the route for this ID.
Definition/construction — projective space and homogeneous coordinates
P^n_k is (A^{n+1}{0}) modulo nonzero scalar multiplication; representatives are homogeneous coordinates.
Not formalized. none; no complete checked declaration under strict bundle semantics — Pinned Mathlib and the project have scheme-theoretic projective space (ProjectiveSpectrum/ProjectiveSpace), but Hartshorne’s row is the classical closed-point quotient (A^{n+1}\{0})/k×; no checked interface identifies that exact point-set construction with the scheme object, so the scheme analogue is not credited.
Definitions — graded ring, homogeneous elements and homogeneous ideals
A graded ring S=⊕{d≥0}S_d has S_dS_e⊆S{d+e}; homogeneous elements lie in one degree and homogeneous ideals are graded submodules (equivalently homogeneously generated).
Formalized. Mathlib/RingTheory/GradedAlgebra/Basic.lean::GradedRing, Mathlib/RingTheory/GradedAlgebra/Homogeneous/Ideal.lean::Ideal.IsHomogeneous, HomogeneousIdeal — Pinned Mathlib has graded-ring decompositions with multiplicative degree compatibility and homogeneous ideals as ideals compatible with the grading, matching the source definitions.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d
Construction — projective zero sets
Homogeneous polynomials have well-defined vanishing on P^n; for homogeneous T, Z(T) is the common projective zero set, and Z(a) uses the homogeneous elements of a homogeneous ideal.
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: Homogeneous polynomials have well-defined vanishing on P^n; for homogeneous T, Z(T) is the common projective zero set, and Z(a) uses the homogeneous elements of a homogeneous ideal. Strict bundle semantics reject a specialization, a scheme-only analogue without the required bridge, one clause/example of a bundled row, or a proper subset as the route for this ID.
Definition — projective algebraic set
Y⊆P^n is algebraic when Y=Z(T) for a set T of homogeneous polynomials.
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: Y⊆P^n is algebraic when Y=Z(T) for a set T of homogeneous polynomials. Strict bundle semantics reject a specialization, a scheme-only analogue without the required bridge, one clause/example of a bundled row, or a proper subset as the route for this ID.
Proposition 2.1 — projective algebraic sets are closed-set data
Projective algebraic sets are closed under arbitrary intersections and finite unions, and include ∅ and P^n.
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: Projective algebraic sets are closed under arbitrary intersections and finite unions, and include ∅ and P^n. Strict bundle semantics reject a specialization, a scheme-only analogue without the required bridge, one clause/example of a bundled row, or a proper subset as the route for this ID.
Definition — Zariski topology on projective space
The projective Zariski topology takes algebraic sets as closed sets.
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 projective Zariski topology takes algebraic sets as closed sets. Strict bundle semantics reject a specialization, a scheme-only analogue without the required bridge, one clause/example of a bundled row, or a proper subset as the route for this ID.
Definition — projective and quasi-projective varieties
A projective variety is an irreducible projective algebraic set; a quasi-projective variety is an open subset of one; dimension is topological dimension.
Not formalized. none; no complete checked declaration under strict bundle semantics — The project defines IsProjectiveVariety/IsQuasiProjectiveVariety by immersion into projective space, but those predicates do not include Hartshorne’s irreducibility requirement. Under strict bundle semantics they are adjacent infrastructure, not a complete route for this row.
Construction — homogeneous ideal and coordinate ring
For Y⊆P^n, I(Y) is generated by homogeneous polynomials vanishing on Y; for algebraic Y, S(Y)=k[x_0,…,x_n]/I(Y).
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 Y⊆P^n, I(Y) is generated by homogeneous polynomials vanishing on Y; for algebraic Y, S(Y)=k[x_0,…,x_n]/I(Y). Strict bundle semantics reject a specialization, a scheme-only analogue without the required bridge, one clause/example of a bundled row, or a proper subset as the route for this ID.
Construction — standard affine charts of projective space
H_i=Z(x_i), U_i=P^n_i, and φ_i:U_i→A^n sends homogeneous coordinates to the ratios x_j/x_i with the ith entry omitted.
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: H_i=Z(x_i), U_i=P^n_i, and φ_i:U_i→A^n sends homogeneous coordinates to the ratios x_j/x_i with the ith entry omitted. Strict bundle semantics reject a specialization, a scheme-only analogue without the required bridge, one clause/example of a bundled row, or a proper subset as the route for this ID.
Proposition 2.2 — projective charts are affine topologically
Each φ_i is a homeomorphism U_i≅A^n for the Zariski topologies.
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: Each φ_i is a homeomorphism U_i≅A^n for the Zariski topologies. Strict bundle semantics reject a specialization, a scheme-only analogue without the required bridge, one clause/example of a bundled row, or a proper subset as the route for this ID.
Corollary 2.3 — affine covers of projective varieties
A projective (resp. quasi-projective) variety is covered by Y∩U_i, each homeomorphic to an affine (resp. quasi-affine) variety.
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 (resp. quasi-projective) variety is covered by Y∩U_i, each homeomorphic to an affine (resp. quasi-affine) variety. Strict bundle semantics reject a specialization, a scheme-only analogue without the required bridge, one clause/example of a bundled row, or a proper subset as the route for this ID.
Definition — regular functions on quasi-affine varieties
f:Y→k is regular at P if locally f=g/h with g,h polynomial and h nowhere zero; it is regular when so at every point.
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: f:Y→k is regular at P if locally f=g/h with g,h polynomial and h nowhere zero; it is regular when so at every point. Strict bundle semantics reject a specialization, a scheme-only analogue without the required bridge, one clause/example of a bundled row, or a proper subset as the route for this ID.
Lemma 3.1 — regular functions are continuous
A regular function on a quasi-affine variety is continuous for the Zariski topology on k=A^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: A regular function on a quasi-affine variety is continuous for the Zariski topology on k=A^1. Strict bundle semantics reject a specialization, a scheme-only analogue without the required bridge, one clause/example of a bundled row, or a proper subset as the route for this ID.
Definition — regular functions on quasi-projective varieties
f:Y→k is regular at P if locally f=g/h for homogeneous g,h of the same degree with h nowhere 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: f:Y→k is regular at P if locally f=g/h for homogeneous g,h of the same degree with h nowhere zero. Strict bundle semantics reject a specialization, a scheme-only analogue without the required bridge, one clause/example of a bundled row, or a proper subset as the route for this ID.
Remark 3.1.1 — identity principle for regular functions
Regular functions on a variety that agree on a nonempty open subset agree everywhere.
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: Regular functions on a variety that agree on a nonempty open subset agree everywhere. Strict bundle semantics reject a specialization, a scheme-only analogue without the required bridge, one clause/example of a bundled row, or a proper subset as the route for this ID.
Definition — varieties and morphisms
A variety means affine, quasi-affine, projective, or quasi-projective; a morphism is continuous and pulls regular functions on target opens back to regular functions.
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 variety means affine, quasi-affine, projective, or quasi-projective; a morphism is continuous and pulls regular functions on target opens back to regular functions. Strict bundle semantics reject a specialization, a scheme-only analogue without the required bridge, one clause/example of a bundled row, or a proper subset as the route for this ID.
Definition/construction — isomorphism of varieties
Morphisms compose; an isomorphism is a morphism admitting a two-sided inverse morphism.
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: Morphisms compose; an isomorphism is a morphism admitting a two-sided inverse morphism. Strict bundle semantics reject a specialization, a scheme-only analogue without the required bridge, one clause/example of a bundled row, or a proper subset as the route for this ID.
Definitions — global and local rings of regular functions
O(Y) is the ring of global regular functions; O_{P,Y} is the local ring of germs of regular functions near 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: O(Y) is the ring of global regular functions; O_{P,Y} is the local ring of germs of regular functions near P. Strict bundle semantics reject a specialization, a scheme-only analogue without the required bridge, one clause/example of a bundled row, or a proper subset as the route for this ID.
Construction — maximal ideal and residue field of O{P,Y}
O_{P,Y} is local: its maximal ideal consists of germs vanishing at P, and its residue field is k.
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: O_{P,Y} is local: its maximal ideal consists of germs vanishing at P, and its residue field is k. Strict bundle semantics reject a specialization, a scheme-only analogue without the required bridge, one clause/example of a bundled row, or a proper subset as the route for this ID.
Definition — function field and rational functions
K(Y) is the equivalence classes of regular functions on nonempty opens, identified when equal on overlap; its elements are rational functions.
Not formalized. none; no complete checked declaration under strict bundle semantics — Pinned Mathlib has Scheme.functionField for integral schemes, but it is constructed through the generic-point stalk rather than Hartshorne’s equivalence classes of regular functions on nonempty classical-variety opens; no audited bridge identifies the two interfaces in this corpus setting.
Proposition/construction — K(Y) is a field
Irreducibility makes nonempty opens intersect, so rational functions add and multiply; a nonzero rational function is invertible after restricting away from its zero set.
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: Irreducibility makes nonempty opens intersect, so rational functions add and multiply; a nonzero rational function is invertible after restricting away from its zero set. Strict bundle semantics reject a specialization, a scheme-only analogue without the required bridge, one clause/example of a bundled row, or a proper subset as the route for this ID.
Construction — O(Y) and local rings inside K(Y)
Restriction gives injective maps O(Y)→O_{P,Y}→K(Y), so these rings are viewed as subrings of the function field.
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: Restriction gives injective maps O(Y)→O_{P,Y}→K(Y), so these rings are viewed as subrings of the function field. Strict bundle semantics reject a specialization, a scheme-only analogue without the required bridge, one clause/example of a bundled row, or a proper subset as the route for this ID.
Comparison — function rings are isomorphism invariants
Replacing Y by an isomorphic variety preserves O(Y), O_{P,Y}, and K(Y) up to isomorphism.
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: Replacing Y by an isomorphic variety preserves O(Y), O_{P,Y}, and K(Y) up to isomorphism. Strict bundle semantics reject a specialization, a scheme-only analogue without the required bridge, one clause/example of a bundled row, or a proper subset as the route for this ID.
Theorem 3.2 — affine function-ring dictionary
For affine Y: O(Y)≅A(Y); points correspond to maximal ideals m_P; O_{P,Y}≅A(Y){m_P} with dim O{P,Y}=dim Y; and K(Y)=Frac A(Y), with trdeg_k K(Y)=dim Y.
Not formalized. none; no complete checked declaration under strict bundle semantics — Pinned Mathlib has localization, stalk and fraction-field theorems for affine schemes, but no checked declaration packages the entire classical affine-function-ring dictionary in this row, including points/maximal ideals, local dimension and transcendence degree.
Proposition 3.3 — standard projective charts are affine varieties
The homeomorphism φ_i:U_i→A^n of Proposition 2.2 is an isomorphism of varieties.
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 homeomorphism φ_i:U_i→A^n of Proposition 2.2 is an isomorphism of varieties. Strict bundle semantics reject a specialization, a scheme-only analogue without the required bridge, one clause/example of a bundled row, or a proper subset as the route for this ID.
Convention/notation — degree-zero homogeneous localizations
For homogeneous prime p in graded S, S_(p) is the degree-zero subring of the homogeneous localization; similarly S_(f) for homogeneous f.
Formalized. Mathlib/RingTheory/GradedAlgebra/HomogeneousLocalization.lean::HomogeneousLocalization, HomogeneousLocalization.AtPrime, HomogeneousLocalization.Away, HomogeneousLocalization.NumDenSameDeg — Pinned Mathlib formalizes homogeneous localization and its degree-zero part, including localization at a homogeneous prime and away from a homogeneous element, exactly the source S_(p)/S_(f) convention.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d
Theorem 3.4 — projective function-ring dictionary
For projective Y with homogeneous ring S(Y): O(Y)=k, O_{P,Y}≅S(Y)(m_P), and K(Y)≅S(Y)((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 projective Y with homogeneous ring S(Y): O(Y)=k, O_{P,Y}≅S(Y)(m_P), and K(Y)≅S(Y)((0)). Strict bundle semantics reject a specialization, a scheme-only analogue without the required bridge, one clause/example of a bundled row, or a proper subset as the route for this ID.
Proposition 3.5 — morphisms to affine varieties via coordinate rings
For any variety X and affine Y, Hom_var(X,Y) is naturally bijective to Hom_{k-alg}(A(Y),O(X)).
Not formalized. none; no complete checked declaration under strict bundle semantics — The Γ–Spec adjunction and Spec.homEquiv give the scheme analogue, but no checked bridge turns Hartshorne’s classical-variety Hom_var(X,Y) into that scheme Hom-set while preserving the complete source statement.
Lemma 3.6 — coordinate criterion for a morphism to affine space
A set map ψ:X→Y⊆A^n is a morphism iff each coordinate function x_i∘ψ is regular on X.
Not formalized. none; no complete checked declaration under strict bundle semantics — Pinned Mathlib has coordinate morphisms for scheme affine space, but no checked theorem states Hartshorne’s iff criterion for arbitrary set maps of classical varieties, so the scheme analogue is not credited.
Corollary 3.7 — affine isomorphism criterion
Affine varieties X and Y are isomorphic iff A(X) and A(Y) are isomorphic as k-algebras.
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: Affine varieties X and Y are isomorphic iff A(X) and A(Y) are isomorphic as k-algebras. Strict bundle semantics reject a specialization, a scheme-only analogue without the required bridge, one clause/example of a bundled row, or a proper subset as the route for this ID.
Corollary 3.8 — affine varieties anti-equivalent to finitely generated domains
X↦A(X) gives an arrow-reversing equivalence between affine varieties over k and finitely generated integral k-algebras.
Not formalized. none; no complete checked declaration under strict bundle semantics — Affine schemes are anti-equivalent to commutative rings in Mathlib, but Hartshorne’s row is the classical category of affine varieties versus finitely generated integral k-algebras. No checked full-subcategory equivalence supplies the complete restriction.
Theorem 3.9A — finiteness of integral closure
If A is a finitely generated k-domain with fraction field K and L/K is finite algebraic, the integral closure A′ of A in L is finite as an A-module and finitely generated over k.
Not formalized. none; no complete checked declaration under strict bundle semantics — Mathlib/RingTheory/DedekindDomain/IntegralClosure.lean::IsIntegralClosure.finite supplies a strong integral-closure finiteness theorem under additional hypotheses, but it does not own Hartshorne’s full arbitrary finitely-generated-domain/finite-field-extension statement. The broader row is not inferred.
Lemma 4.1 — morphisms agree from a dense open
Two morphisms X→Y that agree on a nonempty open subset of the variety X agree everywhere.
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: Two morphisms X→Y that agree on a nonempty open subset of the variety X agree everywhere. Strict bundle semantics reject a specialization, a scheme-only analogue without the required bridge, one clause/example of a bundled row, or a proper subset as the route for this ID.
Definition — rational and dominant rational maps
A rational map X⇢Y is an equivalence class of morphisms U→Y on nonempty opens; it is dominant when the image is dense.
Formalized. Mathlib/AlgebraicGeometry/Birational/RationalMap.lean::Scheme.RationalMap, Scheme.PartialMap; Mathlib/AlgebraicGeometry/Birational/Dominant.lean::RationalMap.IsDominant — Pinned Mathlib packages rational maps as equivalence classes of morphisms on dense domains and defines dominance. On the integral schemes associated to varieties this is the scheme-theoretic generalization of Hartshorne’s rational/dominant rational maps.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d
Definition — birational map and birational equivalence
A birational map is a rational map admitting a two-sided inverse rational map; varieties joined by one are birationally equivalent.
Formalized. Mathlib/AlgebraicGeometry/Birational/Birational.lean::Scheme.PartialIso, Scheme.Birational, BirationalOver — Pinned Mathlib defines birationality through inverse partial isomorphisms on dense opens, the scheme-theoretic form of a rational map with two-sided rational inverse.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d
Lemma 4.2 — principal affine opens
If Y=Z(f)⊆A^n is a hypersurface, then A^nis affine, isomorphic to zf=1 in A^{n+1}, with coordinate ring k[x_1,…,x_n]_f.
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 Y=Z(f)⊆A^n is a hypersurface, then A^nis affine, isomorphic to zf=1 in A^{n+1}, with coordinate ring k[x_1,…,x_n]_f. Strict bundle semantics reject a specialization, a scheme-only analogue without the required bridge, one clause/example of a bundled row, or a proper subset as the route for this ID.
Proposition 4.3 — affine opens form a basis
Every variety has a basis of open subsets that are affine varieties.
Formalized. Mathlib/AlgebraicGeometry/AffineScheme.lean::Scheme.affineOpens, exists_isAffineOpen_mem_and_subset, Scheme.isBasis_affineOpens — Pinned Mathlib proves that affine opens form a basis for every scheme. This is strictly more general than the source assertion for varieties and specializes to it under the standard variety-to-scheme interpretation.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d
Construction — pullback on function fields from a dominant rational map
A dominant rational map φ:X⇢Y induces an injective k-algebra map φ*:K(Y)→K(X) by composition on suitable nonempty opens.
Not formalized. none; no complete checked declaration under strict bundle semantics — Pinned Mathlib has dominant rational maps and function fields, but the audit found no declaration constructing the complete contravariant injective field map interface for this Hartshorne row.
Theorem 4.4 — varieties and function fields
Dominant rational maps X⇢Y correspond bijectively to k-algebra maps K(Y)→K(X), yielding an arrow-reversing equivalence with finitely generated field extensions of k.
Not formalized. none; no complete checked declaration under strict bundle semantics — Pinned Mathlib’s rational-map/function-field interfaces do not contain the full bijection and anti-equivalence with finitely generated field extensions stated here; the generic adjacent infrastructure is not promoted as the missing theorem.
Corollary 4.5 — characterizations of birational equivalence
X and Y are birational iff they contain isomorphic nonempty opens iff K(X)≅K(Y) as k-algebras.
Not formalized. none; no complete checked declaration under strict bundle semantics — Pinned Mathlib has birational schemes/partial isomorphisms and function fields, but no checked declaration packages all three Hartshorne equivalences (birational map, isomorphic nonempty opens, isomorphic function fields).
Theorem 4.6A — primitive element theorem
A finite separable extension L/K is simple; if K is infinite, a primitive element can be chosen as a K-linear combination of any finite generating set.
Not formalized. none; no complete checked declaration under strict bundle semantics — Mathlib/FieldTheory/PrimitiveElement.lean::Field.exists_primitive_element proves the finite-separable primitive-element theorem, and primitive_element_inf_aux internally constructs α+cβ over an infinite field. No stable declaration states the stronger source clause that a primitive element can be chosen as a linear combination of an arbitrary finite generating set, so the whole row remains unmatched.
Definition — separably generated field extension
K/k is separably generated when K is separable algebraic over k(B) for some transcendence basis B; such B is a separating transcendence basis.
Formalized. Mathlib/RingTheory/AlgebraicIndependent/Defs.lean::IsTranscendenceBasis; Mathlib/FieldTheory/Separable.lean::Algebra.IsSeparable — Mathlib represents “separably generated” by the existence of a transcendence basis B (IsTranscendenceBasis) for which the extension from the field generated by B is Algebra.IsSeparable. The latter class includes algebraicity. This is exactly Hartshorne’s definition, although no redundant named IsSeparablyGenerated predicate is introduced.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d
Theorem 4.7A — separating bases inside generators
If K/k is finitely generated and separably generated, every generating set contains a separating transcendence basis.
Not formalized. none; no complete checked declaration under strict bundle semantics — The separably-generated file proves existence theorems for separating transcendence bases, but the audit found no declaration with Hartshorne’s stronger “every generating set contains one” assertion.
Theorem 4.8A — finite-type extensions of perfect fields are separably generated
If k is perfect, in particular algebraically closed, every finitely generated field extension K/k is separably generated.
Formalized. Mathlib/FieldTheory/SeparablyGenerated.lean::exists_isTranscendenceBasis_and_isSeparable_of_perfectField — Pinned Mathlib explicitly proves that an essentially finite-type field extension over a perfect field admits a finite transcendence basis over which the remaining extension is separable; for field extensions this is Hartshorne’s finitely generated/perfect-field theorem.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d
Proposition 4.9 — hypersurface birational model
Every r-dimensional variety is birational to a hypersurface in P^{r+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: Every r-dimensional variety is birational to a hypersurface in P^{r+1}. Strict bundle semantics reject a specialization, a scheme-only analogue without the required bridge, one clause/example of a bundled row, or a proper subset as the route for this ID.
Construction — blowup of A^n at the origin
The blowup X⊆An×P{n−1} is cut out by x_i y_j=x_j y_i; projection to A^n gives the blowup morphism φ.
Not formalized. none; no complete checked declaration under strict bundle semantics — Pinned/current Mathlib has Rees-algebra infrastructure and only a future-facing blowup comment; indexed Lean search found no algebraic-geometric blowup of affine space matching the incidence construction. Plumbing/topological uses of “blow up” are semantically unrelated.
Property — blowup is an isomorphism off the center
φ restricts to X{-1}(O)≅An{O}.
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked algebraic-geometric blowup object is available, hence no exact theorem gives the isomorphism off the center for Hartshorne’s construction.
Property — exceptional fibre of the affine-space blowup
The fibre φ^{-1}(O) is P^{n−1}.
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked algebraic-geometric blowup object is available, hence the exceptional fibre identification with projective space is unmatched.
Property — exceptional directions
Points of φ^{-1}(O) correspond bijectively to lines through O in A^n via their limiting direction.
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked algebraic-geometric blowup interface realizes the exceptional-directions correspondence.
Property — irreducibility of the affine-space blowup
The blowup X of A^n at O is irreducible; the complement of the exceptional fibre is dense.
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked algebraic-geometric blowup interface realizes irreducibility/density for this affine-space blowup.
Definition — blowup of a subvariety at a point
For closed Y⊆A^n through O, the blowup Y is the closure of φ^{-1}(Y{O}) in the blowup of A^n; φ restricts to Y→Y.
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked algebraic-geometric strict-transform/blowup construction realizes this source definition.
Comparison — blowup morphism is birational
Y^{-1}(O)≅Y{O}, hence φ:Y→Y is birational; Hartshorne notes the construction will later be shown intrinsic.
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked algebraic-geometric blowup construction packages the strict-transform isomorphism off the center and resulting birationality.
Example 4.9.1 — blowup of a nodal plane cubic
Blowing up the nodal cubic y²=x²(x+1) replaces O by an exceptional P^1; the strict transform meets it in the two points corresponding to the two branch slopes.
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked Lean source formalizes Hartshorne’s nodal-cubic blowup example with its two exceptional intersection points.
Construction/comparison — strict transform under a blowup
The strict transform of a curve through the center is the closure of its inverse image off the center; distinct tangent directions meet the exceptional curve at distinct points.
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked algebraic-geometric strict-transform interface supplies the tangent-direction/exceptional-intersection statement.
Definition — Jacobian nonsingularity for affine varieties
If Y⊆A^n has dimension r and ideal generators f_i, Y is nonsingular at P when the Jacobian (∂f_i/∂x_j)(P) has rank n−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: If Y⊆A^n has dimension r and ideal generators f_i, Y is nonsingular at P when the Jacobian (∂f_i/∂x_j)(P) has rank n−r. Strict bundle semantics reject a specialization, a scheme-only analogue without the required bridge, one clause/example of a bundled row, or a proper subset as the route for this ID.
Definition/notation — Jacobian matrix at a point
The matrix (∂f_i/∂x_j)(P) is the Jacobian matrix; the nonsingularity condition is independent of the chosen ideal generators.
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 matrix (∂f_i/∂x_j)(P) is the Jacobian matrix; the nonsingularity condition is independent of the chosen ideal generators. Strict bundle semantics reject a specialization, a scheme-only analogue without the required bridge, one clause/example of a bundled row, or a proper subset as the route for this ID.
Definition — regular local ring
A noetherian local ring (A,m,k) is regular when dim_k(m/m²)=dim A.
Formalized. Mathlib/RingTheory/RegularLocalRing/Defs.lean::IsRegularLocalRing, IsRegularLocalRing.iff_finrank_cotangentSpace — Pinned Mathlib defines regular local rings by equality between Krull dimension and embedding dimension and proves the equivalent cotangent-space formula finrank(m/m²)=dim A, exactly the source definition.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d
Theorem 5.1 — intrinsic criterion for nonsingularity
For an affine variety Y and P∈Y, Y is nonsingular at P iff O_{P,Y} is a regular local ring.
Not formalized. none; no complete checked declaration under strict bundle semantics — Pinned Mathlib has regular local rings and substantial smoothness/stalk infrastructure, and historical Atlas work contains nearby smooth-point material, but no checked project-compatible declaration identifies Hartshorne’s Jacobian nonsingularity criterion for affine varieties with regularity of the local ring.
Definition — nonsingular and singular arbitrary varieties
A variety is nonsingular at P when O_P is regular; it is nonsingular if so everywhere and singular 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: A variety is nonsingular at P when O_P is regular; it is nonsingular if so everywhere and singular otherwise. Strict bundle semantics reject a specialization, a scheme-only analogue without the required bridge, one clause/example of a bundled row, or a proper subset as the route for this ID.
Proposition 5.2A — embedding-dimension inequality
For a noetherian local ring (A,m,k), dim_k(m/m²)≥dim A.
Formalized. Mathlib/RingTheory/Ideal/KrullsHeightTheorem.lean::ringKrullDim_le_spanFinrank_maximalIdeal; Mathlib/Algebra/Module/SpanRankOperations.lean::IsLocalRing.spanFinrank_maximalIdeal_eq_finrank_cotangentSpace — For a noetherian local ring, pinned Mathlib bounds Krull dimension by the minimal-generator rank of the maximal ideal and identifies that rank with the residue-field dimension of m/m², yielding exactly Hartshorne’s embedding-dimension inequality.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d
Theorem 5.3 — singular locus is proper closed
For every variety Y, Sing Y is a proper closed subset of Y.
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 every variety Y, Sing Y is a proper closed subset of Y. Strict bundle semantics reject a specialization, a scheme-only analogue without the required bridge, one clause/example of a bundled row, or a proper subset as the route for this ID.
Construction — m-adic completion
For a local ring (A,m), the m-adic completion A is the completion for powers of m, equivalently lim← A/m^n.
Formalized. Mathlib/RingTheory/AdicCompletion/Basic.lean::AdicCompletion, AdicCompletion.of — Pinned Mathlib constructs the I-adic completion as the inverse limit of the quotients by powers of I; specializing I to the maximal ideal is the source m-adic completion.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d
Theorem 5.4A — basic properties of completion
For noetherian local A: A is local and A→A injective; M≅M⊗_AA for finite M; dim A=dim A; regularity is preserved and reflected.
Not formalized. none; no complete checked declaration under strict bundle semantics — Pinned Mathlib proves important pieces of the completion bundle (locality and finite-module completed tensor-product results), but the audit found no single checked route covering injectivity, finite-module tensor identification, Krull-dimension equality, and preservation/reflection of regularity together. Strict bundle semantics reject partial credit.
Theorem 5.5A — Cohen structure theorem, regular case
A complete regular local ring of dimension n containing a field is isomorphic to kx_1,…,x_n for its residue field k.
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked P/H/open/external Lean declaration proves the equicharacteristic regular Cohen structure theorem. Indexed search on 2026-09-06 found only FLT code explicitly noting that no Cohen structure theorem is present.
Definition — analytically isomorphic points
P∈X and Q∈Y are analytically isomorphic when their completed local rings are isomorphic as k-algebras.
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: P∈X and Q∈Y are analytically isomorphic when their completed local rings are isomorphic as k-algebras. Strict bundle semantics reject a specialization, a scheme-only analogue without the required bridge, one clause/example of a bundled row, or a proper subset as the route for this ID.
Example 5.6.1 — analytic isomorphism preserves dimension
Analytically isomorphic points lie on varieties of the same dimension.
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: Analytically isomorphic points lie on varieties of the same dimension. Strict bundle semantics reject a specialization, a scheme-only analogue without the required bridge, one clause/example of a bundled row, or a proper subset as the route for this ID.
Example 5.6.2 — smooth points have one analytic type by dimension
Nonsingular points on varieties of the same dimension are analytically isomorphic.
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: Nonsingular points on varieties of the same dimension are analytically isomorphic. Strict bundle semantics reject a specialization, a scheme-only analogue without the required bridge, one clause/example of a bundled row, or a proper subset as the route for this ID.
Example 5.6.3 — analytic type of a node
In characteristic ≠2, the node of y²=x²(x+1) has completed local ring isomorphic to kx,y/(xy), so analytically it is two transverse branches.
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 ≠2, the node of y²=x²(x+1) has completed local ring isomorphic to kx,y/(xy), so analytically it is two transverse branches. Strict bundle semantics reject a specialization, a scheme-only analogue without the required bridge, one clause/example of a bundled row, or a proper subset as the route for this ID.
Comparison — completion can destroy integrality
In Example 5.6.3 the local ring is a domain whereas its completion is not.
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 Example 5.6.3 the local ring is a domain whereas its completion is not. Strict bundle semantics reject a specialization, a scheme-only analogue without the required bridge, one clause/example of a bundled row, or a proper subset as the route for this ID.
Theorem 5.7A — elimination theory
For homogeneous forms with indeterminate coefficients there are universal integer polynomials in those coefficients whose simultaneous vanishing is equivalent, after specialization to any field, to the forms having a common nonzero 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: For homogeneous forms with indeterminate coefficients there are universal integer polynomials in those coefficients whose simultaneous vanishing is equivalent, after specialization to any field, to the forms having a common nonzero zero. Strict bundle semantics reject a specialization, a scheme-only analogue without the required bridge, one clause/example of a bundled row, or a proper subset as the route for this ID.
Convention — function field of dimension one
A finitely generated extension K/k of transcendence degree one is called a function field of dimension one.
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 finitely generated extension K/k of transcendence degree one is called a function field of dimension one. Strict bundle semantics reject a specialization, a scheme-only analogue without the required bridge, one clause/example of a bundled row, or a proper subset as the route for this ID.
Definition — valuation
A valuation v:K^×→G to a totally ordered abelian group satisfies v(xy)=v(x)+v(y) and v(x+y)≥min(v(x),v(y)).
Formalized. Mathlib/RingTheory/Valuation/Basic.lean::AddValuation, Valuation — Pinned Mathlib provides both multiplicative valuations and the additive-value-group presentation AddValuation; the latter has the multiplicative/additive and ultrametric inequalities in Hartshorne’s definition.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d
Definitions — valuation ring and valuation over k
R={x:v(x)≥0}∪{0} is the valuation ring with maximal ideal {x:v(x)>0}∪{0}; R is a valuation ring of K if K is its fraction field, and of K/k when v is trivial on k^×.
Formalized. Mathlib/RingTheory/Valuation/ValuationSubring.lean::ValuationSubring, Valuation.valuationSubring, Valuation.mem_valuationSubring_iff, Valuation.mem_maximalIdeal_iff; Mathlib/RingTheory/Valuation/Basic.lean::Valuation.IsTrivialOn — Pinned Mathlib constructs the valuation ring from nonnegative values, identifies its maximal ideal by positive values, and records triviality on a specified base. For a field the ambient field is the fraction field, matching the source bundle.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d
Definition — domination of local rings
For local subrings A,B⊆K, B dominates A when A⊆B and m_B∩A=m_A.
Formalized. Mathlib/RingTheory/LocalRing/LocalSubring.lean::LocalSubring, LocalSubring.le_def — Pinned Mathlib’s order on local subrings is explicitly the domination order: A dominates B iff B ⊆ A and the maximal ideal of A contracts to that of B, exactly Hartshorne’s definition.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d
Theorem 6.1A — valuation rings via domination
A local subring R⊆K is a valuation ring iff it is maximal under domination; every local subring of K is dominated by a valuation ring.
Formalized. Mathlib/RingTheory/Valuation/LocalSubring.lean::ValuationSubring.isMax_toLocalSubring, LocalSubring.isMax_iff, LocalSubring.exists_le_valuationSubring — Pinned Mathlib proves valuation subrings are precisely maximal elements for the domination order and that every local subring is dominated by a valuation subring, exactly the two source assertions.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d
Definition — discrete valuation and DVR
A valuation is discrete when its value group is Z; its valuation ring is a discrete valuation ring.
Formalized. Mathlib/RingTheory/Valuation/Discrete/Basic.lean::Valuation.valuationSubring_isDiscreteValuationRing; Mathlib/RingTheory/DiscreteValuationRing/Basic.lean::IsDiscreteValuationRing — Pinned Mathlib expresses discreteness by a nontrivial cyclic value group and proves the associated valuation subring is a DVR. A nontrivial cyclic ordered abelian value group is the standard equivalent presentation of the source value group ℤ.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d
Theorem 6.2A — one-dimensional local-domain characterizations of DVRs
For a one-dimensional noetherian local domain A, the following are equivalent: DVR; integrally closed; regular local; maximal ideal principal.
Formalized. Mathlib/RingTheory/DiscreteValuationRing/TFAE.lean::IsDiscreteValuationRing.TFAE; Mathlib/RingTheory/KrullDimension/LocalRing.lean::ringKrullDim_eq_one_iff_of_isLocalRing_isDomain; Mathlib/RingTheory/RegularLocalRing/Defs.lean::IsRegularLocalRing.iff_finrank_cotangentSpace — Under the source assumptions (noetherian, local, domain, dimension one/nonfield), the pinned TFAE identifies DVR, integrally closed/Dedekind, principal maximal ideal, and one-dimensional cotangent space. The cited dimension-one and regular-local equivalences identify the cotangent clause with regularity, giving exactly Hartshorne’s list.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d
Definition — Dedekind domain
A Dedekind domain is an integrally closed noetherian domain of dimension one.
Formalized. Mathlib/RingTheory/DedekindDomain/Basic.lean::IsDedekindDomain, isDedekindDomain_iff — Pinned Mathlib packages noetherian, integrally closed domains of Krull dimension at most one. Mathlib includes fields in the class; under Hartshorne’s explicit dimension-one (hence nonfield) hypothesis this is exactly the source definition.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d
Comparison — localizations of Dedekind domains are DVRs
Localizing a Dedekind domain at any nonzero prime ideal gives a discrete valuation ring.
Formalized. Mathlib/RingTheory/DedekindDomain/Dvr.lean::IsLocalization.AtPrime.isDiscreteValuationRing_of_dedekind_domain — Pinned Mathlib proves that localizing a Dedekind domain at every nonzero prime ideal is a discrete valuation ring, exactly the source comparison.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d
Theorem 6.3A — integral closure preserves Dedekind domains in finite extensions
The integral closure of a Dedekind domain in a finite extension of its fraction field is Dedekind.
Not formalized. none; no complete checked declaration under strict bundle semantics — Pinned Mathlib/RingTheory/DedekindDomain/IntegralClosure.lean::IsIntegralClosure.isDedekindDomain requires a separability hypothesis on the finite field extension. Hartshorne’s row states arbitrary finite extension, so the pinned theorem is strictly weaker and is not credited.
Comparison — local rings on nonsingular curves are DVRs
If P lies on a nonsingular curve Y, then O_{P,Y} is a DVR of K(Y)/k.
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 P lies on a nonsingular curve Y, then O_{P,Y} is a DVR of K(Y)/k. Strict bundle semantics reject a specialization, a scheme-only analogue without the required bridge, one clause/example of a bundled row, or a proper subset as the route for this ID.
Lemma 6.4 — local-ring containment separates curve points
For a quasi-projective variety Y, O_Q⊆O_P inside K(Y) implies P=Q.
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 quasi-projective variety Y, O_Q⊆O_P inside K(Y) implies P=Q. Strict bundle semantics reject a specialization, a scheme-only analogue without the required bridge, one clause/example of a bundled row, or a proper subset as the route for this ID.
Lemma 6.5 — finiteness of poles across DVRs
For a dimension-one function field K/k and x∈K, only finitely many DVRs R of K/k fail to contain 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 dimension-one function field K/k and x∈K, only finitely many DVRs R of K/k fail to contain x. Strict bundle semantics reject a specialization, a scheme-only analogue without the required bridge, one clause/example of a bundled row, or a proper subset as the route for this ID.
Corollary 6.6 — DVRs occur as local rings on nonsingular affine curves
Every DVR of a dimension-one function field K/k is isomorphic to O_P for a point P on some nonsingular affine curve with function field K.
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 DVR of a dimension-one function field K/k is isomorphic to O_P for a point P on some nonsingular affine curve with function field K. Strict bundle semantics reject a specialization, a scheme-only analogue without the required bridge, one clause/example of a bundled row, or a proper subset as the route for this ID.
Construction — the valuation curve CK
C_K is the set of DVRs R_P of K/k, with finite subsets and C_K closed; for open U, O(U)=∩_{P∈U}R_P. Evaluation uses residues, and its function field is K.
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: C_K is the set of DVRs R_P of K/k, with finite subsets and C_K closed; for open U, O(U)=∩_{P∈U}R_P. Evaluation uses residues, and its function field is K. Strict bundle semantics reject a specialization, a scheme-only analogue without the required bridge, one clause/example of a bundled row, or a proper subset as the route for this ID.
Definition — abstract nonsingular curve
An abstract nonsingular curve is an open subset U⊆C_K with the induced topology and regular functions.
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: An abstract nonsingular curve is an open subset U⊆C_K with the induced topology and regular functions. Strict bundle semantics reject a specialization, a scheme-only analogue without the required bridge, one clause/example of a bundled row, or a proper subset as the route for this ID.
Definition — morphisms involving abstract nonsingular curves
A morphism between abstract nonsingular curves or varieties is continuous and pulls regular functions back to regular functions.
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 morphism between abstract nonsingular curves or varieties is continuous and pulls regular functions back to regular functions. Strict bundle semantics reject a specialization, a scheme-only analogue without the required bridge, one clause/example of a bundled row, or a proper subset as the route for this ID.
Proposition 6.7 — quasi-projective nonsingular curves are abstract curves
Every nonsingular quasi-projective curve is isomorphic to an open subset of C_{K(Y)}.
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 nonsingular quasi-projective curve is isomorphic to an open subset of C_{K(Y)}. Strict bundle semantics reject a specialization, a scheme-only analogue without the required bridge, one clause/example of a bundled row, or a proper subset as the route for this ID.
Proposition 6.8 — extension across a missing point
If X is an abstract nonsingular curve, P∈X, Y is projective, and φ:X{P}→Y is a morphism, φ extends uniquely to X→Y.
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 is an abstract nonsingular curve, P∈X, Y is projective, and φ:X{P}→Y is a morphism, φ extends uniquely to X→Y. Strict bundle semantics reject a specialization, a scheme-only analogue without the required bridge, one clause/example of a bundled row, or a proper subset as the route for this ID.
Theorem 6.9 — projective realization of CK
For every dimension-one function field K/k, the abstract curve C_K is isomorphic to a nonsingular projective 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: For every dimension-one function field K/k, the abstract curve C_K is isomorphic to a nonsingular projective curve. Strict bundle semantics reject a specialization, a scheme-only analogue without the required bridge, one clause/example of a bundled row, or a proper subset as the route for this ID.
Corollary 6.10 — abstract and quasi-projective nonsingular curves coincide
Every abstract nonsingular curve is quasi-projective, and every nonsingular quasi-projective curve is an open subset of a nonsingular projective 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 abstract nonsingular curve is quasi-projective, and every nonsingular quasi-projective curve is an open subset of a nonsingular projective curve. Strict bundle semantics reject a specialization, a scheme-only analogue without the required bridge, one clause/example of a bundled row, or a proper subset as the route for this ID.
Corollary 6.11 — nonsingular projective model of every curve
Every curve is birationally equivalent to a nonsingular projective 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 is birationally equivalent to a nonsingular projective curve. Strict bundle semantics reject a specialization, a scheme-only analogue without the required bridge, one clause/example of a bundled row, or a proper subset as the route for this ID.
Corollary 6.12 — three equivalent curve categories
Nonsingular projective curves with dominant morphisms, quasi-projective curves with dominant rational maps, and dimension-one function fields with k-homomorphisms are equivalent categories.
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: Nonsingular projective curves with dominant morphisms, quasi-projective curves with dominant rational maps, and dimension-one function fields with k-homomorphisms are equivalent categories. Strict bundle semantics reject a specialization, a scheme-only analogue without the required bridge, one clause/example of a bundled row, or a proper subset as the route for this ID.
Proposition 7.1 — affine dimension theorem
If Y,Z⊆A^n have dimensions r,s, every irreducible component of Y∩Z has dimension at least r+s−n.
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 Y,Z⊆A^n have dimensions r,s, every irreducible component of Y∩Z has dimension at least r+s−n. Strict bundle semantics reject a specialization, a scheme-only analogue without the required bridge, one clause/example of a bundled row, or a proper subset as the route for this ID.
Theorem 7.2 — projective dimension theorem
If Y,Z⊆P^n have dimensions r,s, every component of Y∩Z has dimension ≥r+s−n; if r+s−n≥0 then Y∩Z is nonempty.
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 Y,Z⊆P^n have dimensions r,s, every component of Y∩Z has dimension ≥r+s−n; if r+s−n≥0 then Y∩Z is nonempty. Strict bundle semantics reject a specialization, a scheme-only analogue without the required bridge, one clause/example of a bundled row, or a proper subset as the route for this ID.
Definition — numerical polynomial
P(z)∈Q[z] is numerical if P(n)∈Z for all sufficiently large integers n.
Not formalized. none; no complete checked declaration under strict bundle semantics — Pinned/current Mathlib searches found binomial-ring infrastructure and references to integer-valued polynomials, but no definition of Hartshorne’s numerical polynomials (eventual integer values for Q[z]); indexed GitHub Lean search on 2026-09-06 found no exact interface.
Proposition 7.3 — binomial basis and discrete integration for numerical polynomials
A numerical polynomial has an integer-coefficient expansion in binomial polynomials; if Δf eventually equals a numerical polynomial, then f eventually agrees with a numerical polynomial.
Not formalized. none; no complete checked declaration under strict bundle semantics — Pinned/current and indexed searches found no theorem giving the binomial-polynomial basis plus discrete-integration statement for Hartshorne numerical polynomials.
Definitions — graded module, twist, and annihilator
A graded S-module M has M=⊕{d∈Z}M_d with S_dM_e⊆M{d+e}; M(l)d=M{d+l}; Ann M is homogeneous.
Not formalized. none; no complete checked declaration under strict bundle semantics — Pinned Mathlib has graded modules, grading shifts, and annihilators separately, but the audit found no checked route packaging the entire row, including homogeneity of the annihilator, under the source conventions.
Proposition 7.4 — prime filtration of a finite graded module
A finite graded module over noetherian graded S has a filtration with quotients (S/p_i)(l_i); the minimal p_i are the minimal primes of M, and their multiplicities equal lengths of M_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: A finite graded module over noetherian graded S has a filtration with quotients (S/p_i)(l_i); the minimal p_i are the minimal primes of M, and their multiplicities equal lengths of M_p. Strict bundle semantics reject a specialization, a scheme-only analogue without the required bridge, one clause/example of a bundled row, or a proper subset as the route for this ID.
Definition — multiplicity at a minimal prime
For a minimal prime p of graded M, μ_p(M)=length_{S_p}(M_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 a minimal prime p of graded M, μ_p(M)=length_{S_p}(M_p). Strict bundle semantics reject a specialization, a scheme-only analogue without the required bridge, one clause/example of a bundled row, or a proper subset as the route for this ID.
Definition — Hilbert function
For a graded module M over S=k[x_0,…,x_n], the Hilbert function is φ_M(l)=dim_k M_l.
Formalized. LeanCategories/Algebra/DimensionTheory.lean::LeanCategories.Algebra.HilbertFunction — At the current project revision, HilbertFunction sends each graded piece to an additive invariant. Taking the invariant to be k-dimension specializes exactly to Hartshorne’s φ_M(l)=dim_k M_l; this is already project-owned rather than an import/port route.
Searched: A=cd74b69e97f743cd7318a9fe130ed2a749860b3f
Theorem 7.5 — Hilbert–Serre
For finite graded M over k[x_0,…,x_n], φ_M(l)=P_M(l) for l≫0 for a unique P_M∈Q[z], and deg P_M=dim Z(Ann M).
Not formalized. none; no complete checked declaration under strict bundle semantics — Pinned Mathlib/RingTheory/Polynomial/HilbertPoly.lean defines a Hilbert polynomial for rational power-series data and explicitly leaves graded-module Hilbert polynomials for future work. The project has only HilbertFunction/PoincareSeries; no exact Hilbert–Serre theorem for this row is present.
Definition — Hilbert polynomial of a graded module
The eventual polynomial P_M of Theorem 7.5 is the Hilbert polynomial of M.
Not formalized. none; no complete checked declaration under strict bundle semantics — Because the eventual graded-module Hilbert polynomial of U139 is not formalized in the checked sources, Hartshorne’s resulting definition is also unmatched; the same-named pinned polynomial API has different semantics.
Definitions — Hilbert polynomial and degree of a projective algebraic set
For r-dimensional Y⊆P^n, P_Y is the Hilbert polynomial of S(Y); deg Y is r! times the leading coefficient of P_Y.
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked source defines the projective algebraic-set Hilbert polynomial and degree through the leading coefficient of S(Y) in Hartshorne’s classical setting.
Proposition 7.6 — basic properties of degree
Nonempty projective algebraic sets have positive integral degree; degree is additive for equidimensional unions with smaller-dimensional intersection; deg P^n=1; a degree-d hypersurface has degree d.
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked source packages the positivity/integrality, equidimensional-union additivity, projective-space degree, and hypersurface-degree assertions as this complete bundle.
Definition — intersection multiplicity with a hypersurface
If H does not contain projective Y and Z_j is a component of Y∩H with homogeneous prime p_j, define i(Y,H;Z_j)=μ_{p_j}(S/(I_Y+I_H)).
Not formalized. none; no complete checked declaration under strict bundle semantics — Historical/external Lean sources contain plane-curve intersection notions, but no checked compatible declaration realizes Hartshorne’s homogeneous-coordinate-ring multiplicity for an arbitrary hypersurface section, so the broader source definition is unmatched.
Theorem 7.7 — Bézout formula for a hypersurface section
If H does not contain positive-dimensional projective Y and Z_j are the components of Y∩H, then Σ_j i(Y,H;Z_j)deg Z_j=(deg Y)(deg H).
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked project-compatible theorem gives Hartshorne’s projective hypersurface-section Bézout formula with component multiplicities and degrees.
Corollary 7.8 — Bézout theorem for plane curves
For distinct plane curves Y,Z of degrees d,e meeting at P_j, Σ_j i(Y,Z;P_j)=de.
Not formalized. none; no complete checked declaration under strict bundle semantics — Historical Atlas code has nearby plane-curve Bézout/intersection work, but it was not a verified compatible package/import/reference route at the audited revisions; pinned/current Mathlib has no exact theorem, so this row remains unmatched.
Remark 7.8.1 — local and homogeneous intersection multiplicities agree for plane curves
Hartshorne’s homogeneous-coordinate-ring intersection multiplicity agrees with the earlier local definition for intersections of plane curves.
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked declaration proves agreement between Hartshorne’s local and homogeneous intersection-multiplicity definitions for plane curves.
Remark 7.8.2 — Bézout extends to reducible plane curves
The plane-curve Bézout formula extends to reducible one-dimensional algebraic sets provided they share no irreducible component.
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked declaration supplies the reducible-plane-curve extension of Bézout under the no-common-component hypothesis.