Hartshorne, Algebraic Geometry — Chapter II: Schemes
FC06 — Hartshorne, Algebraic Geometry.
This chapter contains 79 definitions, 24 theorems, 59 propositions, 11 lemmas, 17 corollaries, 69 examples, 22 constructions, 28 remarks, 5 conventions and 11 other statements.
Of the 325 statements checked against Lean, 82 are formalized somewhere and 243 are not.
| Status | Statements | Share | What it means |
|---|---|---|---|
| not formalized | 243 | 75% | A documented search found no Lean statement of it anywhere. |
| in Mathlib | 82 | 25% | Mathlib states and proves it. |
| checked in total | 325 |
- Canonical source block: FC06 Hartshorne, Chapter II,
FC06-C02-U001–FC06-C02-U325, in canonical source-ID order. C01 was already promoted and was not modified or regenerated. - Project-first evidence is recorded against
A=cd74b69e97f743cd7318a9fe130ed2a749860b3f. Repository HEAD is3b2239e161592472b34e02ad3b7da308f9ce7280; that later commit changes onlyTODO.md, so no project mathematical declaration changed relative to A. - Pinned Mathlib is
P=db584cd6d46c92f209a44c0f1c829460d327499d, Lean 4.33.0, Apache-2.0 and directly project-compatible. Every Mathlib route promoted in this table was checked at that exact revision. - Current Mathlib evidence was refreshed on 2026-09-06 at
H=5aedf732b6987e8c26ab3c9ebc855314f82b045f, Lean 4.34.0-rc2, Apache-2.0. H/current evidence is used only to close negative gaps; no post-pin declaration is silently treated as project-compatible Mathlib. - The broad C02 project/P/H/open/external/indexed searches already recorded by the concurrent lean-categories audit were reused rather than rerun. This pass only resolved exact declaration boundaries and strict-bundle ambiguities left by those recordings, including sheaf stalk/exactness APIs, affine/Proj ownership, scheme morphism properties, module sheaves, Kähler differentials, and inverse-limit/adic-completion interfaces.
- Strict bundle semantics govern every row. A route owns the entire stable-ID statement. One clause, one example, a specialization, an unbridged classical/scheme analogue, or a theorem with stronger hypotheses than the source is evidence but not a route.
- The basic sheaf, affine
Spec,Proj, scheme-property, separated/proper, module-sheaf, ring-level Kähler, inverse-limit and adic-completion layers have direct pinned owners. The pinned valuative-criterion API exactly owns U083 and U089 after discharging its quasi-separated/quasi-compact side conditions from Hartshorne’s noetherian/finite-type hypotheses. Classical Chapter-I variety bridges, relative projective morphisms, graded-module sheaves onProj, scheme-level differential sheaves, and the formal-scheme layer remain absent where the complete source row is not otherwise realized. - Mathlib’s
IdealSheafDatais credited for rows whose mathematics is exactly the closed-subscheme/ideal correspondence (notably U060, U061, U125 and U127). It is not used to claim Hartshorne’s literalO_X-subsheaf definition U104; Mathlib’s own ideal-sheaf documentation explicitly distinguishes the implementation-level data from an actual subsheaf. - TauCeti at
T=f95596f4ee8cc6cd3e6644aaf04e7fe947364697(Apache-2.0, Lean 4.34.0-rc2; Mathlib5fcc6656691ed31965746c369f41fa75e567ac9d) was checked for U153–U157. It implements Weil divisors viaCodimensionOnePoint,orderAt, principal divisors, linear equivalence and a class group, but no checked formal bridge identifies its codimension-one-point divisor group with Hartshorne prime divisors as closed integral codimension-one subschemes. The plan explicitly rejects unbridged equivalent representations, so U155–U157 remainunmatched, notreference-port. - Ring-level Kähler rows U253–U260 are credited only where the complete algebraic interface exists at P. The stronger differential-dimension/cotangent statements U261–U263 and all scheme-sheaf differential rows from U265 onward remain unmatched absent exact declarations; the existence of ring-level analogues is not sufficient.
Functor.IsMittagLeffler, its stable-image construction, surjective-system criterion, sheaf limits and generic categorical limits give exact routes for U297, U299, U300, U302, U304 and U305. U301 remains unmatched because no checked theorem supplies Hartshorne’s full ML exactness criterion. U307–U308 use the generic module-levelAdicCompletion; the large algebraic bundle U309 and the formal-scheme layer U310–U325 are not inferred from it.N=2026-09-06marks a dated unmatched decision after the recorded project-first, P, H/current, open/current work, indexed search services and relevant external Lean checks. Every unmatched row records exact A/P/H revisions andnoneas its target because no complete route was verified.- Reconciliation against the concurrent promoted C02 artifact changed only nine route rows: U015, U074, U083, U089, U111 and U142 are pinned
mathlib; U155–U157 areunmatched. The retained live decisions for all other 316 rows were not regenerated. Final route counts aremathlib82,project-existing0,package-import0,reference-port0,unmatched243.
Definition — presheaf
A presheaf F on X assigns an abelian group F(U) to each open U and compatible restriction maps F(U)→F(V) for V⊆U, with F(∅)=0, identity, and composition axioms.
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 presheaf F on X assigns an abelian group F(U) to each open U and compatible restriction maps F(U)→F(V) for V⊆U, with F(∅)=0, identity, and composition axioms. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, or a proper subset as the route for this ID.
Convention/comparison — presheaves as contravariant functors
A presheaf is equivalently a contravariant functor Top(X)→Ab; replacing Ab gives presheaves of rings, sets, or objects of another fixed category.
Formalized. Mathlib/Topology/Sheaves/Presheaf.lean::TopCat.Presheaf — Pinned Mathlib realizes the complete source interface for this row: A presheaf is equivalently a contravariant functor Top(X)→Ab; replacing Ab gives presheaves of rings, sets, or objects of another fixed category.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d
Convention/notation — sections and restriction
Elements of F(U) are sections over U, also written Γ(U,F); restriction maps are written s↦s|_V.
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: Elements of F(U) are sections over U, also written Γ(U,F); restriction maps are written s↦s|_V. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, or a proper subset as the route for this ID.
Definition — sheaf
A sheaf is a presheaf satisfying locality and gluing: a section locally zero is zero, and compatible local sections on an open cover glue uniquely.
Formalized. Mathlib/Topology/Sheaves/Sheaf.lean::TopCat.Presheaf.IsSheaf, TopCat.Sheaf; Mathlib/Topology/Sheaves/SheafCondition/UniqueGluing.lean::TopCat.Presheaf.isSheaf_iff_isSheafUniqueGluing — Pinned Mathlib realizes the complete source interface for this row: A sheaf is a presheaf satisfying locality and gluing: a section locally zero is zero, and compatible local sections on an open cover glue uniquely.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d
Example 1.0.1 — sheaf of regular functions
For a variety X, regular functions on open subsets with ordinary restriction maps form a sheaf of rings O_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 variety X, regular functions on open subsets with ordinary restriction maps form a sheaf of rings O_X. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, or a proper subset as the route for this ID.
Example 1.0.2 — standard function sheaves
Continuous real-valued functions, differentiable functions on a manifold, and holomorphic functions on a complex manifold form sheaves.
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: Continuous real-valued functions, differentiable functions on a manifold, and holomorphic functions on a complex manifold form sheaves. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, or a proper subset as the route for this ID.
Example 1.0.3 — constant sheaf
For an abelian group A with the discrete topology, U↦continuous maps U→A defines the constant sheaf; on connected U its sections are 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: For an abelian group A with the discrete topology, U↦continuous maps U→A defines the constant sheaf; on connected U its sections are A. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, or a proper subset as the route for this ID.
Definition — stalk and germs
The stalk F_P is the direct limit of F(U) over neighborhoods U of P; its elements are germs of local sections. For O_X on a variety, O_{X,P} is the local 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: The stalk F_P is the direct limit of F(U) over neighborhoods U of P; its elements are germs of local sections. For O_X on a variety, O_{X,P} is the local ring. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, or a proper subset as the route for this ID.
Definition — morphism of presheaves/sheaves
A morphism F→G is a family of maps on sections commuting with restriction; an isomorphism has a two-sided inverse and induces maps on all stalks.
Formalized. Mathlib/Topology/Sheaves/Sheaf.lean::TopCat.Sheaf; Mathlib/Topology/Sheaves/Stalks.lean::TopCat.Presheaf.stalkFunctor — Pinned Mathlib realizes the complete source interface for this row: A morphism F→G is a family of maps on sections commuting with restriction; an isomorphism has a two-sided inverse and induces maps on all stalks.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d
Proposition 1.1 — stalkwise isomorphism criterion
A morphism of sheaves F→G is an isomorphism iff every induced stalk map F_P→G_P is an isomorphism.
Formalized. Mathlib/Topology/Sheaves/Stalks.lean::isIso_iff_stalkFunctor_map_iso — Pinned Mathlib realizes the complete source interface for this row: A morphism of sheaves F→G is an isomorphism iff every induced stalk map F_P→G_P is an isomorphism.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d
Definition — presheaf kernel, cokernel, image
For a morphism of presheaves φ:F→G, define ker, coker, and im sectionwise by U↦ker φ(U), coker φ(U), and im φ(U).
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 morphism of presheaves φ:F→G, define ker, coker, and im sectionwise by U↦ker φ(U), coker φ(U), and im φ(U). Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, or a proper subset as the route for this ID.
Proposition-Definition 1.2 — associated sheaf
Every presheaf F has an associated sheaf F⁺ with a universal map F→F⁺ through which every map from F to a sheaf factors uniquely; stalks are unchanged and sheaves are fixed up to canonical isomorphism.
Formalized. Mathlib/CategoryTheory/Sites/Sheafification.lean::presheafToSheaf, sheafificationAdjunction, isIso_toSheafify; Mathlib/Topology/Sheaves/Sheafify.lean::sheafifyStalkIso — Pinned Mathlib realizes the complete source interface for this row: Every presheaf F has an associated sheaf F⁺ with a universal map F→F⁺ through which every map from F to a sheaf factors uniquely; stalks are unchanged and sheaves are fixed up to canonical isomorphism.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d
Definition — subsheaf
A subsheaf F′⊆F is a sheaf whose section groups are subgroups compatible with F-restrictions; stalks F′_P embed in F_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 subsheaf F′⊆F is a sheaf whose section groups are subgroups compatible with F-restrictions; stalks F′_P embed in F_P. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, or a proper subset as the route for this ID.
Construction — kernel and injective sheaf morphisms
For sheaves, the presheaf kernel is already a sheaf; φ is injective when ker φ=0, equivalently φ(U) is injective for every open U.
Formalized. Mathlib/Topology/Sheaves/Limits.lean; Mathlib/Topology/Sheaves/Stalks.lean::app_injective_iff_stalkFunctor_map_injective, mono_iff_stalk_mono — Pinned Mathlib creates sheaf limits from presheaf limits, so kernels are computed in the sheaf category, and its stalk/section APIs identify monomorphisms with the expected injectivity conditions.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d
Construction — image and surjective sheaf morphisms
The image sheaf im φ is the sheafification of the presheaf image and embeds in G; φ is surjective when im φ=G.
Formalized. Mathlib/CategoryTheory/Sites/Subsheaf.lean::Sheaf.image, Sheaf.toImage, Sheaf.imageι, imageFactorization — Pinned Mathlib defines the image sheaf as the sheafification of the presheaf range, gives its monomorphism into the target, and gives the epi image factorization; this is exactly Hartshorne’s image/surjective sheaf-morphism construction.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d
Definition — exact sequence of sheaves
A sequence of sheaves is exact when ker φ^i=im φ^{i−1} at every stage; injectivity and surjectivity are the corresponding short exact endpoint conditions.
Formalized. Mathlib/CategoryTheory/Abelian/Exact.lean::ShortComplex.Exact, ShortComplex.exact_iff_image_eq_kernel — Pinned Mathlib realizes the complete source interface for this row: A sequence of sheaves is exact when ker φ^i=im φ^{i−1} at every stage; injectivity and surjectivity are the corresponding short exact endpoint conditions.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d
Construction — quotient sheaf and cokernel
For F′⊆F, the quotient sheaf F/F′ is the sheafification of U↦F(U)/F′(U); coker φ is the sheafification of the presheaf cokernel.
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 F′⊆F, the quotient sheaf F/F′ is the sheafification of U↦F(U)/F′(U); coker φ is the sheafification of the presheaf cokernel. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, or a proper subset as the route for this ID.
Comparison — exactness is stalkwise
Surjectivity need not hold on sections over every open set, but a sheaf morphism is surjective iff all stalk maps are; more generally a sequence of sheaves is exact iff every stalk sequence is exact.
Formalized. Mathlib/Topology/Sheaves/LocallySurjective.lean::locally_surjective_iff_surjective_on_stalks; Mathlib/Topology/Sheaves/Abelian.lean::TopCat.Sheaf.exact_iff_stalkFunctor_map_exact — Pinned Mathlib realizes the complete source interface for this row: Surjectivity need not hold on sections over every open set, but a sheaf morphism is surjective iff all stalk maps are; more generally a sequence of sheaves is exact iff every stalk sequence is exact.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d
Definition — direct and inverse image sheaves
For continuous f:X→Y, (f_*F)(V)=F(f^{-1}V); f^{-1}G is the sheafification of U↦lim_{V⊇f(U)}G(V). These define functors on sheaf categories.
Formalized. Mathlib/Topology/Sheaves/Functors.lean::TopCat.Sheaf.pushforward, TopCat.Sheaf.pullback, TopCat.Sheaf.pullbackPushforwardAdjunction — Pinned Mathlib realizes the complete source interface for this row: For continuous f:X→Y, (f_*F)(V)=F(f^{-1}V); f^{-1}G is the sheafification of U↦lim_{V⊇f(U)}G(V). These define functors on sheaf categories.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d
Definition — restriction of a sheaf
For an inclusion i:Z↪X, the restriction F|_Z means i^{-1}F; its stalk at P∈Z is F_P.
Formalized. Mathlib/Topology/Sheaves/Functors.lean::TopCat.Sheaf.pullback, TopCat.Sheaf.IsOpenEmbedding.sheafPullbackIso; Mathlib/Geometry/RingedSpace/Stalks.lean::PresheafedSpace.restrictStalkIso — Specializing the pinned inverse-image sheaf functor to an open inclusion is restriction; the generic restriction-stalk isomorphism identifies its stalk at a point with the original stalk, exactly the source row.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d
Construction — prime spectrum and V(a)
For a ring A, Spec A is the set of prime ideals; V(a) is the set of primes containing the ideal a.
Formalized. Mathlib/RingTheory/Spectrum/Prime/Basic.lean::PrimeSpectrum; Mathlib/RingTheory/Spectrum/Prime/Topology.lean::PrimeSpectrum.zeroLocus — Pinned Mathlib realizes the complete source interface for this row: For a ring A, Spec A is the set of prime ideals; V(a) is the set of primes containing the ideal a.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d
Lemma 2.1 — closed-set calculus on Spec
For ideals a,b and {a_i}, V(ab)=V(a)∪V(b), V(Σa_i)=∩V(a_i), and V(a)⊆V(b) iff √a⊇√b.
Formalized. Mathlib/RingTheory/Spectrum/Prime/Topology.lean::PrimeSpectrum.zeroLocus_mul, PrimeSpectrum.zeroLocus_iSup; Mathlib/RingTheory/Spectrum/Prime/Basic.lean::PrimeSpectrum.zeroLocus_subset_zeroLocus_iff — Pinned Mathlib realizes the complete source interface for this row: For ideals a,b and {a_i}, V(ab)=V(a)∪V(b), V(Σa_i)=∩V(a_i), and V(a)⊆V(b) iff √a⊇√b.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d
Construction — Zariski topology on Spec
The subsets V(a) are the closed sets of the Zariski topology on Spec A.
Formalized. Mathlib/RingTheory/Spectrum/Prime/Topology.lean::PrimeSpectrum.isClosed_iff_zeroLocus, PrimeSpectrum.isClosed_zeroLocus — Pinned Mathlib realizes the complete source interface for this row: The subsets V(a) are the closed sets of the Zariski topology on Spec A.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d
Construction — structure sheaf on Spec
On U⊆Spec A, O(U) consists of functions with values in A_p locally representable as a/f with f avoiding the relevant primes; these rings and restrictions form a sheaf.
Formalized. Mathlib/AlgebraicGeometry/StructureSheaf.lean; Mathlib/AlgebraicGeometry/AffineScheme.lean::Scheme.Spec — Pinned Mathlib constructs Spec from the prime spectrum equipped with the localization structure sheaf, which is the complete source construction.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d
Definition — spectrum of a ring
The spectrum of A is the topological space Spec A together with the structure sheaf O constructed from local fractions.
Formalized. Mathlib/AlgebraicGeometry/AffineScheme.lean::Scheme.Spec — Pinned Mathlib realizes the complete source interface for this row: The spectrum of A is the topological space Spec A together with the structure sheaf O constructed from local fractions.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d
Construction — basic open D(f)
D(f)=Spec A(f); the D(f) form a basis for the topology on Spec A.
Formalized. Mathlib/RingTheory/Spectrum/Prime/Basic.lean::PrimeSpectrum.basicOpen; Mathlib/AlgebraicGeometry/AffineScheme.lean::Scheme.isBasis_basicOpen — Pinned Mathlib realizes the complete source interface for this row: D(f)=Spec A(f); the D(f) form a basis for the topology on Spec A.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d
Proposition 2.2 — local structure of affine spectra
For X=Spec A: O_{X,p}≅A_p; O_X(D(f))≅A_f; in particular Γ(X,O_X)≅A.
Formalized. Mathlib/AlgebraicGeometry/AffineScheme.lean::Spec.stalkIso, Scheme.basicOpenSectionsToAffine; Mathlib/AlgebraicGeometry/GammaSpecAdjunction.lean::Scheme.ΓSpecIso — Pinned Mathlib realizes the complete source interface for this row: For X=Spec A: O_{X,p}≅A_p; O_X(D(f))≅A_f; in particular Γ(X,O_X)≅A.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d
Definition — ringed and locally ringed spaces
A ringed space is (X,O_X); a morphism is (f,f^#) with f continuous and f^#:O_Y→f_*O_X. It is locally ringed when every stalk is local, and a morphism is locally ringed when all induced stalk maps are local homomorphisms.
Formalized. Mathlib/AlgebraicGeometry/Scheme.lean::Scheme; Mathlib/Topology/Sheaves/LocalPredicate.lean::LocallyRingedSpace — Pinned Mathlib realizes the complete source interface for this row: A ringed space is (X,O_X); a morphism is (f,f^#) with f continuous and f^#:O_Y→f_*O_X. It is locally ringed when every stalk is local, and a morphism is locally ringed when all induced stalk maps are local homomorphisms.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d
Proposition 2.3 — Spec is contravariantly fully faithful on rings
Spec A is locally ringed; a ring homomorphism A→B induces Spec B→Spec A, and every morphism of locally ringed spaces Spec B→Spec A arises uniquely this way.
Formalized. Mathlib/AlgebraicGeometry/GammaSpecAdjunction.lean::Spec.fullyFaithfulToLocallyRingedSpace, Spec.fullyFaithful, Spec.homEquiv — Pinned Mathlib realizes the complete source interface for this row: Spec A is locally ringed; a ring homomorphism A→B induces Spec B→Spec A, and every morphism of locally ringed spaces Spec B→Spec A arises uniquely this way.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d
Comparison — locality is essential for affine morphisms
Without requiring stalk maps to be local homomorphisms, morphisms of ringed spaces between affine spectra need not come from ring homomorphisms.
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: Without requiring stalk maps to be local homomorphisms, morphisms of ringed spaces between affine spectra need not come from ring homomorphisms. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, or a proper subset as the route for this ID.
Definition — affine scheme, scheme, morphism
An affine scheme is a locally ringed space isomorphic to Spec A; a scheme is locally affine. The structure sheaf is O_X, and morphisms/isomorphisms are those of locally ringed spaces.
Formalized. Mathlib/AlgebraicGeometry/AffineScheme.lean::IsAffine, Scheme.isoSpec; Mathlib/AlgebraicGeometry/Scheme.lean::Scheme — Pinned Mathlib realizes the complete source interface for this row: An affine scheme is a locally ringed space isomorphic to Spec A; a scheme is locally affine. The structure sheaf is O_X, and morphisms/isomorphisms are those of locally ringed spaces.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d
Example 2.3.1 — spectrum of a field
Spec k has one point and structure sheaf 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: Spec k has one point and structure sheaf k. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, or a proper subset as the route for this ID.
Example 2.3.2 — spectrum of a DVR
Spec R for a DVR has a closed point with local ring R and an open dense generic point with local ring Frac(R); the local-morphism condition distinguishes the canonical generic-point 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: Spec R for a DVR has a closed point with local ring R and an open dense generic point with local ring Frac(R); the local-morphism condition distinguishes the canonical generic-point map. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, or a proper subset as the route for this ID.
Example 2.3.3 — affine line as a scheme
A^1_k=Spec k[x] has a generic point (0) and closed points given by maximal ideals; over algebraically closed k the closed points correspond to elements of 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: A^1_k=Spec k[x] has a generic point (0) and closed points given by maximal ideals; over algebraically closed k the closed points correspond to elements of k. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, or a proper subset as the route for this ID.
Example 2.3.4 — affine plane and generic curve points
A^2_k=Spec k[x,y] has the classical affine plane as its closed points, a generic point for the whole plane, and a generic point for each irreducible 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^2_k=Spec k[x,y] has the classical affine plane as its closed points, a generic point for the whole plane, and a generic point for each irreducible curve. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, or a proper subset as the route for this ID.
Example 2.3.5 — gluing schemes
Schemes X_1,X_2 with isomorphic open subschemes U_1≅U_2 glue to a scheme obtained by gluing the spaces and compatible structure sheaves.
Formalized. Mathlib/AlgebraicGeometry/Gluing.lean::Scheme.GlueData, Scheme.GlueData.glued — Pinned Mathlib realizes the complete source interface for this row: Schemes X_1,X_2 with isomorphic open subschemes U_1≅U_2 glue to a scheme obtained by gluing the spaces and compatible structure sheaves.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d
Example 2.3.6 — affine line with doubled origin
Gluing two copies of A^1 along A^1{0} produces a nonaffine scheme with doubled origin; it is later the basic nonseparated example.
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: Gluing two copies of A^1 along A^1{0} produces a nonaffine scheme with doubled origin; it is later the basic nonseparated example. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, or a proper subset as the route for this ID.
Construction — Proj S and V(a)
For graded S with irrelevant ideal S_+, Proj S consists of homogeneous primes not containing S_+; homogeneous ideals define subsets V(a).
Formalized. Mathlib/AlgebraicGeometry/ProjectiveSpectrum/Topology.lean::ProjectiveSpectrum, ProjectiveSpectrum.zeroLocus — Pinned Mathlib realizes the complete source interface for this row: For graded S with irrelevant ideal S_+, Proj S consists of homogeneous primes not containing S_+; homogeneous ideals define subsets V(a).
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d
Lemma 2.4 — closed-set calculus on Proj
For homogeneous ideals a,b and {a_i}, V(ab)=V(a)∪V(b) and V(Σa_i)=∩V(a_i).
Formalized. Mathlib/AlgebraicGeometry/ProjectiveSpectrum/Topology.lean::ProjectiveSpectrum.zeroLocus_mul_ideal, ProjectiveSpectrum.zeroLocus_iSup_ideal — Pinned Mathlib realizes the complete source interface for this row: For homogeneous ideals a,b and {a_i}, V(ab)=V(a)∪V(b) and V(Σa_i)=∩V(a_i).
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d
Construction — Zariski topology on Proj
The sets V(a) for homogeneous ideals are the closed sets of the topology on Proj S.
Formalized. Mathlib/AlgebraicGeometry/ProjectiveSpectrum/Topology.lean::ProjectiveSpectrum.zariskiTopology, ProjectiveSpectrum.isClosed_iff_zeroLocus — Pinned Mathlib realizes the complete source interface for this row: The sets V(a) for homogeneous ideals are the closed sets of the topology on Proj S.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d
Construction — structure sheaf on Proj
O on Proj S has stalk targets S_(p), the degree-zero parts of homogeneous localizations, and sections locally represented by same-degree quotients a/f.
Formalized. Mathlib/AlgebraicGeometry/ProjectiveSpectrum/StructureSheaf.lean::Proj.structureSheaf, Proj.stalkIso' — Pinned Mathlib realizes the complete source interface for this row: O on Proj S has stalk targets S_(p), the degree-zero parts of homogeneous localizations, and sections locally represented by same-degree quotients a/f.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d
Definition — Proj as a ringed space
Proj S means the topological space Proj S equipped with the sheaf of rings constructed from degree-zero local fractions.
Formalized. Mathlib/AlgebraicGeometry/ProjectiveSpectrum/StructureSheaf.lean::Proj.toLocallyRingedSpace; Mathlib/AlgebraicGeometry/ProjectiveSpectrum/Scheme.lean::Proj — Pinned Mathlib realizes the complete source interface for this row: Proj S means the topological space Proj S equipped with the sheaf of rings constructed from degree-zero local fractions.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d
Proposition 2.5 — standard affine cover of Proj
For p∈Proj S, O_p≅S_(p). The opens D_+(f) for homogeneous f∈S_+ cover Proj S and are isomorphic to Spec S_(f); hence Proj S is a scheme.
Formalized. Mathlib/AlgebraicGeometry/ProjectiveSpectrum/Basic.lean::Proj.basicOpen, Proj.isBasis_basicOpen, Proj.basicOpenIsoSpec, Proj.stalkIso — Pinned Mathlib realizes the complete source interface for this row: For p∈Proj S, O_p≅S_(p). The opens D_+(f) for homogeneous f∈S_+ cover Proj S and are isomorphic to Spec S_(f); hence Proj S is a scheme.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d
Example 2.5.1 — projective space over a ring
P^n_A is defined as Proj A[x_0,…,x_n]; over algebraically closed k its closed-point subspace is classical projective n-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: P^n_A is defined as Proj A[x_0,…,x_n]; over algebraically closed k its closed-point subspace is classical projective n-space. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, or a proper subset as the route for this ID.
Definition — schemes over a base
A scheme over S is a scheme X with a morphism X→S; an S-morphism commutes with structure maps. Sch(S) denotes their category.
Formalized. Mathlib/CategoryTheory/Comma/Over/Basic.lean::CategoryTheory.Over — The generic over-category applied to schemes is exactly the category of schemes equipped with a structure morphism to the fixed base and morphisms commuting with those maps.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d
Proposition 2.6 — varieties embed fully faithfully in schemes
For algebraically closed k there is a fully faithful functor t:Var(k)→Sch(k); the original variety is the closed-point subspace of t(V), and its regular-function sheaf is the restriction of O_{t(V)}.
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 algebraically closed k there is a fully faithful functor t:Var(k)→Sch(k); the original variety is the closed-point subspace of t(V), and its regular-function sheaf is the restriction of O_{t(V)}. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, or a proper subset as the route for this ID.
Definition — connected and irreducible schemes
A scheme is connected or irreducible exactly when its underlying topological space is.
Formalized. Mathlib/Topology/Connected/Basic.lean::ConnectedSpace; Mathlib/Topology/Irreducible.lean::IrreducibleSpace — Pinned Mathlib realizes the complete source interface for this row: A scheme is connected or irreducible exactly when its underlying topological space is.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d
Definition — reduced scheme
X is reduced when O_X(U) has no nonzero nilpotents for every open U; equivalently all local rings O_{X,P} are reduced.
Formalized. Mathlib/AlgebraicGeometry/Properties.lean::IsReduced, isReduced_of_isReduced_stalk — Pinned Mathlib realizes the complete source interface for this row: X is reduced when O_X(U) has no nonzero nilpotents for every open U; equivalently all local rings O_{X,P} are reduced.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d
Definition — integral scheme
X is integral when O_X(U) is an integral domain for every open U.
Formalized. Mathlib/AlgebraicGeometry/Properties.lean::IsIntegral — Pinned Mathlib realizes the complete source interface for this row: X is integral when O_X(U) is an integral domain for every open U.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d
Example 3.0.1 — affine irreducible/reduced/integral criteria
For X=Spec A: irreducible iff nil(A) is prime; reduced iff nil(A)=0; integral iff A is a domain.
Formalized. Mathlib/RingTheory/Spectrum/Prime/Topology.lean::PrimeSpectrum.irreducibleSpace_iff_isPrime_nilradical; Mathlib/AlgebraicGeometry/Properties.lean::affine_isReduced_iff, affine_isIntegral_iff — Pinned Mathlib realizes the complete source interface for this row: For X=Spec A: irreducible iff nil(A) is prime; reduced iff nil(A)=0; integral iff A is a domain.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d
Proposition 3.1 — integral iff reduced and irreducible
A scheme is integral iff it is both reduced and irreducible.
Formalized. Mathlib/AlgebraicGeometry/Properties.lean::isIntegral_iff_irreducibleSpace_and_isReduced — Pinned Mathlib realizes the complete source interface for this row: A scheme is integral iff it is both reduced and irreducible.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d
Definition — locally noetherian and noetherian schemes
X is locally noetherian if it has an affine cover by spectra of noetherian rings; it is noetherian if additionally quasi-compact, equivalently it has a finite such affine cover.
Formalized. Mathlib/AlgebraicGeometry/Noetherian.lean::IsLocallyNoetherian, IsNoetherian — Pinned Mathlib realizes the complete source interface for this row: X is locally noetherian if it has an affine cover by spectra of noetherian rings; it is noetherian if additionally quasi-compact, equivalently it has a finite such affine cover.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d
Comparison — scheme noetherianity is stronger than topological noetherianity
A noetherian scheme has a noetherian underlying space, but the converse need not hold.
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 noetherian scheme has a noetherian underlying space, but the converse need not hold. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, or a proper subset as the route for this ID.
Proposition 3.2 — noetherianity is affine-local
X is locally noetherian iff every open affine Spec A⊆X has A noetherian; in particular Spec A is noetherian iff A is noetherian.
Formalized. Mathlib/AlgebraicGeometry/Noetherian.lean::isLocallyNoetherian_iff_of_affine_openCover, isNoetherian_Spec — Pinned Mathlib realizes the complete source interface for this row: X is locally noetherian iff every open affine Spec A⊆X has A noetherian; in particular Spec A is noetherian iff A is noetherian.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d
Definition — locally of finite type and finite type morphisms
f:X→Y is locally of finite type if over an affine cover Spec B_i of Y, f^{-1}(Spec B_i) has affine covers Spec A_ij with A_ij finitely generated over B_i; finite type additionally requires finite such covers.
Formalized. Mathlib/AlgebraicGeometry/Morphisms/FiniteType.lean::LocallyOfFiniteType, FiniteType — Pinned Mathlib realizes the complete source interface for this row: f:X→Y is locally of finite type if over an affine cover Spec B_i of Y, f^{-1}(Spec B_i) has affine covers Spec A_ij with A_ij finitely generated over B_i; finite type additionally requires finite such covers.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d
Definition — finite morphism
f:X→Y is finite if over an affine cover Spec B_i of Y, each inverse image is affine Spec A_i with A_i finite as a B_i-module.
Formalized. Mathlib/AlgebraicGeometry/Morphisms/Finite.lean::IsFinite — Pinned Mathlib realizes the complete source interface for this row: f:X→Y is finite if over an affine cover Spec B_i of Y, each inverse image is affine Spec A_i with A_i finite as a B_i-module.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d
Example 3.2.1 — associated variety schemes
For a variety V over algebraically closed k, t(V) is integral, noetherian, and of finite type over 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: For a variety V over algebraically closed k, t(V) is integral, noetherian, and of finite type over k. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, or a proper subset as the route for this ID.
Example 3.2.2 — local spectra need not be finite type
For P on a variety V, Spec O_{V,P} is integral and noetherian but generally not of finite type over 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: For P on a variety V, Spec O_{V,P} is integral and noetherian but generally not of finite type over k. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, or a proper subset as the route for this ID.
Definition — open subscheme and open immersion
An open subscheme has an open underlying subset with restricted structure sheaf; an open immersion identifies its source with an open subscheme.
Formalized. Mathlib/AlgebraicGeometry/OpenImmersion.lean::IsOpenImmersion — Pinned Mathlib realizes the complete source interface for this row: An open subscheme has an open underlying subset with restricted structure sheaf; an open immersion identifies its source with an open subscheme.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d
Definition — closed immersion and closed subscheme
A closed immersion Y→X is a homeomorphism onto a closed subset with O_X→i_*O_Y surjective; closed subschemes are closed immersions modulo isomorphism over X.
Formalized. Mathlib/AlgebraicGeometry/Morphisms/ClosedImmersion.lean::IsClosedImmersion, IsClosedImmersion.overEquivIdealSheafData — Pinned Mathlib realizes the complete source interface for this row: A closed immersion Y→X is a homeomorphism onto a closed subset with O_X→i_*O_Y surjective; closed subschemes are closed immersions modulo isomorphism over X.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d
Example 3.2.3 — ideals define affine closed subschemes
For a⊆A, Spec(A/a)→Spec A is a closed immersion onto V(a); every ideal therefore defines a closed subscheme structure on V(a).
Formalized. Mathlib/AlgebraicGeometry/IdealSheaf/Basic.lean::Scheme.IdealSheafData.equivOfIsAffine; Mathlib/AlgebraicGeometry/Morphisms/ClosedImmersion.lean::IsClosedImmersion.overEquivIdealSheafData — Pinned Mathlib realizes the complete source interface for this row: For a⊆A, Spec(A/a)→Spec A is a closed immersion onto V(a); every ideal therefore defines a closed subscheme structure on V(a).
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d
Example 3.2.4 — nilpotent and embedded structures in A²
Ideals (xy), (x²), and (x²,xy) in k[x,y] exhibit respectively reducible, everywhere nonreduced, and embedded-point closed subscheme structures.
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: Ideals (xy), (x²), and (x²,xy) in k[x,y] exhibit respectively reducible, everywhere nonreduced, and embedded-point closed subscheme structures. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, or a proper subset as the route for this ID.
Example 3.2.5 — infinitesimal neighborhoods
If W⊆V corresponds to prime p and Y=t(W)⊆X=t(V), the closed subscheme Y_n defined by p^n is the nth infinitesimal neighborhood; n>1 is generally nonreduced.
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 W⊆V corresponds to prime p and Y=t(W)⊆X=t(V), the closed subscheme Y_n defined by p^n is the nth infinitesimal neighborhood; n>1 is generally nonreduced. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, or a proper subset as the route for this ID.
Example 3.2.6 — reduced induced closed subscheme
Every closed subset Y⊆X has a canonical reduced induced closed subscheme structure, obtained affinely from the intersection of primes in Y and glued across affine opens.
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 closed subset Y⊆X has a canonical reduced induced closed subscheme structure, obtained affinely from the intersection of primes in Y and glued across affine opens. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, or a proper subset as the route for this ID.
Definition — dimension and codimension of schemes
dim X is the topological dimension. For irreducible closed Z⊆X, codim(Z,X) is the supremum of lengths of irreducible chains starting at Z; for closed Y take the infimum over irreducible Z⊆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: dim X is the topological dimension. For irreducible closed Z⊆X, codim(Z,X) is the supremum of lengths of irreducible chains starting at Z; for closed Y take the infimum over irreducible Z⊆Y. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, or a proper subset as the route for this ID.
Example 3.2.7 — dimension of an affine scheme
For X=Spec A, dim X equals the Krull dimension of A.
Formalized. Mathlib/RingTheory/Spectrum/Prime/Topology.lean::PrimeSpectrum.topologicalKrullDim_eq_ringKrullDim — Pinned Mathlib realizes the complete source interface for this row: For X=Spec A, dim X equals the Krull dimension of A.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d
Comparison — dimension formula need not hold for arbitrary schemes
For integral finite-type schemes over a field, dim Y+codim(Y,X)=dim X for irreducible closed Y; such behavior can fail on arbitrary noetherian schemes.
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 integral finite-type schemes over a field, dim Y+codim(Y,X)=dim X for irreducible closed Y; such behavior can fail on arbitrary noetherian schemes. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, or a proper subset as the route for this ID.
Definition — fibre product
For X,Y over S, X×_S Y with projections is characterized by the usual universal property for pairs of S-compatible morphisms.
Formalized. Mathlib/CategoryTheory/Limits/Shapes/Pullback/HasPullback.lean::pullback.isLimit — Pinned Mathlib realizes the complete source interface for this row: For X,Y over S, X×_S Y with projections is characterized by the usual universal property for pairs of S-compatible morphisms.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d
Convention — product over Spec Z
For schemes with no stated base, X×Y means X×_{Spec Z}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 schemes with no stated base, X×Y means X×_{Spec Z}Y. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, or a proper subset as the route for this ID.
Theorem 3.3 — existence of fibre products
Fibre products of schemes over any base S exist and are unique up to unique isomorphism; affinely Spec A×_{Spec R}Spec B≅Spec(A⊗_R B).
Formalized. Mathlib/AlgebraicGeometry/Pullbacks.lean::AlgebraicGeometry.pullbackSpecIso — Pinned Mathlib realizes the complete source interface for this row: Fibre products of schemes over any base S exist and are unique up to unique isomorphism; affinely Spec A×_{Spec R}Spec B≅Spec(A⊗_R B).
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d
Definition — fibre of a morphism
For f:X→Y and y∈Y with residue field k(y), the fibre is X_y=X×_Y Spec k(y); its underlying space is f^{-1}(y).
Formalized. Mathlib/AlgebraicGeometry/Fiber.lean::Scheme.Hom.fiber, Spec.fiberToSpecResidueFieldIso, Scheme.Hom.fiberHomeo — Pinned Mathlib realizes the complete source interface for this row: For f:X→Y and y∈Y with residue field k(y), the fibre is X_y=X×_Y Spec k(y); its underlying space is f^{-1}(y).
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d
Construction — families and deformations
A family of deformations of X_0/k is a morphism f:X→Y with Y connected and a k-rational y_0 such that X_{y_0}≅X_0; other fibres are deformations.
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 family of deformations of X_0/k is a morphism f:X→Y with Y connected and a k-rational y_0 such that X_{y_0}≅X_0; other fibres are deformations. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, or a proper subset as the route for this ID.
Construction — reduction modulo p
For X over Spec Z, the generic fibre X_Q is over Q and the fibre X_p over a closed prime p is over F_p; X_p is the reduction mod 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 X over Spec Z, the generic fibre X_Q is over Q and the fibre X_p over a closed prime p is over F_p; X_p is the reduction mod p. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, or a proper subset as the route for this ID.
Construction — base extension
Given S′→S and X/S, the base extension is X_{S′}=X×_S S′; base extension is transitive up to canonical isomorphism.
Formalized. Mathlib/CategoryTheory/Comma/Over/Pullback.lean::CategoryTheory.Over.pullback; Mathlib/CategoryTheory/Limits/Shapes/Pullback/Pasting.lean::pullbackRightPullbackFstIso; Mathlib/AlgebraicGeometry/Pullbacks.lean — Schemes have pullbacks at the pin; the over-category pullback is base extension and the canonical pullback-pasting isomorphism gives transitivity up to canonical isomorphism.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d
Comparison — stability under base extension
Finite type is stable under arbitrary base extension; integrality of schemes need not be, as fibres/base changes may become reducible or nonreduced.
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: Finite type is stable under arbitrary base extension; integrality of schemes need not be, as fibres/base changes may become reducible or nonreduced. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, or a proper subset as the route for this ID.
Example 3.3.1 — family with nonreduced special fibre
The family ay=x² over A¹ has integral total/base schemes and irreducible reduced fibres for a≠0, but special fibre x²=0 is nonreduced.
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 family ay=x² over A¹ has integral total/base schemes and irreducible reduced fibres for a≠0, but special fibre x²=0 is nonreduced. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, or a proper subset as the route for this ID.
Example 3.3.2 — family with reducible special fibre
The family xy=t has irreducible hyperbola fibres for t≠0 and special fibre xy=0, the union of two lines.
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 family xy=t has irreducible hyperbola fibres for t≠0 and special fibre xy=0, the union of two lines. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, or a proper subset as the route for this ID.
Definition — diagonal morphism and separated morphism
For f:X→Y, the diagonal Δ:X→X×_Y X is the unique map whose two projections are id_X. The morphism f is separated when Δ is a closed immersion; X is separated when separated over Spec Z.
Formalized. Mathlib/AlgebraicGeometry/Morphisms/Separated.lean::IsSeparated, IsSeparated.isSeparated_eq_diagonal_isClosedImmersion — Pinned Mathlib realizes the complete source interface for this row: For f:X→Y, the diagonal Δ:X→X×_Y X is the unique map whose two projections are id_X. The morphism f is separated when Δ is a closed immersion; X is separated when separated over Spec Z.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d
Example 4.0.1 — doubled-origin line is not separated
The affine line with doubled origin is not separated over k: its diagonal misses two origins lying in the closure of the diagonal image.
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 affine line with doubled origin is not separated over k: its diagonal misses two origins lying in the closure of the diagonal image. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, or a proper subset as the route for this ID.
Example 4.0.2 — associated varieties are separated
For every variety V over algebraically closed k, the associated scheme t(V) is separated over 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: For every variety V over algebraically closed k, the associated scheme t(V) is separated over k. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, or a proper subset as the route for this ID.
Proposition 4.1 — affine morphisms are separated
Every morphism of affine schemes is separated.
Formalized. Mathlib/AlgebraicGeometry/Morphisms/Separated.lean::IsSeparated.of_isAffineHom — Pinned Mathlib realizes the complete source interface for this row: Every morphism of affine schemes is separated.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d
Corollary 4.2 — topological diagonal criterion
A morphism f:X→Y is separated iff the image Δ(X) is closed in X×_Y 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: A morphism f:X→Y is separated iff the image Δ(X) is closed in X×_Y X. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, or a proper subset as the route for this ID.
Theorem 4.3 — valuative criterion of separatedness
If X is noetherian, f:X→Y is separated iff for every valuation ring R with fraction field K, any two Y-morphisms Spec R→X agreeing on Spec K are equal.
Formalized. Mathlib/AlgebraicGeometry/ValuativeCriterion.lean::IsSeparated.eq_valuativeCriterion, IsSeparated.valuativeCriterion; Mathlib/AlgebraicGeometry/Noetherian.lean::IsLocallyNoetherian.quasiSeparatedSpace; Mathlib/AlgebraicGeometry/Morphisms/QuasiSeparated.lean::QuasiSeparated.of_quasiSeparatedSpace — Pinned Mathlib identifies separatedness with uniqueness in all valuation-ring lifting diagrams plus quasi-separatedness. The source hypothesis that X is noetherian supplies quasi-separatedness for every X→Y, so this specializes exactly to Hartshorne Theorem 4.3.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d
Lemma 4.4 — maps from a valuation spectrum
A map Spec K→X is a point x₁ with k(x₁)↪K. A map Spec R→X is a specialization x₀ of x₁ together with such a field inclusion for which R dominates the local ring of x₀ on the reduced closure 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: A map Spec K→X is a point x₁ with k(x₁)↪K. A map Spec R→X is a specialization x₀ of x₁ together with such a field inclusion for which R dominates the local ring of x₀ on the reduced closure of x₁. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, or a proper subset as the route for this ID.
Lemma 4.5 — quasi-compact image criterion
For a quasi-compact morphism f:X→Y, f(X) is closed iff it is stable under specialization.
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-compact morphism f:X→Y, f(X) is closed iff it is stable under specialization. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, or a proper subset as the route for this ID.
Corollary 4.6 — stability properties of separated morphisms
For noetherian schemes: open/closed immersions are separated; separated morphisms are closed under composition, base change, and products; if g∘f is separated then f is; and separatedness is local on the base.
Formalized. Mathlib/AlgebraicGeometry/Morphisms/Separated.lean::IsSeparated.stableUnderComposition, IsSeparated.isStableUnderBaseChange, IsSeparated.of_comp — Pinned Mathlib realizes the complete source interface for this row: For noetherian schemes: open/closed immersions are separated; separated morphisms are closed under composition, base change, and products; if g∘f is separated then f is; and separatedness is local on the base.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d
Definition — proper and universally closed morphisms
f:X→Y is proper when it is separated, of finite type, and universally closed; universally closed means every base change is a closed map.
Formalized. Mathlib/AlgebraicGeometry/Morphisms/Proper.lean::IsProper; Mathlib/AlgebraicGeometry/Morphisms/UniversallyClosed.lean::UniversallyClosed — Pinned Mathlib realizes the complete source interface for this row: f:X→Y is proper when it is separated, of finite type, and universally closed; universally closed means every base change is a closed map.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d
Example 4.6.1 — affine line is not proper
A¹_k is separated and finite type but not proper: after base change, projection A²→A¹ sends the closed hyperbola xy=1 to A¹{0}, which is not closed.
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¹_k is separated and finite type but not proper: after base change, projection A²→A¹ sends the closed hyperbola xy=1 to A¹{0}, which is not closed. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, or a proper subset as the route for this ID.
Theorem 4.7 — valuative criterion of properness
If f:X→Y is finite type with X noetherian, then f is proper iff every commutative diagram Spec K→X over Spec R→Y for a valuation ring R has a unique lift Spec R→X.
Formalized. Mathlib/AlgebraicGeometry/ValuativeCriterion.lean::IsProper.eq_valuativeCriterion, IsProper.of_valuativeCriterion; Mathlib/AlgebraicGeometry/Noetherian.lean::quasiCompact_of_noetherianSpace_source, IsLocallyNoetherian.quasiSeparatedSpace; Mathlib/AlgebraicGeometry/Morphisms/FiniteType.lean::FiniteType — Pinned Mathlib identifies properness with the full valuation-ring lifting criterion together with quasi-compactness, quasi-separatedness and local finite type. Hartshorne’s finite-type plus noetherian-source hypotheses supply those auxiliary conditions, yielding the stated iff criterion.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d
Corollary 4.8 — stability properties of proper morphisms
For noetherian schemes: closed immersions are proper; proper morphisms are closed under composition, base change, and products; if g∘f is proper and g separated then f is proper; properness is local on the base.
Formalized. Mathlib/AlgebraicGeometry/Morphisms/Proper.lean::IsProper.stableUnderComposition, IsProper.isStableUnderBaseChange, IsProper.of_comp — Pinned Mathlib realizes the complete source interface for this row: For noetherian schemes: closed immersions are proper; proper morphisms are closed under composition, base change, and products; if g∘f is proper and g separated then f is proper; properness is local on the base.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d
Definition — projective and quasi-projective morphisms
Pn_Y=Pn_Z×Y. A morphism X→Y is projective if it factors as a closed immersion into P^n_Y followed by projection; it is quasi-projective if it factors as an open immersion followed by a projective 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: Pn_Y=Pn_Z×Y. A morphism X→Y is projective if it factors as a closed immersion into P^n_Y followed by projection; it is quasi-projective if it factors as an open immersion followed by a projective morphism. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, or a proper subset as the route for this ID.
Example 4.8.1 — Proj of a degree-one generated algebra is projective
If S_0=A and S is finitely generated over A by S_1, then Proj S→Spec A is projective via a closed immersion into projective 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: If S_0=A and S is finitely generated over A by S_1, then Proj S→Spec A is projective via a closed immersion into projective space. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, or a proper subset as the route for this ID.
Theorem 4.9 — projective implies proper
A projective morphism of noetherian schemes is proper; a quasi-projective morphism of noetherian schemes is finite type and separated.
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 morphism of noetherian schemes is proper; a quasi-projective morphism of noetherian schemes is finite type and separated. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, or a proper subset as the route for this ID.
Proposition 4.10 — scheme-theoretic image of classical varieties
Over algebraically closed k, the essential image of t:Var(k)→Sch(k) is exactly the quasi-projective integral k-schemes; projective varieties correspond to projective integral k-schemes. Thus t(V) is integral, separated, finite type.
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, the essential image of t:Var(k)→Sch(k) is exactly the quasi-projective integral k-schemes; projective varieties correspond to projective integral k-schemes. Thus t(V) is integral, separated, finite type. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, or a proper subset as the route for this ID.
Definition — abstract variety and complete variety
An abstract variety over algebraically closed k is an integral separated finite-type k-scheme; it is complete when proper over k.
Formalized. Mathlib/AlgebraicGeometry/Properties.lean::IsIntegral; Mathlib/AlgebraicGeometry/Morphisms/Separated.lean::Scheme.IsSeparated; Mathlib/AlgebraicGeometry/Morphisms/FiniteType.lean::FiniteType; Mathlib/AlgebraicGeometry/Morphisms/Proper.lean::IsProper — Mathlib represents Hartshorne’s abstract-variety convention propositionally by the conjunction of the exact integral, separated and finite-type scheme predicates; completeness is exactly properness over the base field.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d
Remark 4.10.1 — scheme-theoretic variety convention
From here on, “variety” means abstract variety; Chapter-I varieties are identified with their associated quasi-projective schemes; curve/surface/threefold mean dimensions 1/2/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: From here on, “variety” means abstract variety; Chapter-I varieties are identified with their associated quasi-projective schemes; curve/surface/threefold mean dimensions 1/2/3. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, or a proper subset as the route for this ID.
Remark 4.10.2 — complete versus projective varieties
Complete curves are projective and nonsingular complete surfaces are projective, but complete nonprojective varieties exist in dimensions ≥2; every variety admits an open dense embedding into a complete 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: Complete curves are projective and nonsingular complete surfaces are projective, but complete nonprojective varieties exist in dimensions ≥2; every variety admits an open dense embedding into a complete variety. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, or a proper subset as the route for this ID.
Theorem 4.11A — integral closure as intersection of valuation rings
For A⊆K a field, the integral closure of A in K is the intersection of all valuation rings of K containing A.
Formalized. Mathlib/RingTheory/Valuation/LocalSubring.lean::Subring.eq_iInf_of_isIntegrallyClosedIn, iInf_valuationSubring_superset — Pinned Mathlib realizes the complete source interface for this row: For A⊆K a field, the integral closure of A in K is the intersection of all valuation rings of K containing A.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d
Definitions — sheaf of modules and module morphism
An O_X-module is a sheaf F whose F(U) are O_X(U)-modules compatibly with restrictions; a morphism is O_X-linear on every open set.
Formalized. Mathlib/AlgebraicGeometry/Modules/Sheaf.lean::Scheme.Modules, Scheme.Modules.Hom — Pinned Mathlib realizes the complete source interface for this row: An O_X-module is a sheaf F whose F(U) are O_X(U)-modules compatibly with restrictions; a morphism is O_X-linear on every open set.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d
Construction/convention — exact and additive operations on OX-modules
Kernels, cokernels, images, quotients, sums, products, direct/inverse limits remain O_X-modules; Hom_X(F,G) denotes module morphisms; exactness is exactness of underlying abelian sheaves.
Formalized. Mathlib/AlgebraicGeometry/Modules/Sheaf.lean::Scheme.Modules; Mathlib/Algebra/Category/ModuleCat/Sheaf/Abelian.lean; Mathlib/Algebra/Category/ModuleCat/Sheaf/Limits.lean::SheafOfModules.hasLimitsOfShape; Mathlib/Algebra/Category/ModuleCat/Sheaf/Colimits.lean — Pinned Mathlib makes Scheme.Modules an abelian category with all limits and colimits. Hence kernels, cokernels, images, quotients, sums, products and direct/inverse limits remain sheaves of modules and exactness is categorical exactness of the underlying abelian sheaves.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d
Construction — internal sheaf Hom
The assignment U↦Hom_{O_X|U}(F|U,G|U) is a sheaf O_X-module, denoted Hom_OX(F,G).
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 assignment U↦Hom_{O_X|U}(F|U,G|U) is a sheaf O_X-module, denoted Hom_OX(F,G). Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, or a proper subset as the route for this ID.
Construction — tensor product of sheaves of modules
F⊗{O_X}G is the sheafification of U↦F(U)⊗{O_X(U)}G(U).
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⊗{O_X}G is the sheafification of U↦F(U)⊗{O_X(U)}G(U). Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, or a proper subset as the route for this ID.
Definition — free, locally free, rank, invertible sheaf
F is free if a direct sum of copies of O_X; locally free if so on an open cover. Rank is the local number of copies, constant on connected X; rank one means invertible.
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 is free if a direct sum of copies of O_X; locally free if so on an open cover. Rank is the local number of copies, constant on connected X; rank one means invertible. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, or a proper subset as the route for this ID.
Definition — sheaf of ideals
A sheaf of ideals I on X is an O_X-submodule of O_X, equivalently I(U) is an ideal of O_X(U) for every open U.
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 sheaf of ideals I on X is an O_X-submodule of O_X, equivalently I(U) is an ideal of O_X(U) for every open U. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, or a proper subset as the route for this ID.
Construction — direct image of modules
For f:(X,O_X)→(Y,O_Y) and O_X-module F, f_F becomes an O_Y-module via O_Y→f_O_X.
Formalized. Mathlib/AlgebraicGeometry/Modules/Sheaf.lean::Scheme.Modules.pushforward — Pinned Mathlib realizes the complete source interface for this row: For f:(X,O_X)→(Y,O_Y) and O_X-module F, f_F becomes an O_Y-module via O_Y→f_O_X.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d
Construction — inverse image/pullback of modules
For an O_Y-module G, define f^*G=f^{-1}G⊗_{f^{-1}O_Y}O_X; it is an O_X-module.
Formalized. Mathlib/AlgebraicGeometry/Modules/Sheaf.lean::Scheme.Modules.pullback — Pinned Mathlib realizes the complete source interface for this row: For an O_Y-module G, define f^*G=f^{-1}G⊗_{f^{-1}O_Y}O_X; it is an O_X-module.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d
Comparison — pullback/direct-image adjunction
For O_X-module F and O_Y-module G there is a natural isomorphism Hom_X(f^G,F)≅Hom_Y(G,f_F).
Formalized. Mathlib/AlgebraicGeometry/Modules/Sheaf.lean::Scheme.Modules.pullbackPushforwardAdjunction — Pinned Mathlib realizes the complete source interface for this row: For O_X-module F and O_Y-module G there is a natural isomorphism Hom_X(f^G,F)≅Hom_Y(G,f_F).
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d
Definition — sheaf associated to a module on Spec
For A-module M, the sheaf M~ on Spec A has stalk values M_p and sections locally represented by fractions m/f.
Formalized. Mathlib/AlgebraicGeometry/Modules/Tilde.lean::AlgebraicGeometry.tilde — Pinned Mathlib realizes the complete source interface for this row: For A-module M, the sheaf M~ on Spec A has stalk values M_p and sections locally represented by fractions m/f.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d
Proposition 5.1 — affine associated-sheaf properties
For X=Spec A: M~ is an O_X-module, (M~)_p≅M_p, Γ(D(f),M~)≅M_f, and Γ(X,M~)≅M.
Formalized. Mathlib/AlgebraicGeometry/Modules/Tilde.lean::AlgebraicGeometry.tilde, tilde.toTildeΓNatIso, tilde.isoTop — Pinned Mathlib realizes the complete source interface for this row: For X=Spec A: M~ is an O_X-module, (M~)_p≅M_p, Γ(D(f),M~)≅M_f, and Γ(X,M~)≅M.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d
Proposition 5.2 — functoriality of associated sheaves
M↦M~ is exact and fully faithful; it commutes with tensor products and direct sums. For Spec B→Spec A, direct image corresponds to restriction of scalars and pullback to M⊗_A B.
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: M↦M~ is exact and fully faithful; it commutes with tensor products and direct sums. For Spec B→Spec A, direct image corresponds to restriction of scalars and pullback to M⊗_A B. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, or a proper subset as the route for this ID.
Definition — quasi-coherent and coherent sheaves
An O_X-module F is quasi-coherent if locally on affine U_i=Spec A_i it is M_i~; it is coherent if the M_i can be finitely generated (normally used on noetherian schemes).
Formalized. Mathlib/Algebra/Category/ModuleCat/Sheaf/Quasicoherent.lean::SheafOfModules.IsQuasicoherent; Mathlib/Algebra/Category/ModuleCat/Sheaf/Generators.lean::SheafOfModules.IsFiniteType; Mathlib/AlgebraicGeometry/Modules/Tilde.lean::Scheme.Modules.isQuasicoherent_iff_isIso_fromTildeΓ — Pinned Mathlib formalizes quasi-coherence by local presentations and proves the affine tilde/global-sections characterization; its finite-type module-sheaf predicate is local finite generation. Their conjunction realizes Hartshorne’s quasi-coherent/coherent definition used here.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d
Example 5.2.1 — structure sheaf is quasi-coherent/coherent
O_X is quasi-coherent, in fact coherent, on every scheme.
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_X is quasi-coherent, in fact coherent, on every scheme. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, or a proper subset as the route for this ID.
Example 5.2.2 — structure sheaf of an affine closed subscheme
If X=Spec A and Y=Spec(A/a) is closed with inclusion i, then i_*O_Y≅(A/a)~, hence is quasi-coherent and coherent.
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=Spec A and Y=Spec(A/a) is closed with inclusion i, then i_*O_Y≅(A/a)~, hence is quasi-coherent and coherent. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, or a proper subset as the route for this ID.
Example 5.2.3 — extension by zero need not be quasi-coherent
For an open immersion j:U→X, extension by zero j_!O_U is an O_X-module but need not be quasi-coherent.
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 open immersion j:U→X, extension by zero j_!O_U is an O_X-module but need not be quasi-coherent. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, or a proper subset as the route for this ID.
Example 5.2.4 — topological restriction need not be an OY-module
For a closed subscheme Y⊆X, the sheaf O_X|_Y is generally not quasi-coherent on Y and may not even carry an O_Y-module structure.
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 subscheme Y⊆X, the sheaf O_X|_Y is generally not quasi-coherent on Y and may not even carry an O_Y-module structure. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, or a proper subset as the route for this ID.
Example 5.2.5 — constant function-field sheaf
On an integral noetherian scheme, the constant sheaf K of the function field is quasi-coherent but not coherent unless X is a 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: On an integral noetherian scheme, the constant sheaf K of the function field is quasi-coherent but not coherent unless X is a point. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, or a proper subset as the route for this ID.
Lemma 5.3 — sections on a principal affine open
For quasi-coherent F on X=Spec A and D(f): a global section restricting to zero is killed by some f^n; every section on D(f), after multiplication by some f^n, extends globally.
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 quasi-coherent F on X=Spec A and D(f): a global section restricting to zero is killed by some f^n; every section on D(f), after multiplication by some f^n, extends globally. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, or a proper subset as the route for this ID.
Proposition 5.4 — affine-local criterion for quasi-coherence/coherence
F is quasi-coherent iff on every affine open Spec A it is M~; if X is noetherian, coherence is equivalently the same with M finitely generated.
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 is quasi-coherent iff on every affine open Spec A it is M~; if X is noetherian, coherence is equivalently the same with M finitely generated. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, or a proper subset as the route for this ID.
Corollary 5.5 — modules versus quasi-coherent sheaves on affine schemes
For X=Spec A, M↦M~ and Γ(X,−) are inverse equivalences A-Mod≃QCoh(X); for noetherian A they restrict to finite A-modules≃coherent sheaves.
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=Spec A, M↦M~ and Γ(X,−) are inverse equivalences A-Mod≃QCoh(X); for noetherian A they restrict to finite A-modules≃coherent sheaves. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, or a proper subset as the route for this ID.
Proposition 5.6 — exactness of global sections on affine schemes
If X is affine and 0→F′→F→F″→0 is exact with F′ quasi-coherent, then 0→Γ(X,F′)→Γ(X,F)→Γ(X,F″)→0 is exact.
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 affine and 0→F′→F→F″→0 is exact with F′ quasi-coherent, then 0→Γ(X,F′)→Γ(X,F)→Γ(X,F″)→0 is exact. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, or a proper subset as the route for this ID.
Remark 5.6.1 — affine exactness and H¹
The preceding exactness is later recovered from H¹(X,F′)=0 for quasi-coherent F′ on affine 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 preceding exactness is later recovered from H¹(X,F′)=0 for quasi-coherent F′ on affine X. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, or a proper subset as the route for this ID.
Proposition 5.7 — closure properties of quasi-coherent/coherent sheaves
Kernels, cokernels, images, and extensions of quasi-coherent sheaves are quasi-coherent; on noetherian schemes the same holds for coherent sheaves.
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: Kernels, cokernels, images, and extensions of quasi-coherent sheaves are quasi-coherent; on noetherian schemes the same holds for coherent sheaves. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, or a proper subset as the route for this ID.
Proposition 5.8 — quasi-coherence under pullback and pushforward
Pullback preserves quasi-coherence and, for noetherian X,Y, coherence. Pushforward preserves quasi-coherence when X is noetherian or f is quasi-compact separated.
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: Pullback preserves quasi-coherence and, for noetherian X,Y, coherence. Pushforward preserves quasi-coherence when X is noetherian or f is quasi-compact separated. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, or a proper subset as the route for this ID.
Comparison 5.8.1 — pushforward need not preserve coherence
Pushforward of a coherent sheaf need not be coherent in general; it is coherent for finite or projective morphisms, and more generally for proper morphisms.
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: Pushforward of a coherent sheaf need not be coherent in general; it is coherent for finite or projective morphisms, and more generally for proper morphisms. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, or a proper subset as the route for this ID.
Definition — ideal sheaf of a closed subscheme
For closed immersion i:Y→X, I_Y is ker(O_X→i_*O_Y).
Formalized. Mathlib/AlgebraicGeometry/IdealSheaf/Basic.lean::Scheme.Hom.ker; Mathlib/AlgebraicGeometry/Morphisms/ClosedImmersion.lean::IsClosedImmersion.overEquivIdealSheafData — Pinned Mathlib realizes the complete source interface for this row: For closed immersion i:Y→X, I_Y is ker(O_X→i_*O_Y).
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d
Proposition 5.9 — quasi-coherent ideal sheaves classify closed subschemes
I_Y is quasi-coherent (coherent if X noetherian), and every quasi-coherent ideal sheaf on X determines a unique closed subscheme.
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: I_Y is quasi-coherent (coherent if X noetherian), and every quasi-coherent ideal sheaf on X determines a unique closed subscheme. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, or a proper subset as the route for this ID.
Corollary 5.10 — affine ideals classify closed subschemes
For X=Spec A, ideals a⊆A are in bijection with closed subschemes Spec(A/a)↪X; hence every closed subscheme of an affine scheme is affine.
Formalized. Mathlib/AlgebraicGeometry/IdealSheaf/Basic.lean::Scheme.IdealSheafData.equivOfIsAffine; Mathlib/AlgebraicGeometry/Morphisms/ClosedImmersion.lean::IsClosedImmersion.overEquivIdealSheafData — Pinned Mathlib realizes the complete source interface for this row: For X=Spec A, ideals a⊆A are in bijection with closed subschemes Spec(A/a)↪X; hence every closed subscheme of an affine scheme is affine.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d
Definition — sheaf associated to a graded module on Proj
For graded S-module M, M~ on Proj S has stalk M_(p), the degree-zero part of homogeneous localization, and sections locally represented by same-degree fractions.
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 graded S-module M, M~ on Proj S has stalk M_(p), the degree-zero part of homogeneous localization, and sections locally represented by same-degree fractions. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, or a proper subset as the route for this ID.
Proposition 5.11 — associated graded sheaf properties
For X=Proj S: (M~)p=M(p); on D_+(f), M~ is associated to M_(f); M~ is quasi-coherent, and coherent if S is noetherian and M finite.
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=Proj S: (M~)p=M(p); on D_+(f), M~ is associated to M_(f); M~ is quasi-coherent, and coherent if S is noetherian and M finite. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, or a proper subset as the route for this ID.
Definition — Serre twisting sheaf and twists
For X=Proj S define O_X(n)=S(n)~; O_X(1) is the twisting sheaf. For any O_X-module F, set F(n)=F⊗O_X(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: For X=Proj S define O_X(n)=S(n)~; O_X(1) is the twisting sheaf. For any O_X-module F, set F(n)=F⊗O_X(n). Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, or a proper subset as the route for this ID.
Proposition 5.12 — properties of twists on Proj
If S is generated by S_1 over S_0, O_X(n) is invertible, M(n)≅M(n), O(n)⊗O(m)≅O(n+m), and twists pull back compatibly under morphisms induced by graded maps.
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 S is generated by S_1 over S_0, O_X(n) is invertible, M(n)≅M(n), O(n)⊗O(m)≅O(n+m), and twists pull back compatibly under morphisms induced by graded maps. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, or a proper subset as the route for this ID.
Definition — graded module associated to a sheaf on Proj
For F on X=Proj S, Γ_*(F)=⊕_{n∈Z}Γ(X,F(n)), with its natural graded S-module structure.
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 F on X=Proj S, Γ_*(F)=⊕_{n∈Z}Γ(X,F(n)), with its natural graded S-module structure. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, or a proper subset as the route for this ID.
Proposition 5.13 — Γ(O) on projective space
For S=A[x_0,…,x_r], r≥1, X=Proj S, there is a natural graded isomorphism Γ_*(O_X)≅S.
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 S=A[x_0,…,x_r], r≥1, X=Proj S, there is a natural graded isomorphism Γ_*(O_X)≅S. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, or a proper subset as the route for this ID.
Comparison 5.13.1 — Γ(O) need not recover a general graded ring
For a general graded ring S, Γ_*(O_{Proj S}) need not equal S.
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 general graded ring S, Γ_*(O_{Proj S}) need not equal S. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, or a proper subset as the route for this ID.
Lemma 5.14 — killing and extending sections across Xf
For invertible L with section f and X_f where f is nonvanishing: on quasi-compact X, a global F-section vanishing on X_f is killed by some f^n; under a finite affine cover with quasi-compact overlaps, a section on X_f extends after multiplying by a power of 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: For invertible L with section f and X_f where f is nonvanishing: on quasi-compact X, a global F-section vanishing on X_f is killed by some f^n; under a finite affine cover with quasi-compact overlaps, a section on X_f extends after multiplying by a power of f. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, or a proper subset as the route for this ID.
Remark 5.14.1 — hypotheses for Lemma 5.14
The hypotheses of Lemma 5.14 hold if X is noetherian, or if X is quasi-compact and separated.
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 hypotheses of Lemma 5.14 hold if X is noetherian, or if X is quasi-compact and separated. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, or a proper subset as the route for this ID.
Proposition 5.15 — recovery from Γ
If S is finitely generated by S_1 over S_0 and X=Proj S, every quasi-coherent F has a natural isomorphism Γ_*(F)~≅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 S is finitely generated by S_1 over S_0 and X=Proj S, every quasi-coherent F has a natural isomorphism Γ_*(F)~≅F. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, or a proper subset as the route for this ID.
Corollary 5.16 — closed/projective schemes as Proj
Closed subschemes of P^r_A are defined by homogeneous ideals in A[x_0,…,x_r]; a scheme over Spec A is projective iff it is Proj S for a graded A-algebra S generated by S_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: Closed subschemes of P^r_A are defined by homogeneous ideals in A[x_0,…,x_r]; a scheme over Spec A is projective iff it is Proj S for a graded A-algebra S generated by S_1. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, or a proper subset as the route for this ID.
Definition — twisting sheaf on relative projective space
For any Y, O(1) on P^r_Y is the pullback of O(1) on P^r_Z; for Y=Spec A this agrees with the Proj definition.
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 Y, O(1) on P^r_Y is the pullback of O(1) on P^r_Z; for Y=Spec A this agrees with the Proj definition. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, or a proper subset as the route for this ID.
Definition — relatively very ample invertible sheaf and immersion
L on X/Y is very ample relative to Y if L≅i^*O(1) for an immersion i:X→P^r_Y; an immersion identifies X with an open subscheme of a closed subscheme.
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: L on X/Y is very ample relative to Y if L≅i^*O(1) for an immersion i:X→P^r_Y; an immersion identifies X with an open subscheme of a closed subscheme. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, or a proper subset as the route for this ID.
Remark 5.16.1 — projectivity via properness and a very ample sheaf
For noetherian Y, X/Y is projective iff it is proper and admits an invertible sheaf very ample relative to 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 noetherian Y, X/Y is projective iff it is proper and admits an invertible sheaf very ample relative to Y. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, or a proper subset as the route for this ID.
Definition — generated by global sections
F is generated by global sections when some family of global sections generates every stalk; equivalently F is a quotient of a free sheaf.
Formalized. Mathlib/Algebra/Category/ModuleCat/Sheaf/Generators.lean::SheafOfModules.GeneratingSections, SheafOfModules.GeneratingSections.π, SheafOfModules.freeHomEquiv — A pinned GeneratingSections object is a family of global sections whose associated map from a free sheaf is epi; this is exactly the source equivalence between stalkwise generation by global sections and being a quotient of a free sheaf.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d
Example 5.16.2 — quasi-coherent sheaves on affine schemes are globally generated
Every quasi-coherent sheaf on an affine scheme is generated by global sections.
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 quasi-coherent sheaf on an affine scheme is generated by global sections. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, or a proper subset as the route for this ID.
Example 5.16.3 — O(1) on degree-one Proj is globally generated
If S is generated by S_1, the degree-one elements give global sections generating O_{Proj S}(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 S is generated by S_1, the degree-one elements give global sections generating O_{Proj S}(1). Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, or a proper subset as the route for this ID.
Theorem 5.17 — Serre global-generation theorem
If X is projective over noetherian A, O(1) is very ample, and F coherent, then F(n) is generated by finitely many global sections for all n≫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 X is projective over noetherian A, O(1) is very ample, and F coherent, then F(n) is generated by finitely many global sections for all n≫0. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, or a proper subset as the route for this ID.
Corollary 5.18 — coherent sheaves are quotients of sums of twists
On a projective scheme over noetherian A, every coherent F is a quotient of a finite direct sum of O(n_i).
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 projective scheme over noetherian A, every coherent F is a quotient of a finite direct sum of O(n_i). Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, or a proper subset as the route for this ID.
Theorem 5.19 — finiteness of global sections
If k is a field, A a finitely generated k-algebra, X projective over A, and F coherent, then Γ(X,F) is a finite A-module; over A=k it is finite-dimensional.
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 k is a field, A a finitely generated k-algebra, X projective over A, and F coherent, then Γ(X,F) is a finite A-module; over A=k it is finite-dimensional. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, or a proper subset as the route for this ID.
Remark 5.19.1 — cohomological proof of finiteness
The finiteness theorem also admits a later proof by coherent cohomology.
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 finiteness theorem also admits a later proof by coherent cohomology. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, or a proper subset as the route for this ID.
Remark 5.19.2 — Nagata-ring weakening
In Theorem 5.19, “A finitely generated over k” can be weakened to A being a Nagata ring; this is the hypothesis needed for finiteness of integral closure.
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 Theorem 5.19, “A finitely generated over k” can be weakened to A being a Nagata ring; this is the hypothesis needed for finiteness of integral closure. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, or a proper subset as the route for this ID.
Corollary 5.20 — projective pushforward preserves coherence
If f:X→Y is projective between schemes finite type over a field and F is coherent on X, then f_*F is coherent on 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 f:X→Y is projective between schemes finite type over a field and F is coherent on X, then f_*F is coherent on Y. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, or a proper subset as the route for this ID.
Definition — regular in codimension one
A scheme X is regular (nonsingular) in codimension one when every local ring of dimension one is regular.
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 scheme X is regular (nonsingular) in codimension one when every local ring of dimension one is regular. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, or a proper subset as the route for this ID.
Convention — divisor standing hypothesis ()
Throughout the Weil-divisor discussion, (*) means X is noetherian, integral, separated, and regular in codimension 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: Throughout the Weil-divisor discussion, (*) means X is noetherian, integral, separated, and regular in codimension one. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, or a proper subset as the route for this ID.
Definition — prime, Weil, and effective divisors
Under (*), a prime divisor is a closed integral codimension-one subscheme; Div X is the free abelian group on prime divisors, and a divisor is effective when all coefficients are nonnegative.
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 (*), a prime divisor is a closed integral codimension-one subscheme; Div X is the free abelian group on prime divisors, and a divisor is effective when all coefficients are nonnegative. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, or a proper subset as the route for this ID.
Construction — valuation of a prime divisor
For a prime divisor Y with generic point η, O_{X,η} is a DVR with fraction field K(X); its valuation v_Y records zero/pole order of rational functions along 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 a prime divisor Y with generic point η, O_{X,η} is a DVR with fraction field K(X); its valuation v_Y records zero/pole order of rational functions along Y. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, or a proper subset as the route for this ID.
Lemma 6.1 — finite support of valuations
For nonzero f∈K(X), v_Y(f)=0 for all but finitely many prime divisors Y.
Not formalized. none; no complete checked declaration under strict bundle semantics — TauCeti proves finite support for orderAt indexed by its CodimensionOnePoint representation, but no checked formal bridge identifies those indices with Hartshorne prime divisors (closed integral codimension-one subschemes). Under the plan’s strict unbridged-representation rule this is evidence, not a route.
Definition — divisor of a rational function and principal divisors
For f∈K(X)^, define (f)=Σ_Y v_Y(f)Y; Lemma 6.1 makes the sum finite. Divisors of this form are principal, and f↦(f) is a homomorphism K(X)^→Div X.
Not formalized. none; no complete checked declaration under strict bundle semantics — TauCeti constructs principal divisors and the principal-divisor homomorphism for its codimension-one-point Weil-divisor representation, but the source Div X is the unbridged prime-divisor representation from U153; strict bundle semantics therefore forbid a route.
Definition — linear equivalence and divisor class group
D∼D′ when D−D′ is principal; Cl X=Div X/(principal divisors).
Not formalized. none; no complete checked declaration under strict bundle semantics — TauCeti defines linear equivalence and a class group for its codimension-one-point Weil-divisor representation, but no checked bridge identifies that divisor group with Hartshorne Div X; the equivalent-but-unbridged representation remains unmatched.
Proposition 6.2 — UFD criterion via class group
For a noetherian domain A, A is a UFD iff Spec A is normal and Cl(Spec A)=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 a noetherian domain A, A is a UFD iff Spec A is normal and Cl(Spec A)=0. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, or a proper subset as the route for this ID.
Proposition 6.3A — normal domain as intersection of height-one localizations
If A is an integrally closed noetherian domain with fraction field K, then A=∩_{ht p=1}A_p inside 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 A is an integrally closed noetherian domain with fraction field K, then A=∩_{ht p=1}A_p inside K. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, or a proper subset as the route for this ID.
Example 6.3.1 — class group of affine space
For affine n-space over a field, Cl A^n=0 because the polynomial ring is a UFD.
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 n-space over a field, Cl A^n=0 because the polynomial ring is a UFD. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, or a proper subset as the route for this ID.
Example 6.3.2 — Dedekind ideal class group
For a Dedekind domain A, Cl(Spec A) is its usual ideal class group.
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 Dedekind domain A, Cl(Spec A) is its usual ideal class group. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, or a proper subset as the route for this ID.
Proposition 6.4 — class group and degree on projective space
For X=P^n_k and hyperplane H: every divisor D of degree d is linearly equivalent to dH; principal divisors have degree zero; degree induces Cl X≅Z.
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^n_k and hyperplane H: every divisor D of degree d is linearly equivalent to dH; principal divisors have degree zero; degree induces Cl X≅Z. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, or a proper subset as the route for this ID.
Proposition 6.5 — class group under deleting a closed subset
If X satisfies (*) and U=Xfor proper closed Z, Cl X→Cl U is surjective; it is an isomorphism if codim(Z,X)≥2, and for irreducible codimension-one Z there is an exact sequence Z→Cl X→Cl U→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 X satisfies (*) and U=Xfor proper closed Z, Cl X→Cl U is surjective; it is an isomorphism if codim(Z,X)≥2, and for irreducible codimension-one Z there is an exact sequence Z→Cl X→Cl U→0. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, or a proper subset as the route for this ID.
Example 6.5.1 — class group of a plane-curve complement
If Y⊂P^2 is irreducible of degree d, then Cl(P^2)≅Z/dZ.
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⊂P^2 is irreducible of degree d, then Cl(P^2)≅Z/dZ. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, or a proper subset as the route for this ID.
Example 6.5.2 — class group of the affine quadric cone
For X=Spec k[x,y,z]/(xy−z²), Cl X≅Z/2Z, generated by a ruling of the cone.
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=Spec k[x,y,z]/(xy−z²), Cl X≅Z/2Z, generated by a ruling of the cone. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, or a proper subset as the route for this ID.
Proposition 6.6 — homotopy invariance of the class group
If X satisfies (), then X×A^1 also satisfies () and pullback gives Cl X≅Cl(X×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: If X satisfies (), then X×A^1 also satisfies () and pullback gives Cl X≅Cl(X×A^1). Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, or a proper subset as the route for this ID.
Example 6.6.1 — divisors on a smooth quadric surface
For Q≅P1×P1, Cl Q≅Z⊕Z via pullback from the two factors; a divisor class is said to have type (a,b).
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 Q≅P1×P1, Cl Q≅Z⊕Z via pullback from the two factors; a divisor class is said to have type (a,b). Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, or a proper subset as the route for this ID.
Example 6.6.2 — hyperplane class on a quadric
For Q⊂P^3 smooth, restriction Cl P^3→Cl Q sends a hyperplane to type (1,1); the two rulings have types (1,0) and (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 Q⊂P^3 smooth, restriction Cl P^3→Cl Q sends a hyperplane to type (1,1); the two rulings have types (1,0) and (0,1). Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, or a proper subset as the route for this ID.
Example 6.6.3 — twisted cubic on a quadric
A twisted cubic C on Q has divisor type (1,2); hence no surface in P^3 not containing Q can cut out C even set-theoretically, since degree-d hypersurface sections have type (d,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: A twisted cubic C on Q has divisor type (1,2); hence no surface in P^3 not containing Q can cut out C even set-theoretically, since degree-d hypersurface sections have type (d,d). Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, or a proper subset as the route for this ID.
Example 6.6.4 — cubic-surface class group preview
A later calculation gives the class group of a nonsingular cubic surface in P^3 as a free abelian group of rank seven.
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 later calculation gives the class group of a nonsingular cubic surface in P^3 as a free abelian group of rank seven. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, or a proper subset as the route for this ID.
Definition — curve, complete curve, nonsingular curve
Over algebraically closed k, a curve is an integral separated finite-type k-scheme of dimension one; it is complete if proper over k and nonsingular if all local rings are regular.
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, a curve is an integral separated finite-type k-scheme of dimension one; it is complete if proper over k and nonsingular if all local rings are regular. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, or a proper subset as the route for this ID.
Proposition 6.7 — complete/projective nonsingular curves
For a nonsingular curve X with function field K, the following are equivalent: X projective; X complete; X≅t(C_K), the scheme associated to Hartshorne’s abstract valuation 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 a nonsingular curve X with function field K, the following are equivalent: X projective; X complete; X≅t(C_K), the scheme associated to Hartshorne’s abstract valuation curve. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, or a proper subset as the route for this ID.
Proposition 6.8 — morphisms from complete nonsingular curves
For f:X→Y from a complete nonsingular curve to a curve, either f is constant or f(X)=Y; in the latter case K(X)/K(Y) is finite, f is finite, and Y is complete.
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 f:X→Y from a complete nonsingular curve to a curve, either f is constant or f(X)=Y; in the latter case K(X)/K(Y) is finite, f is finite, and Y is complete. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, or a proper subset as the route for this ID.
Definition — degree of a finite curve morphism and of a divisor
For finite f:X→Y of curves, deg f=[K(X):K(Y)]. On a nonsingular curve, divisors are finite sums Σn_iP_i of closed points and deg(Σn_iP_i)=Σn_i.
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 f:X→Y of curves, deg f=[K(X):K(Y)]. On a nonsingular curve, divisors are finite sums Σn_iP_i of closed points and deg(Σn_iP_i)=Σn_i. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, or a proper subset as the route for this ID.
Definition — pullback of divisors along finite curve maps
For finite f:X→Y between nonsingular curves, define f^*Q=Σ_{f(P)=Q}v_P(t)P for a local parameter t at Q; this is independent of t, extends linearly, and sends principal divisors to pullbacks of their 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: For finite f:X→Y between nonsingular curves, define f^*Q=Σ_{f(P)=Q}v_P(t)P for a local parameter t at Q; this is independent of t, extends linearly, and sends principal divisors to pullbacks of their functions. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, or a proper subset as the route for this ID.
Proposition 6.9 — degree under pullback
For finite f:X→Y of nonsingular curves and divisor D on Y, deg(f^*D)=(deg f)(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: For finite f:X→Y of nonsingular curves and divisor D on Y, deg(f^*D)=(deg f)(deg D). Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, or a proper subset as the route for this ID.
Corollary 6.10 — principal divisors have degree zero on complete curves
On a complete nonsingular curve, every principal divisor has degree zero; therefore degree descends to a surjective homomorphism Cl X→Z.
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 complete nonsingular curve, every principal divisor has degree zero; therefore degree descends to a surjective homomorphism Cl X→Z. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, or a proper subset as the route for this ID.
Example 6.10.1 — rationality via equivalent points
A complete nonsingular curve is rational iff it contains two distinct linearly equivalent 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: A complete nonsingular curve is rational iff it contains two distinct linearly equivalent points. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, or a proper subset as the route for this ID.
Example 6.10.2 — class group and group law on a nonsingular cubic
For a nonsingular plane cubic with chosen inflection P_0, P↦[P−P_0] identifies closed points with Cl^0 X=ker(deg), and the chord-tangent construction gives the induced algebraic group law.
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 nonsingular plane cubic with chosen inflection P_0, P↦[P−P_0] identifies closed points with Cl^0 X=ker(deg), and the chord-tangent construction gives the induced algebraic group law. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, or a proper subset as the route for this ID.
Remark 6.10.3 — Jacobian, Picard variety, and Néron–Severi preview
For a complete nonsingular curve, Cl^0 X is the group of closed points of its Jacobian; in higher dimensions algebraically trivial divisor classes form the Picard variety and the quotient is the finitely generated Néron–Severi group.
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 complete nonsingular curve, Cl^0 X is the group of closed points of its Jacobian; in higher dimensions algebraically trivial divisor classes form the Picard variety and the quotient is the finitely generated Néron–Severi group. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, or a proper subset as the route for this ID.
Definition — sheaf of total quotient rings
For a scheme X, localize affine coordinate rings at nonzerodivisors and sheafify to obtain the total quotient sheaf K; write K^* and O_X^* for its and the structure sheaf’s units.
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 scheme X, localize affine coordinate rings at nonzerodivisors and sheafify to obtain the total quotient sheaf K; write K^* and O_X^* for its and the structure sheaf’s units. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, or a proper subset as the route for this ID.
Definition — Cartier divisor, principal Cartier divisor, linear equivalence
A Cartier divisor is a global section of K^/O_X^, represented by local meromorphic units f_i whose ratios are regular units on overlaps; principal divisors come from Γ(X,K^*), and linear equivalence means difference principal.
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 Cartier divisor is a global section of K^/O_X^, represented by local meromorphic units f_i whose ratios are regular units on overlaps; principal divisors come from Γ(X,K^*), and linear equivalence means difference principal. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, or a proper subset as the route for this ID.
Proposition 6.11 — Weil and Cartier divisors on locally factorial schemes
If X is integral, separated, noetherian, and locally factorial, Weil divisors are canonically isomorphic to Cartier divisors, with principal divisors corresponding.
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 integral, separated, noetherian, and locally factorial, Weil divisors are canonically isomorphic to Cartier divisors, with principal divisors corresponding. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, or a proper subset as the route for this ID.
Remark 6.11.1A — regular schemes are locally factorial
Regular local rings are UFDs; hence Proposition 6.11 applies to regular integral separated noetherian schemes. A regular scheme has all local rings regular.
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 local rings are UFDs; hence Proposition 6.11 applies to regular integral separated noetherian schemes. A regular scheme has all local rings regular. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, or a proper subset as the route for this ID.
Remark 6.11.2 — Cartier divisors on normal schemes
On a normal scheme, Cartier divisors identify with the locally principal Weil divisors.
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 normal scheme, Cartier divisors identify with the locally principal Weil divisors. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, or a proper subset as the route for this ID.
Example 6.11.3 — Weil need not be Cartier
On the affine quadric cone, a ruling Y is a Weil divisor not locally principal, so not Cartier; 2Y is principal. Thus CaCl X=0 while Cl X≅Z/2Z.
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 the affine quadric cone, a ruling Y is a Weil divisor not locally principal, so not Cartier; 2Y is principal. Thus CaCl X=0 while Cl X≅Z/2Z. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, or a proper subset as the route for this ID.
Example 6.11.4 — Cartier class group of a cuspidal cubic
For the cuspidal cubic, Cartier divisor classes have a surjective degree map to Z whose kernel is identified with the nonsingular locus and, as a group variety, with the additive group G_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: For the cuspidal cubic, Cartier divisor classes have a surjective degree map to Z whose kernel is identified with the nonsingular locus and, as a group variety, with the additive group G_a. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, or a proper subset as the route for this ID.
Proposition 6.12 — tensor group law for invertible sheaves
The tensor product of invertible sheaves is invertible, and every invertible L has inverse L^{-1}=Hom(L,O_X) with L⊗L^{-1}≅O_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 tensor product of invertible sheaves is invertible, and every invertible L has inverse L^{-1}=Hom(L,O_X) with L⊗L^{-1}≅O_X. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, or a proper subset as the route for this ID.
Definition — Picard group
Pic X is the group of isomorphism classes of invertible sheaves under tensor product.
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: Pic X is the group of isomorphism classes of invertible sheaves under tensor product. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, or a proper subset as the route for this ID.
Remark 6.12.1 — Picard group as H¹ of units
Later Pic X is identified with H1(X,O_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: Later Pic X is identified with H1(X,O_X*). Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, or a proper subset as the route for this ID.
Definition — invertible sheaf associated to a Cartier divisor
If D is represented by local functions f_i, L(D) is the O_X-subsheaf of K locally generated by f_i^{-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 D is represented by local functions f_i, L(D) is the O_X-subsheaf of K locally generated by f_i^{-1}. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, or a proper subset as the route for this ID.
Proposition 6.13 — Cartier divisors and invertible subsheaves
L(D) is invertible; D↦L(D) bijects Cartier divisors with invertible subsheaves of K; L(D_1−D_2)≅L(D_1)⊗L(D_2)^{-1}; and D_1∼D_2 iff L(D_1)≅L(D_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: L(D) is invertible; D↦L(D) bijects Cartier divisors with invertible subsheaves of K; L(D_1−D_2)≅L(D_1)⊗L(D_2)^{-1}; and D_1∼D_2 iff L(D_1)≅L(D_2). Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, or a proper subset as the route for this ID.
Corollary 6.14 — Cartier classes inject into Pic
D↦L(D) induces an injective homomorphism CaCl X→Pic 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: D↦L(D) induces an injective homomorphism CaCl X→Pic X. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, or a proper subset as the route for this ID.
Remark 6.14.1 — CaCl→Pic need not be surjective
CaCl X→Pic X can fail to be surjective in general, though it is an isomorphism for projective schemes over a field and, as shown next, for integral schemes.
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: CaCl X→Pic X can fail to be surjective in general, though it is an isomorphism for projective schemes over a field and, as shown next, for integral schemes. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, or a proper subset as the route for this ID.
Proposition 6.15 — Cartier classes equal Pic on integral schemes
If X is integral, CaCl X→Pic X is an 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: If X is integral, CaCl X→Pic X is an isomorphism. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, or a proper subset as the route for this ID.
Corollary 6.16 — Weil classes equal Pic on locally factorial schemes
If X is noetherian, integral, separated, and locally factorial, then Cl X≅Pic 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 X is noetherian, integral, separated, and locally factorial, then Cl X≅Pic X. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, or a proper subset as the route for this ID.
Corollary 6.17 — Picard group of projective space
Every invertible sheaf on P^n_k is isomorphic to O(l) for a unique class l∈Z; Pic(P^n_k) is generated by O(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 invertible sheaf on P^n_k is isomorphic to O(l) for a unique class l∈Z; Pic(P^n_k) is generated by O(1). Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, or a proper subset as the route for this ID.
Definition — effective Cartier divisor and associated closed subscheme
A Cartier divisor is effective if represented by regular local functions f_i; these generate an ideal sheaf defining its associated codimension-one closed subscheme.
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 Cartier divisor is effective if represented by regular local functions f_i; these generate an ideal sheaf defining its associated codimension-one closed subscheme. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, or a proper subset as the route for this ID.
Remark 6.17.1 — effective Cartier divisors are locally principal subschemes
Effective Cartier divisors correspond bijectively to locally principal closed subschemes; on integral separated noetherian locally factorial schemes they coincide with effective Weil divisors.
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: Effective Cartier divisors correspond bijectively to locally principal closed subschemes; on integral separated noetherian locally factorial schemes they coincide with effective Weil divisors. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, or a proper subset as the route for this ID.
Proposition 6.18 — ideal sheaf of an effective Cartier divisor
If D is effective Cartier with associated closed subscheme Y, then I_Y≅L(−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 D is effective Cartier with associated closed subscheme Y, then I_Y≅L(−D). Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, or a proper subset as the route for this ID.
Theorem 7.1 — morphisms to projective space from generated line bundles
For X over A, an A-morphism φ:X→P^n_A pulls O(1) back to an invertible sheaf generated by φ^x_0,…,φ^x_n. Conversely, an invertible sheaf L with n+1 generating global sections determines a unique such morphism with L≅φ^*O(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 X over A, an A-morphism φ:X→P^n_A pulls O(1) back to an invertible sheaf generated by φ^x_0,…,φ^x_n. Conversely, an invertible sheaf L with n+1 generating global sections determines a unique such morphism with L≅φ^*O(1). Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, or a proper subset as the route for this ID.
Example 7.1.1 — projective linear automorphisms
An invertible (n+1)×(n+1) matrix over k induces an automorphism of P^n_k, and scalar multiples induce the same map; hence PGL(n,k)=GL(n+1,k)/k^* acts by projective automorphisms.
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 invertible (n+1)×(n+1) matrix over k induces an automorphism of P^n_k, and scalar multiples induce the same map; hence PGL(n,k)=GL(n+1,k)/k^* acts by projective automorphisms. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, or a proper subset as the route for this ID.
Example 7.1.2 — sections define a morphism on their generation locus
Arbitrary sections s_0,…,s_n of an invertible L define a morphism to P^n on the open locus where they generate L; for O(1) on P^{n+1} omitting one coordinate gives projection from the missing 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: Arbitrary sections s_0,…,s_n of an invertible L define a morphism to P^n on the open locus where they generate L; for O(1) on P^{n+1} omitting one coordinate gives projection from the missing point. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, or a proper subset as the route for this ID.
Proposition 7.2 — affine-chart criterion for a projective morphism to be a closed immersion
For φ:X→P^n_A determined by L and s_i, φ is a closed immersion iff every X_i={s_i≠0} is affine and each A[y_0,…,y_n]→Γ(X_i,O_X), y_j↦s_j/s_i, is surjective.
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^n_A determined by L and s_i, φ is a closed immersion iff every X_i={s_i≠0} is affine and each A[y_0,…,y_n]→Γ(X_i,O_X), y_j↦s_j/s_i, is surjective. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, or a proper subset as the route for this ID.
Proposition 7.3 — point/tangent separation criterion
If X is projective over algebraically closed k and V⊆Γ(X,L) is spanned by sections defining φ:X→P^n, then φ is a closed immersion iff V separates distinct closed points and separates tangent vectors at every closed 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: If X is projective over algebraically closed k and V⊆Γ(X,L) is spanned by sections defining φ:X→P^n, then φ is a closed immersion iff V separates distinct closed points and separates tangent vectors at every closed point. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, or a proper subset as the route for this ID.
Lemma 7.4 — local criterion for surjectivity of a finite algebra map
For a local map A→B of noetherian local rings inducing an isomorphism on residue fields, surjective on m_A/m_A²→m_B/m_B², and with B finite as an A-module, the map A→B is surjective.
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 local map A→B of noetherian local rings inducing an isomorphism on residue fields, surjective on m_A/m_A²→m_B/m_B², and with B finite as an A-module, the map A→B is surjective. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, or a proper subset as the route for this ID.
Definition — ample invertible sheaf
An invertible L on noetherian X is ample if for every coherent F there exists n_0 such that F⊗L^n is generated by global sections for all n≥n_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: An invertible L on noetherian X is ample if for every coherent F there exists n_0 such that F⊗L^n is generated by global sections for all n≥n_0. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, or a proper subset as the route for this ID.
Remark 7.4.1 — ample is absolute, very ample is relative
Ampleness depends only on X, while very ampleness is relative to a chosen morphism 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: Ampleness depends only on X, while very ampleness is relative to a chosen morphism X→Y. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, or a proper subset as the route for this ID.
Example 7.4.2 — every invertible sheaf on an affine scheme is ample
On an affine scheme every invertible sheaf is ample because every coherent sheaf is globally generated.
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 an affine scheme every invertible sheaf is ample because every coherent sheaf is globally generated. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, or a proper subset as the route for this ID.
Remark 7.4.3 — ample as stable very ampleness
Very ample implies ample on a projective scheme over a noetherian ring; conversely an ample invertible sheaf need not be very ample, but a positive tensor power is 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: Very ample implies ample on a projective scheme over a noetherian ring; conversely an ample invertible sheaf need not be very ample, but a positive tensor power is very ample. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, or a proper subset as the route for this ID.
Remark 7.4.4 — cohomological criterion for ampleness
A later criterion characterizes ampleness by vanishing of suitable higher cohomology groups after twisting.
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 later criterion characterizes ampleness by vanishing of suitable higher cohomology groups after twisting. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, or a proper subset as the route for this ID.
Proposition 7.5 — ampleness is invariant under positive powers
For an invertible L on noetherian X, the following are equivalent: L is ample; every L^m with m>0 is ample; some L^m with m>0 is 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: For an invertible L on noetherian X, the following are equivalent: L is ample; every L^m with m>0 is ample; some L^m with m>0 is ample. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, or a proper subset as the route for this ID.
Theorem 7.6 — ample iff some power is very ample
If X is finite type over a noetherian ring A, L is ample iff L^m is very ample over Spec A for some m>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 X is finite type over a noetherian ring A, L is ample iff L^m is very ample over Spec A for some m>0. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, or a proper subset as the route for this ID.
Example 7.6.1 — ample twists on projective space
On P^n_k, O(l) is ample iff it is very ample iff l>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 P^n_k, O(l) is ample iff it is very ample iff l>0. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, or a proper subset as the route for this ID.
Example 7.6.2 — ample line bundles on a smooth quadric
On Q≅P1×P1, an invertible sheaf of type (a,b) is ample exactly when a>0 and b>0; such positive types are very ample via product Veronese and Segre embeddings.
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 Q≅P1×P1, an invertible sheaf of type (a,b) is ample exactly when a>0 and b>0; such positive types are very ample via product Veronese and Segre embeddings. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, or a proper subset as the route for this ID.
Example 7.6.3 — ample need not be very ample
On the nonsingular cubic curve with inflection P_0, L(P_0) is ample because L(3P_0)≅O_X(1) is very ample, but L(P_0) itself is not globally generated and hence not 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: On the nonsingular cubic curve with inflection P_0, L(P_0) is ample because L(3P_0)≅O_X(1) is very ample, but L(P_0) itself is not globally generated and hence not very ample. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, or a proper subset as the route for this ID.
Example 7.6.4 — curve ampleness by degree
A later consequence of Riemann–Roch is that on a complete nonsingular curve L(D) is 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: A later consequence of Riemann–Roch is that on a complete nonsingular curve L(D) is ample iff deg D>0. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, or a proper subset as the route for this ID.
Proposition 7.7 — sections and effective divisors in a linear class
For nonsingular projective X and L≅L(D_0): every nonzero section s has an effective zero divisor (s)_0∼D_0; every effective divisor linearly equivalent to D_0 arises this way; two sections give the same zero divisor iff they differ by a scalar in 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: For nonsingular projective X and L≅L(D_0): every nonzero section s has an effective zero divisor (s)_0∼D_0; every effective divisor linearly equivalent to D_0 arises this way; two sections give the same zero divisor iff they differ by a scalar in k^*. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, or a proper subset as the route for this ID.
Definition — complete linear system
The complete linear system |D_0| is the set of effective divisors linearly equivalent to D_0; via Proposition 7.7 it is the projective space of nonzero sections of L(D_0) modulo 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: The complete linear system |D_0| is the set of effective divisors linearly equivalent to D_0; via Proposition 7.7 it is the projective space of nonzero sections of L(D_0) modulo k^*. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, or a proper subset as the route for this ID.
Definition — linear system and its dimension
A linear system is a projective linear subspace of a complete linear system, corresponding to a vector subspace V⊆Γ(X,L); its dimension is dim_k V−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 linear system is a projective linear subspace of a complete linear system, corresponding to a vector subspace V⊆Γ(X,L); its dimension is dim_k V−1. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, or a proper subset as the route for this ID.
Definition — base point of a linear system
P∈X is a base point of a linear system D when P lies in the support of every divisor in 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: P∈X is a base point of a linear system D when P lies in the support of every divisor in D. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, or a proper subset as the route for this ID.
Lemma 7.8 — base points and global generation
For D corresponding to V⊆Γ(X,L), P is a base point iff every s∈V has s_P∈m_PL_P; thus D is base-point-free iff V generates L.
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 D corresponding to V⊆Γ(X,L), P is a base point iff every s∈V has s_P∈m_PL_P; thus D is base-point-free iff V generates L. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, or a proper subset as the route for this ID.
Remark 7.8.1 — base-point-free linear systems define projective maps
A base-point-free linear system together with a basis of its section space determines a morphism X→P^n; changing basis changes it only by a projective automorphism.
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 base-point-free linear system together with a basis of its section space determines a morphism X→P^n; changing basis changes it only by a projective automorphism. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, or a proper subset as the route for this ID.
Remark 7.8.2 — embedding criterion for linear systems
The morphism determined by a base-point-free linear system is a closed immersion iff the system separates points and tangent vectors.
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 morphism determined by a base-point-free linear system is a closed immersion iff the system separates points and tangent vectors. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, or a proper subset as the route for this ID.
Definition — trace of a linear system on a subvariety
For closed immersion i:Y↪X of nonsingular projective varieties and a system determined by (L,V), its trace on Y is determined by (i^L, image(V→Γ(Y,i^L))); geometrically it is intersection with Y for divisors not containing 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 closed immersion i:Y↪X of nonsingular projective varieties and a system determined by (L,V), its trace on Y is determined by (i^L, image(V→Γ(Y,i^L))); geometrically it is intersection with Y for divisors not containing Y. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, or a proper subset as the route for this ID.
Example 7.8.3 — complete degree-d system on projective space
On P^n, all effective divisors of degree d>0 form the complete system |O(d)| of dimension binom(n+d,n)−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: On P^n, all effective divisors of degree d>0 form the complete system |O(d)| of dimension binom(n+d,n)−1. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, or a proper subset as the route for this ID.
Example 7.8.4 — projective normality via complete hypersurface systems
A nonsingular projective X⊂P^n is projectively normal iff for every d>0 the linear system on X cut out by degree-d hypersurfaces is complete.
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 projective X⊂P^n is projectively normal iff for every d>0 the linear system on X cut out by degree-d hypersurfaces is complete. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, or a proper subset as the route for this ID.
Example 7.8.5 — uniqueness of the twisted cubic up to projective automorphism
Every nonsingular degree-three nonplanar curve in P^3 abstractly isomorphic to P^1 is obtained from the standard twisted cubic by an automorphism of P^3, via the complete degree-three system on 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: Every nonsingular degree-three nonplanar curve in P^3 abstractly isomorphic to P^1 is obtained from the standard twisted cubic by an automorphism of P^3, via the complete degree-three system on P^1. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, or a proper subset as the route for this ID.
Example 7.8.6 — rational quartics need not be projectively equivalent
Degree-four rational curves in P^3 arise from four-dimensional subspaces of Γ(P^1,O(4)); different subspaces can yield smooth nonprojectively-equivalent quartics, with smooth embedding checked by point/tangent separation.
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: Degree-four rational curves in P^3 arise from four-dimensional subspaces of Γ(P^1,O(4)); different subspaces can yield smooth nonprojectively-equivalent quartics, with smooth embedding checked by point/tangent separation. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, or a proper subset as the route for this ID.
Convention — relative Proj hypothesis (+)
For relative Proj, X is noetherian and S=⊕_{d≥0}S_d is a quasi-coherent graded O_X-algebra with S_0=O_X, S_1 coherent, and S locally generated by S_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 relative Proj, X is noetherian and S=⊕_{d≥0}S_d is a quasi-coherent graded O_X-algebra with S_0=O_X, S_1 coherent, and S locally generated by S_1. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, or a proper subset as the route for this ID.
Construction — relative Proj and O(1)
For (X,S) satisfying (+), glue Proj Γ(U,S) over affine opens U⊆X to obtain Proj S with projection π:Proj S→X; the local twisting sheaves glue to an invertible O_{Proj S}(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 (X,S) satisfying (+), glue Proj Γ(U,S) over affine opens U⊆X to obtain Proj S with projection π:Proj S→X; the local twisting sheaves glue to an invertible O_{Proj S}(1). Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, or a proper subset as the route for this ID.
Example 7.8.7 — relative projective space as Proj
If S=O_X[T_0,…,T_n], then Proj S=P^n_X with its usual O(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 S=O_X[T_0,…,T_n], then Proj S=P^n_X with its usual O(1). Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, or a proper subset as the route for this ID.
Comparison 7.8.8 — relative O(1) need not be very ample
For a general relative Proj, O(1) need not be very ample relative 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: For a general relative Proj, O(1) need not be very ample relative to X. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, or a proper subset as the route for this ID.
Lemma 7.9 — twisting the graded algebra by a line bundle
For invertible L on X and S′d=S_d⊗L^d, Proj S′≅Proj S over X and O{Proj S′}(1)≅φ^O_{Proj S}(1)⊗π′^L.
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 invertible L on X and S′d=S_d⊗L^d, Proj S′≅Proj S over X and O{Proj S′}(1)≅φ^O_{Proj S}(1)⊗π′^L. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, or a proper subset as the route for this ID.
Proposition 7.10 — proper/projective relative Proj
For (X,S) satisfying (+), π:Proj S→X is proper. If X admits an ample L, then π is projective, and O(1)⊗π^*L^n is very ample relative to X for n≫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 (X,S) satisfying (+), π:Proj S→X is proper. If X admits an ample L, then π is projective, and O(1)⊗π^*L^n is very ample relative to X for n≫0. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, or a proper subset as the route for this ID.
Definition — projective space bundle P(E)
For noetherian X and locally free coherent E, define P(E)=Proj Sym(E); locally where E is free of rank n+1 it is P^n over the base, with projection π and O(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 noetherian X and locally free coherent E, define P(E)=Proj Sym(E); locally where E is free of rank n+1 it is P^n over the base, with projection π and O(1). Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, or a proper subset as the route for this ID.
Proposition 7.11 — section algebra and tautological quotient on P(E)
For rank E≥2, Sym(E)≅⊕*{l∈Z}π**O(l), with negative pieces zero, degree 0 equal O_X and degree 1 equal E; there is a natural surjection π^*E→O(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 rank E≥2, Sym(E)≅⊕*{l∈Z}π**O(l), with negative pieces zero, degree 0 equal O_X and degree 1 equal E; there is a natural surjection π^*E→O(1). Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, or a proper subset as the route for this ID.
Proposition 7.12 — universal property of P(E)
For g:Y→X, morphisms Y→P(E) over X are equivalent to pairs consisting of an invertible L on Y and a surjection g^*E→L.
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 g:Y→X, morphisms Y→P(E) over X are equivalent to pairs consisting of an invertible L on Y and a surjection g^*E→L. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, or a proper subset as the route for this ID.
Definition — blowing up a coherent ideal
For noetherian X and coherent ideal sheaf I, the blowup of X along the closed subscheme defined by I is X~=Proj(⊕_{d≥0}I^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: For noetherian X and coherent ideal sheaf I, the blowup of X along the closed subscheme defined by I is X~=Proj(⊕_{d≥0}I^d). Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, or a proper subset as the route for this ID.
Example 7.12.1 — relative-Proj blowup agrees with the affine-space construction
For X=A^n_k and the ideal of the origin, Proj(⊕I^d) is the earlier blowup in An×P{n−1}, cut out by x_i y_j=x_j y_i.
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=A^n_k and the ideal of the origin, Proj(⊕I^d) is the earlier blowup in An×P{n−1}, cut out by x_i y_j=x_j y_i. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, or a proper subset as the route for this ID.
Definition — inverse image ideal sheaf
For f:X→Y and ideal I⊆O_Y, the inverse image ideal f^{-1}I·O_X is the ideal generated in O_X by the image of f^{-1}I→O_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 f:X→Y and ideal I⊆O_Y, the inverse image ideal f^{-1}I·O_X is the ideal generated in O_X by the image of f^{-1}I→O_X. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, or a proper subset as the route for this ID.
Comparison 7.12.2 — inverse image ideal differs from module pullback
The module pullback f^I need not inject into O_X; the inverse image ideal f^{-1}I·O_X is the image of the natural map f^I→O_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 module pullback f^I need not inject into O_X; the inverse image ideal f^{-1}I·O_X is the image of the natural map f^I→O_X. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, or a proper subset as the route for this ID.
Proposition 7.13 — exceptional ideal and complement of the center
For blowup π:X~→X of coherent I, the inverse image ideal I=π^{-1}I·O_{X} is invertible, and π is an isomorphism over X minus the center.
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 blowup π:X~→X of coherent I, the inverse image ideal I=π^{-1}I·O_{X} is invertible, and π is an isomorphism over X minus the center. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, or a proper subset as the route for this ID.
Proposition 7.14 — universal property of blowing up
If f:Z→X is any morphism for which f^{-1}I·O_Z is an invertible ideal, then f factors uniquely through the blowup π:X~→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 f:Z→X is any morphism for which f^{-1}I·O_Z is an invertible ideal, then f factors uniquely through the blowup π:X~→X. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, or a proper subset as the route for this ID.
Corollary 7.15 — functoriality of blowup under inverse-image ideals
For f:Y→X and coherent I on X, blowing up X along I and Y along f^{-1}I·O_Y yields a unique lifted map Y→X; if f is a closed immersion, so is the lift.
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 f:Y→X and coherent I on X, blowing up X along I and Y along f^{-1}I·O_Y yields a unique lifted map Y→X; if f is a closed immersion, so is the lift. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, or a proper subset as the route for this ID.
Definition — strict transform
If Y↪X is closed, its blowup along the inverse image of the center is the strict transform Y⊆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 Y↪X is closed, its blowup along the inverse image of the center is the strict transform Y⊆X. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, or a proper subset as the route for this ID.
Example 7.15.1 — strict transform as closure off the center
For Y⊆A^n through the blown-up origin P, the strict transform is the closure of π^{-1}(Y{P}); this recovers the Chapter-I construction and proves that construction intrinsic.
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⊆A^n through the blown-up origin P, the strict transform is the closure of π^{-1}(Y{P}); this recovers the Chapter-I construction and proves that construction intrinsic. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, or a proper subset as the route for this ID.
Proposition 7.16 — blowups of varieties
For a variety X and nonzero coherent ideal I, X~ is a variety; π is birational, proper, and surjective; quasi-projectivity/projectivity of X is preserved, and π is projective.
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 variety X and nonzero coherent ideal I, X~ is a variety; π is birational, proper, and surjective; quasi-projectivity/projectivity of X is preserved, and π is projective. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, or a proper subset as the route for this ID.
Theorem 7.17 — projective birational morphisms are blowups
If X is a quasi-projective variety and f:Z→X is birational and projective, then f is isomorphic over X to the blowup of X along some coherent ideal sheaf.
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 a quasi-projective variety and f:Z→X is birational and projective, then f is isomorphic over X to the blowup of X along some coherent ideal sheaf. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, or a proper subset as the route for this ID.
Remark 7.17.1 — blowup ideal is not unique
The coherent ideal realizing a given projective birational morphism as a blowup need not be unique.
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 coherent ideal realizing a given projective birational morphism as a blowup need not be unique. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, or a proper subset as the route for this ID.
Remark 7.17.2 — restricted centers in geometric applications
Although arbitrary coherent ideals give all projective birational morphisms as blowups, important applications often restrict to geometrically controlled centers, such as nonsingular centers in resolution or points on surfaces.
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: Although arbitrary coherent ideals give all projective birational morphisms as blowups, important applications often restrict to geometrically controlled centers, such as nonsingular centers in resolution or points on surfaces. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, or a proper subset as the route for this ID.
Example 7.17.3 — eliminating indeterminacy by blowing up the base ideal
Given sections s_0,…,s_n of an invertible L on noetherian X, their generation locus carries a rational map to P^n; blowing up the coherent image ideal generated by the sections makes the pulled-back sections base-point-free and extends the map to the blowup.
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: Given sections s_0,…,s_n of an invertible L on noetherian X, their generation locus carries a rational map to P^n; blowing up the coherent image ideal generated by the sections makes the pulled-back sections base-point-free and extends the map to the blowup. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, or a proper subset as the route for this ID.
Definition — A-derivation
For an A-algebra B and B-module M, an A-derivation d:B→M is additive, satisfies Leibniz d(bb′)=b d(b′)+b′ d(b), and vanishes on A.
Formalized. Mathlib/RingTheory/Derivation/Basic.lean::Derivation — Pinned Mathlib realizes the complete source interface for this row: For an A-algebra B and B-module M, an A-derivation d:B→M is additive, satisfies Leibniz d(bb′)=b d(b′)+b′ d(b), and vanishes on A.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d
Definition — module of Kähler differentials
Ω_{B/A} with d:B→Ω_{B/A} represents A-derivations: every A-derivation B→M factors uniquely through a B-linear map Ω_{B/A}→M.
Formalized. Mathlib/RingTheory/Kaehler/Basic.lean::KaehlerDifferential, KaehlerDifferential.D, Derivation.liftKaehlerDifferential, KaehlerDifferential.linearMapEquivDerivation — Pinned Mathlib realizes the complete source interface for this row: Ω_{B/A} with d:B→Ω_{B/A} represents A-derivations: every A-derivation B→M factors uniquely through a B-linear map Ω_{B/A}→M.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d
Proposition 8.1A — diagonal construction of Kähler differentials
For I=ker(B⊗A B→B), the B-module I/I² with d(b)=1⊗b−b⊗1 is a module of relative differentials Ω{B/A}.
Formalized. Mathlib/RingTheory/Kaehler/Basic.lean::KaehlerDifferential.ideal, KaehlerDifferential.quotientCotangentIdealRingEquiv, KaehlerDifferential.quotientCotangentIdeal — Pinned Mathlib realizes the complete source interface for this row: For I=ker(B⊗A B→B), the B-module I/I² with d(b)=1⊗b−b⊗1 is a module of relative differentials Ω{B/A}.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d
Proposition 8.2A — base change and localization for differentials
For B′=B⊗A A′, Ω{B′/A′}≅Ω_{B/A}⊗B B′; for multiplicative S⊆B, Ω{S{-1}B/A}≅S{-1}Ω_{B/A}.
Formalized. Mathlib/RingTheory/Kaehler/TensorProduct.lean::KaehlerDifferential.tensorKaehlerEquivBase, KaehlerDifferential.tensorKaehlerEquiv, KaehlerDifferential.isLocalizedModule — Pinned Mathlib realizes the complete source interface for this row: For B′=B⊗A A′, Ω{B′/A′}≅Ω_{B/A}⊗B B′; for multiplicative S⊆B, Ω{S{-1}B/A}≅S{-1}Ω_{B/A}.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d
Example 8.2.1 — differentials of a polynomial algebra
For B=A[x_1,…,x_n], Ω_{B/A} is free of rank n with basis dx_1,…,dx_n.
Formalized. Mathlib/RingTheory/Kaehler/Polynomial.lean::KaehlerDifferential.mvPolynomialBasis — Pinned Mathlib realizes the complete source interface for this row: For B=A[x_1,…,x_n], Ω_{B/A} is free of rank n with basis dx_1,…,dx_n.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d
Proposition 8.3A — first exact sequence of differentials
For ring maps A→B→C there is a natural exact sequence Ω_{B/A}⊗B C→Ω{C/A}→Ω_{C/B}→0.
Formalized. Mathlib/RingTheory/Kaehler/Basic.lean::KaehlerDifferential.mapBaseChange, KaehlerDifferential.exact_mapBaseChange_map — Pinned Mathlib realizes the complete source interface for this row: For ring maps A→B→C there is a natural exact sequence Ω_{B/A}⊗B C→Ω{C/A}→Ω_{C/B}→0.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d
Proposition 8.4A — conormal exact sequence for rings
For B an A-algebra, ideal I, and C=B/I, there is a natural exact sequence I/I²→Ω_{B/A}⊗B C→Ω{C/A}→0, with a mod I mapping to da⊗1.
Formalized. Mathlib/RingTheory/Kaehler/Basic.lean::KaehlerDifferential.kerCotangentToTensor, KaehlerDifferential.exact_kerCotangentToTensor_mapBaseChange — Pinned Mathlib realizes the complete source interface for this row: For B an A-algebra, ideal I, and C=B/I, there is a natural exact sequence I/I²→Ω_{B/A}⊗B C→Ω{C/A}→0, with a mod I mapping to da⊗1.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d
Corollary 8.5 — finite generation of differentials
If B is finitely generated over A or a localization of a finitely generated A-algebra, then Ω_{B/A} is a finitely generated B-module.
Formalized. Mathlib/RingTheory/Kaehler/Basic.lean::KaehlerDifferential.finite — Pinned Mathlib realizes the complete source interface for this row: If B is finitely generated over A or a localization of a finitely generated A-algebra, then Ω_{B/A} is a finitely generated B-module.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d
Theorem 8.6A — field differentials and separable generation
For finitely generated K/k, dim_K Ω_{K/k}≥trdeg_k K, with equality iff K/k is separably generated.
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 finitely generated K/k, dim_K Ω_{K/k}≥trdeg_k K, with equality iff K/k is separably generated. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, or a proper subset as the route for this ID.
Proposition 8.7 — cotangent space as fibre of differentials
If local B contains a field k identified with B/m, then the natural map m/m²→Ω_{B/k}⊗_B k is an 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: If local B contains a field k identified with B/m, then the natural map m/m²→Ω_{B/k}⊗_B k is an isomorphism. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, or a proper subset as the route for this ID.
Theorem 8.8 — regular local rings via differentials
If B is a localization of a finite-type algebra over a perfect field k equal to its residue field, then Ω_{B/k} is free of rank dim B iff B is regular local.
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 B is a localization of a finite-type algebra over a perfect field k equal to its residue field, then Ω_{B/k} is free of rank dim B iff B is regular local. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, or a proper subset as the route for this ID.
Lemma 8.9 — equal fibre and generic ranks imply freeness
For a noetherian local domain A with residue field k and fraction field K, if finite M has dim_k(M⊗k)=dim_K(M⊗K)=r, then M is free of rank 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 a noetherian local domain A with residue field k and fraction field K, if finite M has dim_k(M⊗k)=dim_K(M⊗K)=r, then M is free of rank r. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, or a proper subset as the route for this ID.
Definition — sheaf of relative differentials
For f:X→Y, take the diagonal Δ:X→X×Y X, its locally closed image inside a suitable open W with ideal I, and define Ω{X/Y}=Δ^*(I/I²).
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 f:X→Y, take the diagonal Δ:X→X×Y X, its locally closed image inside a suitable open W with ideal I, and define Ω{X/Y}=Δ^*(I/I²). Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, or a proper subset as the route for this ID.
Remark 8.9.1 — quasi-coherence/coherence of Ω
Ω_{X/Y} is a quasi-coherent O_X-module; if Y is noetherian and f finite type, then it is coherent.
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/Y} is a quasi-coherent O_X-module; if Y is noetherian and f finite type, then it is coherent. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, or a proper subset as the route for this ID.
Remark 8.9.2 — affine compatibility and universal differential
On affines V=Spec B→U=Spec A, Ω_{V/U}≅(Ω_{B/A})~. The affine derivations glue to d:O_X→Ω_{X/Y}, so the sheaf definition can equivalently be made by gluing affine modules of differentials.
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 affines V=Spec B→U=Spec A, Ω_{V/U}≅(Ω_{B/A})~. The affine derivations glue to d:O_X→Ω_{X/Y}, so the sheaf definition can equivalently be made by gluing affine modules of differentials. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, or a proper subset as the route for this ID.
Proposition 8.10 — base change for sheaves of differentials
For base change X′=X×Y Y′ with projection g′:X′→X, Ω{X′/Y′}≅g′*Ω_{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: For base change X′=X×Y Y′ with projection g′:X′→X, Ω{X′/Y′}≅g′*Ω_{X/Y}. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, or a proper subset as the route for this ID.
Proposition 8.11 — transitivity exact sequence
For X→Y→Z there is a natural exact sequence f^*Ω_{Y/Z}→Ω_{X/Z}→Ω_{X/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 X→Y→Z there is a natural exact sequence f^*Ω_{Y/Z}→Ω_{X/Z}→Ω_{X/Y}→0. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, or a proper subset as the route for this ID.
Proposition 8.12 — conormal exact sequence
For Z↪X closed with ideal I and X→Y, there is a natural exact sequence I/I²→Ω_{X/Y}⊗O_Z→Ω_{Z/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 Z↪X closed with ideal I and X→Y, there is a natural exact sequence I/I²→Ω_{X/Y}⊗O_Z→Ω_{Z/Y}→0. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, or a proper subset as the route for this ID.
Example 8.12.1 — differentials of relative affine space
For X=A^n_Y, Ω_{X/Y} is free of rank n generated by global dx_1,…,dx_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: For X=A^n_Y, Ω_{X/Y} is free of rank n generated by global dx_1,…,dx_n. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, or a proper subset as the route for this ID.
Theorem 8.13 — Euler sequence on projective space
For X=P^n_A over Y=Spec A there is an exact sequence 0→Ω_{X/Y}→O_X(−1)^{⊕(n+1)}→O_X→0, the last map induced by the homogeneous 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: For X=P^n_A over Y=Spec A there is an exact sequence 0→Ω_{X/Y}→O_X(−1)^{⊕(n+1)}→O_X→0, the last map induced by the homogeneous coordinates. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, or a proper subset as the route for this ID.
Definition — nonsingular abstract variety
An abstract variety over algebraically closed k is nonsingular when all its local rings are regular local rings.
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 variety over algebraically closed k is nonsingular when all its local rings are regular local rings. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, or a proper subset as the route for this ID.
Theorem 8.14A — regularity localizes
Any localization of a regular local ring at a prime ideal is again a regular local 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: Any localization of a regular local ring at a prime ideal is again a regular local ring. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, or a proper subset as the route for this ID.
Theorem 8.15 — nonsingularity via locally free differentials
For irreducible separated finite-type X over algebraically closed k, Ω_{X/k} is locally free of rank dim X iff X is a nonsingular 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: For irreducible separated finite-type X over algebraically closed k, Ω_{X/k} is locally free of rank dim X iff X is a nonsingular variety. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, or a proper subset as the route for this ID.
Corollary 8.16 — nonsingular locus contains a dense open
Every variety over k has a dense open subset that is nonsingular.
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 variety over k has a dense open subset that is nonsingular. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, or a proper subset as the route for this ID.
Theorem 8.17 — conormal criterion for a nonsingular subvariety
For irreducible closed Y⊂X with X nonsingular, Y is nonsingular iff Ω_{Y/k} is locally free and 0→I/I²→Ω_{X/k}⊗O_Y→Ω_{Y/k}→0 is exact; then I is locally generated by codim(Y,X) elements and I/I² is locally free of that rank.
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 irreducible closed Y⊂X with X nonsingular, Y is nonsingular iff Ω_{Y/k} is locally free and 0→I/I²→Ω_{X/k}⊗O_Y→Ω_{Y/k}→0 is exact; then I is locally generated by codim(Y,X) elements and I/I² is locally free of that rank. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, or a proper subset as the route for this ID.
Theorem 8.18 — Bertini hyperplane theorem
If X⊂P^n_k is nonsingular closed over algebraically closed k, there is a hyperplane H not containing X for which H∩X is regular everywhere; such hyperplanes form a dense open subset of the complete hyperplane system.
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_k is nonsingular closed over algebraically closed k, there is a hyperplane H not containing X for which H∩X is regular everywhere; such hyperplanes form a dense open subset of the complete hyperplane system. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, or a proper subset as the route for this ID.
Remark 8.18.1 — Bertini with finitely many singular points
The Bertini conclusion remains valid when X has only finitely many singular points, by avoiding the proper closed sets of hyperplanes through them.
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 Bertini conclusion remains valid when X has only finitely many singular points, by avoiding the proper closed sets of hyperplanes through them. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, or a proper subset as the route for this ID.
Definition — tangent sheaf, canonical sheaf, geometric genus
For nonsingular n-fold X, T_X=Hom(Ω_{X/k},O_X), ω_X=∧^nΩ_{X/k}; if X is projective, p_g(X)=dim_k Γ(X,ω_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 nonsingular n-fold X, T_X=Hom(Ω_{X/k},O_X), ω_X=∧^nΩ_{X/k}; if X is projective, p_g(X)=dim_k Γ(X,ω_X). Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, or a proper subset as the route for this ID.
Remark 8.18.2 — arithmetic versus geometric genus
For smooth projective curves arithmetic and geometric genus coincide; in dimension ≥2 they need 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: For smooth projective curves arithmetic and geometric genus coincide; in dimension ≥2 they need not. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, or a proper subset as the route for this ID.
Remark 8.18.3 — geometric genus as intrinsic and birational data
Differentials, tangent and canonical sheaves are intrinsic isomorphism invariants; the next theorem strengthens p_g to a birational invariant for nonsingular projective 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: Differentials, tangent and canonical sheaves are intrinsic isomorphism invariants; the next theorem strengthens p_g to a birational invariant for nonsingular projective varieties. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, or a proper subset as the route for this ID.
Theorem 8.19 — birational invariance of geometric genus
Birationally equivalent nonsingular projective varieties over k have the same geometric genus.
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: Birationally equivalent nonsingular projective varieties over k have the same geometric genus. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, or a proper subset as the route for this ID.
Definition — conormal and normal sheaves
For nonsingular Y⊂X with ideal I, I/I² is the conormal sheaf and N_{Y/X}=Hom(I/I²,O_Y) its normal sheaf, locally free of rank codim(Y,X); dualizing the conormal sequence gives 0→T_Y→T_X|Y→N{Y/X}→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 nonsingular Y⊂X with ideal I, I/I² is the conormal sheaf and N_{Y/X}=Hom(I/I²,O_Y) its normal sheaf, locally free of rank codim(Y,X); dualizing the conormal sequence gives 0→T_Y→T_X|Y→N{Y/X}→0. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, or a proper subset as the route for this ID.
Proposition 8.20 — adjunction formula
For nonsingular codimension-r Y⊂X, ω_Y≅ω_X|Y⊗∧^r N{Y/X}; for r=1 with associated divisor sheaf L, ω_Y≅ω_X⊗L⊗O_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 nonsingular codimension-r Y⊂X, ω_Y≅ω_X|Y⊗∧^r N{Y/X}; for r=1 with associated divisor sheaf L, ω_Y≅ω_X⊗L⊗O_Y. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, or a proper subset as the route for this ID.
Example 8.20.1 — canonical sheaf of projective space
Dualizing the Euler sequence yields the tangent sequence; taking determinants gives ω_{P^n}=O(−n−1), hence p_g(P^n)=0 and every nonsingular projective rational variety has p_g=0 by birational invariance.
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: Dualizing the Euler sequence yields the tangent sequence; taking determinants gives ω_{P^n}=O(−n−1), hence p_g(P^n)=0 and every nonsingular projective rational variety has p_g=0 by birational invariance. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, or a proper subset as the route for this ID.
Example 8.20.2 — existence of smooth hypersurfaces
For every d≥1 and n≥2, smooth degree-d hypersurfaces in P^n exist and form a dense open subset of the complete system |dH|.
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 d≥1 and n≥2, smooth degree-d hypersurfaces in P^n exist and form a dense open subset of the complete system |dH|. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, or a proper subset as the route for this ID.
Example 8.20.3 — canonical sheaf of a smooth hypersurface
For a smooth degree-d hypersurface Y⊂P^n, adjunction gives ω_Y≅O_Y(d−n−1), yielding the usual genus/canonical calculations in low dimensions.
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 smooth degree-d hypersurface Y⊂P^n, adjunction gives ω_Y≅O_Y(d−n−1), yielding the usual genus/canonical calculations in low dimensions. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, or a proper subset as the route for this ID.
Theorem 8.21A — Cohen–Macaulay and regular-sequence facts
For local noetherian A: regular implies Cohen–Macaulay; CM localizes; in a CM ring x_1,…,x_r is regular iff quotient dimension drops by r; quotient by a regular sequence is CM; and for I=(x_i), gr_I A≅(A/I)[t_1,…,t_r], so I/I² is free and Symn(I/I²)≅In/I^{n+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 local noetherian A: regular implies Cohen–Macaulay; CM localizes; in a CM ring x_1,…,x_r is regular iff quotient dimension drops by r; quotient by a regular sequence is CM; and for I=(x_i), gr_I A≅(A/I)[t_1,…,t_r], so I/I² is free and Symn(I/I²)≅In/I^{n+1}. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, or a proper subset as the route for this ID.
Theorem 8.22A — Serre criterion for normality
A noetherian ring is normal iff it satisfies R_1 (localizations at primes of height ≤1 are regular) and S_2 (depth at primes of height ≥2 is at least 2, with the height-one consequence).
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 noetherian ring is normal iff it satisfies R_1 (localizations at primes of height ≤1 are regular) and S_2 (depth at primes of height ≥2 is at least 2, with the height-one consequence). Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, or a proper subset as the route for this ID.
Definition — local complete intersection
A closed subscheme Y of a nonsingular variety X is a local complete intersection in X if its ideal sheaf is locally generated by r=codim(Y,X) 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 closed subscheme Y of a nonsingular variety X is a local complete intersection in X if its ideal sheaf is locally generated by r=codim(Y,X) elements. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, or a proper subset as the route for this ID.
Example 8.22.1 — nonsingular subvarieties are local complete intersections
A nonsingular subvariety Y inside a nonsingular X is a local complete intersection.
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 subvariety Y inside a nonsingular X is a local complete intersection. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, or a proper subset as the route for this ID.
Remark 8.22.2 — lci is intrinsic
The local-complete-intersection property is intrinsic to Y, independent of the chosen embedding into a nonsingular ambient variety; Hartshorne notes this is proved using the cotangent complex.
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 local-complete-intersection property is intrinsic to Y, independent of the chosen embedding into a nonsingular ambient variety; Hartshorne notes this is proved using the cotangent complex. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, or a proper subset as the route for this ID.
Proposition 8.23 — local complete intersections are Cohen–Macaulay
If Y is lci in a nonsingular variety, then Y is Cohen–Macaulay; moreover Y is normal iff it is regular in codimension 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: If Y is lci in a nonsingular variety, then Y is Cohen–Macaulay; moreover Y is normal iff it is regular in codimension one. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, or a proper subset as the route for this ID.
Theorem 8.24 — blowup along a nonsingular center
If X and closed Y⊂X are nonsingular and X~ is the blowup of I_Y, then X~ is nonsingular; the exceptional divisor Y′≅P(I/I²) over Y; under this identification its normal sheaf is O_{P(I/I²)}(−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 X and closed Y⊂X are nonsingular and X~ is the blowup of I_Y, then X~ is nonsingular; the exceptional divisor Y′≅P(I/I²) over Y; under this identification its normal sheaf is O_{P(I/I²)}(−1). Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, or a proper subset as the route for this ID.
Theorem 8.25A — Cohen field of representatives
If complete local A contains k and its residue field is separably generated over k, then A contains a subfield K⊇k mapping isomorphically onto the residue field; K is a field of representatives.
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 complete local A contains k and its residue field is separably generated over k, then A contains a subfield K⊇k mapping isomorphically onto the residue field; K is a field of representatives. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, or a proper subset as the route for this ID.
Definition/construction — inverse systems and inverse limits of abelian groups
An inverse system (A_n,φ_{n′n}) has compatible transition maps for n′≥n; lim←A_n consists of compatible sequences and is characterized by the universal property for compatible maps into all A_n.
Formalized. Mathlib/Algebra/Category/Grp/Limits.lean; Mathlib/CategoryTheory/Limits/Types/Limits.lean::Types.limitEquivSections; Mathlib/CategoryTheory/Limits/HasLimits.lean::limit, limit.π, limit.isLimit — Pinned Mathlib realizes the complete source interface for this row: An inverse system (A_n,φ_{n′n}) has compatible transition maps for n′≥n; lim←A_n consists of compatible sequences and is characterized by the universal property for compatible maps into all A_n.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d
Construction/comparison — morphisms, exact systems, and left exactness of inverse limit
Morphisms of inverse systems are levelwise maps commuting with transitions; exactness is levelwise. Applying inverse limit to a short exact sequence is always left exact, but the final map need not be surjective.
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 of inverse systems are levelwise maps commuting with transitions; exactness is levelwise. Applying inverse limit to a short exact sequence is always left exact, but the final map need not be surjective. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, or a proper subset as the route for this ID.
Definition — Mittag–Leffler condition
An inverse system satisfies (ML) when for each n the decreasing family of images im(A_{n′}→A_n) stabilizes for n′≫n.
Formalized. Mathlib/CategoryTheory/CofilteredSystem.lean::Functor.IsMittagLeffler — Pinned Mathlib realizes the complete source interface for this row: An inverse system satisfies (ML) when for each n the decreasing family of images im(A_{n′}→A_n) stabilizes for n′≫n.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d
Construction — stable-image inverse system
For an ML system, replacing each A_n by its stable image gives an inverse system with surjective transition maps and the same inverse limit; lim←A_n maps onto each stable image.
Formalized. Mathlib/CategoryTheory/CofilteredSystem.lean::Functor.toEventualRanges, Functor.toEventualRangesSectionsEquiv, Functor.surjective_toEventualRanges, Functor.eval_section_surjective_of_surjective — Pinned Mathlib realizes the complete source interface for this row: For an ML system, replacing each A_n by its stable image gives an inverse system with surjective transition maps and the same inverse limit; lim←A_n maps onto each stable image.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d
Proposition 9.1 — Mittag–Leffler exactness criterion
For a short exact sequence 0→(A_n)→(B_n)→(C_n)→0: if (B_n) is ML then (C_n) is ML; if (A_n) is ML, then 0→lim A_n→lim B_n→lim C_n→0 is exact.
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 short exact sequence 0→(A_n)→(B_n)→(C_n)→0: if (B_n) is ML then (C_n) is ML; if (A_n) is ML, then 0→lim A_n→lim B_n→lim C_n→0 is exact. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, or a proper subset as the route for this ID.
Example 9.1.1 — surjective systems are Mittag–Leffler
If all transition maps are surjective, the inverse system satisfies the ML condition.
Formalized. Mathlib/CategoryTheory/CofilteredSystem.lean::Functor.isMittagLeffler_of_surjective — Pinned Mathlib realizes the complete source interface for this row: If all transition maps are surjective, the inverse system satisfies the ML condition.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d
Example 9.1.2 — finite-dimensional/DCC systems are Mittag–Leffler
Inverse systems of finite-dimensional vector spaces, more generally modules satisfying descending chain condition, satisfy ML.
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: Inverse systems of finite-dimensional vector spaces, more generally modules satisfying descending chain condition, satisfy ML. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, or a proper subset as the route for this ID.
Definition/construction — inverse limit in an arbitrary category
For an inverse system in a category C, lim←A_n is an object with compatible projections universal for compatible cones; when it exists it is unique up to unique isomorphism.
Formalized. Mathlib/CategoryTheory/Limits/HasLimits.lean::limit, limit.π, limit.isLimit — Pinned Mathlib realizes the complete source interface for this row: For an inverse system in a category C, lim←A_n is an object with compatible projections universal for compatible cones; when it exists it is unique up to unique isomorphism.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d
Proposition 9.2 — inverse limits of sheaves
Inverse limits exist for sheaves of abelian groups on X, and sections commute with them: Γ(U,lim←F_n)=lim←Γ(U,F_n) for every open U.
Formalized. Mathlib/Topology/Sheaves/Limits.lean; Mathlib/CategoryTheory/Limits/FunctorCategory/Basic.lean::limitObjIsoLimitCompEvaluation — Pinned Mathlib constructs limits in sheaf categories via the underlying presheaf limits, while functor-category evaluation commutes with limits; evaluation on an open set is therefore the inverse limit of the section groups, exactly Hartshorne’s statement.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d
Caution 9.2.1 — inverse-limit exactness differs for sheaves
The ML surjectivity conclusion of Proposition 9.1(b) can fail inside the category of sheaves even for surjective transition maps; exactness arguments therefore pass to sections.
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 ML surjectivity conclusion of Proposition 9.1(b) can fail inside the category of sheaves even for surjective transition maps; exactness arguments therefore pass to sections. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, or a proper subset as the route for this ID.
Definition — I-adic completion of a ring
For ideal I⊆A, the inverse system A/I^n has completion Â=lim←A/I^n with its canonical homomorphism A→Â.
Formalized. Mathlib/RingTheory/AdicCompletion/Basic.lean::AdicCompletion; Mathlib/RingTheory/AdicCompletion/Algebra.lean::AdicCompletion.algebraMap_apply — Pinned Mathlib realizes the complete source interface for this row: For ideal I⊆A, the inverse system A/I^n has completion Â=lim←A/I^n with its canonical homomorphism A→Â.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d
Definition — I-adic completion of a module
For A-module M, M=lim←M/InM, naturally an Â-module.
Formalized. Mathlib/RingTheory/AdicCompletion/Basic.lean::AdicCompletion, AdicCompletion.of; Mathlib/RingTheory/AdicCompletion/Algebra.lean::AdicCompletion.module — Pinned Mathlib realizes the complete source interface for this row: For A-module M, M=lim←M/InM, naturally an Â-module.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d
Theorem 9.3A — algebra of I-adic completion
For noetherian A: Î is an ideal of  with În=In and Â/În≅A/In; finite M satisfies M^≅M⊗_AÂ; completion is exact on finite modules;  is noetherian; compatible surjective finite A/I^n-modules arise from a finite Â-module by inverse limit.
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 noetherian A: Î is an ideal of  with În=In and Â/În≅A/In; finite M satisfies M^≅M⊗_AÂ; completion is exact on finite modules;  is noetherian; compatible surjective finite A/I^n-modules arise from a finite Â-module by inverse limit. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, or a proper subset as the route for this ID.
Definition — formal completion of a scheme along a closed subscheme
For noetherian X and closed Y defined by I, the formal completion X^ has underlying topological space Y and structure sheaf O_{X}=lim←O_X/In.
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 noetherian X and closed Y defined by I, the formal completion X^ has underlying topological space Y and structure sheaf O_{X}=lim←O_X/In. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, or a proper subset as the route for this ID.
Remark 9.3.1 — formal completion depends only on the closed support
O_{X^} depends only on the closed subset Y, not its chosen closed-subscheme structure, because ideals defining the same closed support have cofinal powers; on affine U=Spec A its sections are the I-adic completion of 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: O_{X^} depends only on the closed subset Y, not its chosen closed-subscheme structure, because ideals defining the same closed support have cofinal powers; on affine U=Spec A its sections are the I-adic completion of A. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, or a proper subset as the route for this ID.
Definition — completion of a coherent sheaf
For coherent F on X and Y defined by I, define F=lim←F/InF on Y; it is naturally an O_{X^}-module.
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 coherent F on X and Y defined by I, define F=lim←F/InF on Y; it is naturally an O_{X^}-module. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, or a proper subset as the route for this ID.
Definition — noetherian formal scheme, morphism, coherent sheaf
A noetherian formal scheme is a locally ringed space with a finite open cover by completions of noetherian schemes along closed subschemes; morphisms are locally-ringed-space morphisms, and coherent modules are locally completions of coherent modules on such algebraizations.
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 noetherian formal scheme is a locally ringed space with a finite open cover by completions of noetherian schemes along closed subschemes; morphisms are locally-ringed-space morphisms, and coherent modules are locally completions of coherent modules on such algebraizations. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, or a proper subset as the route for this ID.
Examples 9.3.2 — algebraizable and nonalgebraizable formal schemes
A completion of one noetherian scheme along one closed subscheme is algebraizable; nonalgebraizable noetherian formal schemes also exist.
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 completion of one noetherian scheme along one closed subscheme is algebraizable; nonalgebraizable noetherian formal schemes also exist. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, or a proper subset as the route for this ID.
Example 9.3.3 — schemes as formal schemes
Completing a noetherian scheme X along Y=X gives X itself, so noetherian schemes form a subcategory of noetherian formal schemes.
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: Completing a noetherian scheme X along Y=X gives X itself, so noetherian schemes form a subcategory of noetherian formal schemes. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, or a proper subset as the route for this ID.
Example 9.3.4 — completion at a closed point
Completing noetherian X at a closed point P gives a one-point formal scheme with structure ring the completed local ring O^_{X,P}; its coherent sheaves are exactly finite modules over that 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: Completing noetherian X at a closed point P gives a one-point formal scheme with structure ring the completed local ring O^_{X,P}; its coherent sheaves are exactly finite modules over that ring. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, or a proper subset as the route for this ID.
Definition — affine formal scheme and M^Δ
An affine formal scheme is the completion of an affine noetherian scheme Spec A along V(I); for finite A-module M, M^Δ is the completion of M~ and is coherent.
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 formal scheme is the completion of an affine noetherian scheme Spec A along V(I); for finite A-module M, M^Δ is the completion of M~ and is coherent. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, or a proper subset as the route for this ID.
Proposition 9.4 — basic affine formal-scheme module properties
For X^ the completion of Spec A along V(I): I^Δ is an ideal with O_{X}/(IΔ)n≅(A/In)~; MΔ≅M~⊗{O_X}O{X}; and M↦M^Δ is exact on finite A-modules.
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^ the completion of Spec A along V(I): I^Δ is an ideal with O_{X}/(IΔ)n≅(A/In)~; MΔ≅M~⊗{O_X}O{X}; and M↦M^Δ is exact on finite A-modules. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, or a proper subset as the route for this ID.
Definition — ideal of definition
An ideal sheaf J⊆O_𝔛 on a noetherian formal scheme is an ideal of definition if Supp(O_𝔛/J)=𝔛 and (𝔛,O_𝔛/J) is a noetherian scheme.
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 ideal sheaf J⊆O_𝔛 on a noetherian formal scheme is an ideal of definition if Supp(O_𝔛/J)=𝔛 and (𝔛,O_𝔛/J) is a noetherian scheme. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, or a proper subset as the route for this ID.
Proposition 9.5 — properties of ideals of definition
Any two ideals of definition contain powers of one another; there is a unique largest ideal of definition, whose quotient scheme is reduced; and every positive power of an ideal of definition is again 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: Any two ideals of definition contain powers of one another; there is a unique largest ideal of definition, whose quotient scheme is reduced; and every positive power of an ideal of definition is again one. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, or a proper subset as the route for this ID.
Proposition 9.6 — coherent formal sheaves as compatible infinitesimal layers
For ideal of definition J and Y_n=(𝔛,O_𝔛/J^n), a coherent F gives coherent F_n=F/J^nF with F≅lim←F_n; conversely a compatible surjective system of coherent F_n with the expected kernels has coherent inverse limit and recovers each F_n by quotient.
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 ideal of definition J and Y_n=(𝔛,O_𝔛/J^n), a coherent F gives coherent F_n=F/J^nF with F≅lim←F_n; conversely a compatible surjective system of coherent F_n with the expected kernels has coherent inverse limit and recovers each F_n by quotient. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, or a proper subset as the route for this ID.
Theorem 9.7 — affine formal schemes and finite modules
If noetherian A is I-adically complete and 𝔛 is the completion of Spec A along V(I), M↦M^Δ and Γ(𝔛,−) are exact inverse equivalences between finite A-modules and coherent O_𝔛-modules.
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 noetherian A is I-adically complete and 𝔛 is the completion of Spec A along V(I), M↦M^Δ and Γ(𝔛,−) are exact inverse equivalences between finite A-modules and coherent O_𝔛-modules. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, or a proper subset as the route for this ID.
Corollary 9.8 — exactness and tensor description of sheaf completion
For completion X^ of noetherian X along Y, F↦F^ is exact on coherent sheaves; F/(I)nF≅F/I^nF and F^ is obtained by tensoring with O_{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 completion X^ of noetherian X along Y, F↦F^ is exact on coherent sheaves; F/(I)nF≅F/I^nF and F^ is obtained by tensoring with O_{X^}. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, or a proper subset as the route for this ID.
Corollary 9.9 — kernels, cokernels, and images remain coherent
On a noetherian formal scheme, kernels, cokernels, and images of morphisms of coherent sheaves are coherent.
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 noetherian formal scheme, kernels, cokernels, and images of morphisms of coherent sheaves are coherent. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, or a proper subset as the route for this ID.
Remark 9.9.1 — extensions and failure of global generation on formal schemes
Extensions of coherent formal-scheme sheaves are coherent, but scheme-theoretic generation properties can fail: a nonzero coherent sheaf on a projective completion may have no global sections after any twist.
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: Extensions of coherent formal-scheme sheaves are coherent, but scheme-theoretic generation properties can fail: a nonzero coherent sheaf on a projective completion may have no global sections after any twist. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, or a proper subset as the route for this ID.