Hartshorne, Algebraic Geometry — Chapter III: Cohomology
FC06 — Hartshorne, Algebraic Geometry.
This chapter contains 25 definitions, 21 theorems, 42 propositions, 16 lemmas, 23 corollaries, 33 examples, 9 constructions, 33 remarks and 2 other statements.
Of the 204 statements checked against Lean, 23 are formalized somewhere and 181 are not.
| Status | Statements | Share | What it means |
|---|---|---|---|
| not formalized | 181 | 89% | A documented search found no Lean statement of it anywhere. |
| in Mathlib | 21 | 10% | Mathlib states and proves it. |
| in another Lean project | 2 | 1% | Some other Lean development has it; using it means porting that code. |
| checked in total | 204 |
- Canonical source block: FC06 Hartshorne, Chapter III,
FC06-C03-U001–FC06-C03-U204, in canonical source-ID order. C01–C02 were already promoted and were not modified. - Project-first inspection is recorded against
A=cd74b69e97f743cd7318a9fe130ed2a749860b3f; repository HEAD3b2239e161592472b34e02ad3b7da308f9ce7280changes onlyTODO.md. Pinned Mathlib isP=db584cd6d46c92f209a44c0f1c829460d327499d, Lean 4.33.0, Apache-2.0. Current Mathlib was refreshed atH=5aedf732b6987e8c26ab3c9ebc855314f82b045f, Lean 4.34.0-rc2. - The pre-existing project source atlas and Hartshorne definition catalogue were reused before new discovery. Targeted P/H exact-declaration checks then resolved derived functors, sheaf cohomology, Čech complexes, flatness, projective dimension and semicontinuity. Open Mathlib PR and indexed GitHub searches were run for Serre duality, higher direct images, formal functions, semicontinuity/cohomology base change, Stein factorization, generic smoothness and Bertini; no additional complete route was verified.
- Strict bundle semantics govern every row. A route must own the complete source statement; partial clauses, analogous interfaces, stronger hypotheses, and declarations whose proof is
sorryare not promoted. - Clawristotle
coherent-cohomology-finiteatC=09497ebf6ee48ef49c4f3d24501954bc3a2855d6is Apache-2.0, Lean 4.32.0-rc1, Mathlib360da6fa66c1273b76b6b2d8c5666fd5ac2e3b56and therefore reference-only relative to P. Its axiom-cleanAcyclicResolution.leanexactly supplies U015 (Functor.IsRightAcyclic) and U016 (rightDerivedIsoOfAcyclicResolution), which are recorded asreference-port. - The recorded Atlas files
AffinePushforwardHigher.leanandAffinePushforwardCohomology.leanat local Atlas revision34ffed396f376454c1a9b297f3fd74c5c801fb50contain matching affine-pushforward statements but their substantive theorems useby sorry; they are statement-bank evidence only and are not mapping routes. Their noncommercial/no-training license would in any case require separate handling before any port. - Pinned Mathlib contains generic sheaf cohomology and a Čech-complex construction, but not the affine/projective coherent-cohomology comparison and finiteness theorems required by Hartshorne III.2–III.5. It contains global Ext/projective-dimension infrastructure, but not the internal sheaf-Ext/Serre-duality programme. The regular-sequence source explicitly lists Koszul regular sequences as TODO, so U095–U096 remain unmatched.
- Flatness primitives U119/U121/U122/U123 have direct pinned owners. Smooth/étale infrastructure exists, but it is not credited to Hartshorne’s differently bundled smoothness definition or the major geometric generic-smoothness/Bertini assertions without checked equivalence theorems.
- No checked P/H/open/external implementation was found for Hartshorne’s formal-functions theorem, coherent higher-direct-image finiteness, semicontinuity theorem for proper families, cohomology-and-base-change theorem, or Stein factorization. Generic
UpperSemicontinuousand its closed-superlevel characterization do exactly own U195–U196. N=2026-09-06marks a dated unmatched decision after project-first, P, H/current, recorded open/current work, indexed search services and relevant external Lean checks.
Definition — abelian category
An abelian category has abelian Hom groups with bilinear composition, finite direct sums, kernels/cokernels, every mono/epi is normal, and every morphism factors as an epi followed by a mono.
Formalized. Mathlib/CategoryTheory/Abelian/Basic.lean::CategoryTheory.Abelian — Pinned Mathlib realizes the complete source interface: An abelian category has abelian Hom groups with bilinear composition, finite direct sums, kernels/cokernels, every mono/epi is normal, and every morphism factors as an epi followed by a mono.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d
Example 1.0.1 — abelian groups
The category Ab of abelian groups is abelian.
Formalized. Mathlib/Algebra/Category/Grp/Abelian.lean::AddCommGrpCat.instAbelian — Pinned Mathlib realizes the complete source interface: The category Ab of abelian groups is abelian.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d
Example 1.0.2 — modules
For a ring A, Mod(A) is an abelian category.
Formalized. Mathlib/Algebra/Category/ModuleCat/Abelian.lean::ModuleCat.abelian — Pinned Mathlib realizes the complete source interface: For a ring A, Mod(A) is an abelian category.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d
Example 1.0.3 — sheaves of abelian groups
For a topological space X, Ab(X), the category of sheaves of abelian groups, is abelian.
Formalized. Mathlib/Topology/Sheaves/Abelian.lean::CategoryTheory.Sheaf.instIsGrothendieckAbelian — Pinned Mathlib makes sheaves valued in a Grothendieck abelian category Grothendieck abelian, hence abelian; specializing to abelian groups is exactly Hartshorne’s example.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d
Example 1.0.4 — sheaves of modules
For a ringed space X, Mod(X), the category of O_X-modules, is abelian.
Formalized. Mathlib/Algebra/Category/ModuleCat/Sheaf/Abelian.lean::SheafOfModules.instAbelian — Pinned Mathlib realizes the complete source interface: For a ringed space X, Mod(X), the category of O_X-modules, is abelian.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d
Example 1.0.5 — quasi-coherent sheaves
For a scheme X, quasi-coherent O_X-modules form an abelian category.
Not formalized. none; no complete checked declaration under strict bundle semantics — Quasi-coherent sheaves are formalized, but no checked pinned instance makes their full subcategory abelian as Hartshorne states.
Example 1.0.6 — coherent sheaves
On a noetherian scheme, coherent O_X-modules form an abelian category.
Not formalized. none; no complete checked declaration under strict bundle semantics — Coherent sheaves are formalized only partially at the checked pin; no abelian coherent-sheaf category on noetherian schemes was found.
Example 1.0.7 — coherent sheaves on noetherian formal schemes
Coherent modules on a noetherian formal scheme form an abelian category.
Not formalized. none; no complete checked declaration under strict bundle semantics — No noetherian formal-scheme layer exists at the checked pin, so this abelian-category example is unmatched.
Definition/construction — complexes, cohomology objects, homotopies
A complex A^• has d²=0; hi(A•)=ker d^i/im d^{i−1}. Morphisms induce cohomology maps, short exact sequences of complexes induce long exact cohomology sequences, and homotopic maps induce the same maps on cohomology.
Not formalized. none; no complete checked declaration under strict bundle semantics — Mathlib has complexes, homology objects, homotopies and long exact homology machinery, but this source row bundles all constructions and comparison theorems; the audit did not isolate one complete stable interface for every clause.
Definition — additive, left/right exact, exact functors
An additive functor preserves addition on Hom groups; left/right exactness means preservation of the corresponding half of every short exact sequence, and exact means both. Contravariant left exactness reverses the short sequence.
Formalized. Mathlib/CategoryTheory/Preadditive/AdditiveFunctor.lean::Functor.Additive; Mathlib/CategoryTheory/Limits/ExactFunctor.lean::LeftExactFunctor, RightExactFunctor, ExactFunctor — Pinned Mathlib realizes the complete source interface: An additive functor preserves addition on Hom groups; left/right exactness means preservation of the corresponding half of every short exact sequence, and exact means both. Contravariant left exactness reverses the short sequence.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d
Example 1.0.8 — Hom functors are left exact
For fixed A in an abelian category, Hom(A,−) is covariant left exact and Hom(−,A) is contravariant left 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 fixed A in an abelian category, Hom(A,−) is covariant left exact and Hom(−,A) is contravariant left exact. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, an incomplete proof, or a proper subset as the route for this ID.
Definition/construction — injectives, enough injectives, injective resolutions
I is injective when Hom(−,I) is exact. An injective resolution 0→A→I0→I1→… has all I^i injective. If the category has enough injectives, every object admits such a resolution, unique up to homotopy equivalence.
Formalized. Mathlib/CategoryTheory/Preadditive/Injective/Basic.lean::CategoryTheory.Injective, EnoughInjectives; Mathlib/CategoryTheory/Abelian/Injective/Resolution.lean::InjectiveResolution, InjectiveResolution.homotopyEquiv — Pinned Mathlib realizes the complete source interface: I is injective when Hom(−,I) is exact. An injective resolution 0→A→I0→I1→… has all I^i injective. If the category has enough injectives, every object admits such a resolution, unique up to homotopy equivalence.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d
Definition/construction — right derived functors
For left exact F on an abelian category with enough injectives, choose an injective resolution I^• of A and define RiF(A)=hi(F(I^•)).
Formalized. Mathlib/CategoryTheory/Abelian/RightDerived.lean::Functor.rightDerived, InjectiveResolution.isoRightDerivedObj — Pinned Mathlib realizes the complete source interface: For left exact F on an abelian category with enough injectives, choose an injective resolution I^• of A and define RiF(A)=hi(F(I^•)).
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d
Theorem 1.1A — basic properties of right derived functors
R^iF are well-defined additive functors independent up to natural isomorphism of resolutions; R^0F≅F; short exact sequences yield natural long exact sequences; morphisms of short exact sequences give compatible connecting morphisms.
Not formalized. none; no complete checked declaration under strict bundle semantics — Pinned right-derived functors include resolution-independence and degree-zero comparison infrastructure, but the audit did not verify the entire bundled long-exact-sequence/naturality theorem as one route.
Definition — F-acyclic object
An object J is acyclic for F if R^iF(J)=0 for all i>0.
Formalized. coherent-cohomology-finite/CoherentCohomologyFinite/AcyclicResolution.lean::CategoryTheory.Functor.IsRightAcyclic — Clawristotle at C realizes the complete source interface: An object J is acyclic for F if R^iF(J)=0 for all i>0.
Searched: C=09497ebf6ee48ef49c4f3d24501954bc3a2855d6; repo=Vilin97/Clawristotle; subproject=coherent-cohomology-finite; license=Apache-2.0; toolchain=Lean 4.32.0-rc1; mathlib=360da6fa66c1273b76b6b2d8c5666fd5ac2e3b56; compatibility=reference-only against P=db584cd6d46c92f209a44c0f1c829460d327499d
Proposition 1.2A — computing derived functors from acyclic resolutions
If 0→A→J0→J1→… is an F-acyclic resolution, then RiF(A)≅hi(F(J^•)) for all i≥0.
Formalized. coherent-cohomology-finite/CoherentCohomologyFinite/AcyclicResolution.lean::CategoryTheory.Functor.rightDerivedIsoOfAcyclicResolution — Clawristotle at C realizes the complete source interface: If 0→A→J0→J1→… is an F-acyclic resolution, then RiF(A)≅hi(F(J^•)) for all i≥0.
Searched: C=09497ebf6ee48ef49c4f3d24501954bc3a2855d6; repo=Vilin97/Clawristotle; subproject=coherent-cohomology-finite; license=Apache-2.0; toolchain=Lean 4.32.0-rc1; mathlib=360da6fa66c1273b76b6b2d8c5666fd5ac2e3b56; compatibility=reference-only against P=db584cd6d46c92f209a44c0f1c829460d327499d
Definition — δ-functor
A covariant δ-functor T=(T^i) consists of functors with natural connecting maps for short exact sequences, producing functorial long exact sequences.
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked P/H declaration packages Hartshorne’s δ-functor structure and functorial long exact sequences under this interface.
Definition — universal δ-functor
A δ-functor T is universal if any morphism T0→T′0 extends uniquely to a morphism of δ-functors T→T′.
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked P/H universal δ-functor interface was found.
Remark 1.2.1 — uniqueness of universal δ-functors
For fixed additive F there is at most one universal δ-functor with T^0=F up to unique isomorphism; its higher terms are the right satellite functors.
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked P/H satellite/universal-δ uniqueness theorem was found.
Definition — effaceable and coeffaceable functors
An additive F is effaceable if every object A embeds into some M with F(A→M)=0; coeffaceable dually uses an epimorphism P→A killed by F.
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked P/H effaceable/coeffaceable functor definition matching Hartshorne was found.
Theorem 1.3A — effaceable δ-functors are universal
If T is a covariant δ-functor and every T^i for i>0 is effaceable, then T is universal.
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked P/H theorem states that an effaceable δ-functor is universal.
Corollary 1.4 — derived functors are the universal δ-functor
With enough injectives, (R^iF) is the universal δ-functor extending left exact F. Conversely every universal δ-functor is naturally isomorphic to the derived functors of its degree-zero term.
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked P/H theorem packages right derived functors as the universal δ-functor with the converse uniqueness assertion.
Proposition 2.1A — enough injective modules
Every module over any ring embeds in an injective module.
Formalized. Mathlib/Algebra/Category/ModuleCat/EnoughInjectives.lean::ModuleCat.enoughInjectives — Pinned Mathlib realizes the complete source interface: Every module over any ring embeds in an injective module.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d
Proposition 2.2 — sheaves of modules have enough injectives
For any ringed space X, Mod(X) has enough injectives.
Not formalized. none; no complete checked declaration under strict bundle semantics — The module-sheaf category is abelian, but no checked enough-injectives instance for arbitrary sheaves of modules on a ringed space was found.
Corollary 2.3 — abelian sheaves have enough injectives
For any topological space X, Ab(X) has enough injectives.
Formalized. Mathlib/Topology/Sheaves/Abelian.lean::CategoryTheory.Sheaf.instIsGrothendieckAbelian; Mathlib/CategoryTheory/Abelian/GrothendieckCategory/EnoughInjectives.lean::enoughInjectives — Pinned Mathlib realizes the complete source interface: For any topological space X, Ab(X) has enough injectives.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d
Definition — sheaf cohomology
For a topological space X, H^i(X,−) is the ith right derived functor of Γ(X,−) on abelian sheaves. All scheme/sheaf cohomology is taken in this underlying abelian-sheaf sense.
Formalized. Mathlib/CategoryTheory/Sites/SheafCohomology/Basic.lean::CategoryTheory.Sheaf.H, cohomologyPresheafFunctor, H.equiv₀ — Pinned Mathlib realizes the complete source interface: For a topological space X, H^i(X,−) is the ith right derived functor of Γ(X,−) on abelian sheaves. All scheme/sheaf cohomology is taken in this underlying abelian-sheaf sense.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d
Definition — flasque sheaf
A sheaf F is flasque if every restriction F(U)→F(V) for V⊆U is surjective.
Formalized. Mathlib/Topology/Sheaves/Flasque.lean::TopCat.Sheaf.IsFlasque — Pinned Mathlib realizes the complete source interface: A sheaf F is flasque if every restriction F(U)→F(V) for V⊆U is surjective.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d
Lemma 2.4 — injective module sheaves are flasque
Every injective O_X-module on a ringed space is flasque.
Not formalized. none; no complete checked declaration under strict bundle semantics — Flasque and injective sheaves are separately formalized, but no checked theorem states injective module sheaves are flasque.
Proposition 2.5 — flasque sheaves are acyclic for global sections
If F is flasque, then H^i(X,F)=0 for all i>0.
Not formalized. none; no complete checked declaration under strict bundle semantics — The flasque API does not contain the sheaf-cohomology acyclicity theorem at the pin.
Remark 2.5.1 — cohomology from flasque resolutions
Flasque sheaves are Γ-acyclic, so sheaf cohomology may be computed using flasque resolutions.
Not formalized. none; no complete checked declaration under strict bundle semantics — Without flasque acyclicity, the complete flasque-resolution computation theorem is absent.
Proposition 2.6 — module-derived global sections equal sheaf cohomology
For a ringed space, the derived functors of Γ(X,−) on O_X-modules coincide with H^i(X,−) defined in abelian 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 a ringed space, the derived functors of Γ(X,−) on O_X-modules coincide with H^i(X,−) defined in abelian sheaves. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, an incomplete proof, or a proper subset as the route for this ID.
Remark 2.6.1 — module structure on cohomology
If A=Γ(X,O_X), then H^i(X,F) for an O_X-module F is naturally an A-module and all long exact sequences are A-linear; for X over Spec B they are B-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 A=Γ(X,O_X), then H^i(X,F) for an O_X-module F is naturally an A-module and all long exact sequences are A-linear; for X over Spec B they are B-modules. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, an incomplete proof, or a proper subset as the route for this ID.
Theorem 2.7 — Grothendieck vanishing
If X is a noetherian topological space of dimension n, then H^i(X,F)=0 for every abelian sheaf F and every i>n.
Not formalized. none; no complete checked declaration under strict bundle semantics — As of 2026-09-06, no checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: If X is a noetherian topological space of dimension n, then H^i(X,F)=0 for every abelian sheaf F and every i>n. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, an incomplete proof, or a proper subset as the route for this ID.
Lemma 2.8 — direct limits of flasque sheaves
On a noetherian topological space, a direct limit of flasque sheaves is flasque.
Not formalized. none; no complete checked declaration 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 topological space, a direct limit of flasque sheaves is flasque. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, an incomplete proof, or a proper subset as the route for this ID.
Proposition 2.9 — cohomology commutes with direct limits
On a noetherian topological space, Hi(X,lim→F_α)≅lim→Hi(X,F_α) naturally for every i≥0.
Not formalized. none; no complete checked declaration under strict bundle semantics — As of 2026-09-06, no checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: On a noetherian topological space, Hi(X,lim→F_α)≅lim→Hi(X,F_α) naturally for every i≥0. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, an incomplete proof, or a proper subset as the route for this ID.
Remark 2.9.1 — cohomology commutes with arbitrary direct sums
As a special case of direct-limit compatibility, sheaf cohomology commutes with infinite direct sums.
Not formalized. none; no complete checked declaration under strict bundle semantics — As of 2026-09-06, no checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: As a special case of direct-limit compatibility, sheaf cohomology commutes with infinite direct sums. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, an incomplete proof, or a proper subset as the route for this ID.
Lemma 2.10 — cohomology under extension by zero from a closed subset
For closed j:Y↪X and abelian sheaf F on Y, Hi(Y,F)≅Hi(X,j_*F) for all 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 closed j:Y↪X and abelian sheaf F on Y, Hi(Y,F)≅Hi(X,j_*F) for all i. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, an incomplete proof, or a proper subset as the route for this ID.
Remark 2.10.1 — suppressing closed extension by zero
Hartshorne often writes F for j_*F when a sheaf on a closed subset is regarded on X; Lemma 2.10 makes its cohomology unambiguous.
Not formalized. none; no complete checked declaration under strict bundle semantics — As of 2026-09-06, no checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: Hartshorne often writes F for j_*F when a sheaf on a closed subset is regarded on X; Lemma 2.10 makes its cohomology unambiguous. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, an incomplete proof, or a proper subset as the route for this ID.
Proposition 3.1A — Krull topology theorem
For noetherian A, finite M⊆N, and ideal a, the a-adic topology on M is induced from N: for each n there is n′≥n with anM⊇M∩a{n′}N.
Not formalized. none; no complete checked declaration under strict bundle semantics — The recorded searches found no formalization of Hartshorne’s Krull topology theorem.
Construction — Γa(M)
For ideal a⊆A and A-module M, Γ_a(M)={m∈M : a^n m=0 for some n>0}.
Not formalized. none; no complete checked declaration under strict bundle semantics — Pinned local-cohomology infrastructure defines higher local cohomology as a colimit of Ext, but does not directly own Hartshorne’s section-torsion functor row as bundled here.
Lemma 3.2 — torsion submodule of an injective is injective
If A is noetherian, a⊆A, and I is injective, then Γ_a(I) is injective.
Not formalized. none; no complete checked declaration 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 noetherian, a⊆A, and I is injective, then Γ_a(I) is injective. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, an incomplete proof, or a proper subset as the route for this ID.
Lemma 3.3 — localization of an injective module is a quotient
For injective I over noetherian A and f∈A, the natural map I→I_f 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 injective I over noetherian A and f∈A, the natural map I→I_f is surjective. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, an incomplete proof, or a proper subset as the route for this ID.
Proposition 3.4 — sheaf of an injective module is flasque
If I is injective over noetherian A, then I~ on Spec A is flasque.
Not formalized. none; no complete checked declaration 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 I is injective over noetherian A, then I~ on Spec A is flasque. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, an incomplete proof, or a proper subset as the route for this ID.
Theorem 3.5 — vanishing on noetherian affine schemes
If X=Spec A with A noetherian and F quasi-coherent, then H^i(X,F)=0 for every i>0.
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked theorem proves affine quasi-coherent higher cohomology vanishing in the source generality.
Remark 3.5.1 — noetherian hypothesis can be removed
The affine quasi-coherent vanishing theorem remains true without the noetherian hypothesis, though Hartshorne does not prove that generality here.
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked theorem proves the non-noetherian affine quasi-coherent vanishing statement.
Corollary 3.6 — quasi-coherent sheaves embed in flasque quasi-coherent sheaves
On a noetherian scheme every quasi-coherent F embeds in a flasque quasi-coherent 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: On a noetherian scheme every quasi-coherent F embeds in a flasque quasi-coherent G. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, an incomplete proof, or a proper subset as the route for this ID.
Theorem 3.7 — Serre cohomological criterion for affineness
For noetherian X, the following are equivalent: X affine; H^i(X,F)=0 for every quasi-coherent F and i>0; H^1(X,I)=0 for every coherent ideal sheaf I.
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked Serre affine criterion was found.
Remark 3.7.1 — Stein-space analogy
Serre’s affine criterion is analogous to the characterization of Stein spaces by vanishing of coherent analytic sheaf 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: Serre’s affine criterion is analogous to the characterization of Stein spaces by vanishing of coherent analytic sheaf cohomology. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, an incomplete proof, or a proper subset as the route for this ID.
Construction — Čech complex for an open cover
For a well-ordered open cover U=(U_i) and abelian sheaf F, set C^p(U,F)=∏{i_0<⋯<i_p}F(U{i_0…i_p}) with the alternating restriction coboundary; d²=0.
Formalized. Mathlib/CategoryTheory/Sites/SheafCohomology/Cech.lean::CategoryTheory.Sheaf.cechComplexFunctor — Pinned Mathlib realizes the complete source interface: For a well-ordered open cover U=(U_i) and abelian sheaf F, set C^p(U,F)=∏{i_0<⋯<i_p}F(U{i_0…i_p}) with the alternating restriction coboundary; d²=0.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d
Remark 4.0.1 — alternating-index convention
Extend a Čech cochain component to arbitrary index tuples by zero on repetitions and the sign of permutations; the usual differential formula then applies without ordering hypotheses.
Not formalized. none; no complete checked declaration under strict bundle semantics — As of 2026-09-06, no checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: Extend a Čech cochain component to arbitrary index tuples by zero on repetitions and the sign of permutations; the usual differential formula then applies without ordering hypotheses. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, an incomplete proof, or a proper subset as the route for this ID.
Definition — Čech cohomology
Define Čech Hp(U,F)=hp(C^•(U,F)).
Not formalized. none; no complete checked declaration under strict bundle semantics — The Čech complex is formalized, but the audit did not find a named Čech-cohomology object matching Hartshorne’s definition as a complete route.
Caution 4.0.2 — fixed-cover Čech cohomology is not generally a δ-functor
For a fixed cover, a short exact sequence of sheaves need not induce a long exact Čech sequence; even the one-open-set cover reflects nonexactness of 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: For a fixed cover, a short exact sequence of sheaves need not induce a long exact Čech sequence; even the one-open-set cover reflects nonexactness of global sections. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, an incomplete proof, or a proper subset as the route for this ID.
Example 4.0.3 — Čech computation on P¹
For P¹ covered by its two standard affine lines, the Čech complex computes cohomology of Ω_{P¹}; Hartshorne exhibits the two-term section complex and its quotient explicitly.
Not formalized. none; no complete checked declaration 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¹ covered by its two standard affine lines, the Čech complex computes cohomology of Ω_{P¹}; Hartshorne exhibits the two-term section complex and its quotient explicitly. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, an incomplete proof, or a proper subset as the route for this ID.
Example 4.0.4 — constant sheaf on the circle
For S¹ covered by two connected semicircles with two-component overlap and constant Z, the two-term Čech complex gives Čech H^0≅Z and H^1≅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 S¹ covered by two connected semicircles with two-component overlap and constant Z, the two-term Čech complex gives Čech H^0≅Z and H^1≅Z. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, an incomplete proof, or a proper subset as the route for this ID.
Lemma 4.1 — Čech degree zero equals global sections
For every X, open cover U, and sheaf F, Čech H^0(U,F)≅Γ(X,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 every X, open cover U, and sheaf F, Čech H^0(U,F)≅Γ(X,F). Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, an incomplete proof, or a proper subset as the route for this ID.
Lemma 4.2 — Čech sheaf complex resolves F
The sheafified Čech complex C^•(U,F), augmented by F→C^0(U,F), is an exact resolution 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: The sheafified Čech complex C^•(U,F), augmented by F→C^0(U,F), is an exact resolution of F. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, an incomplete proof, or a proper subset as the route for this ID.
Proposition 4.3 — higher Čech cohomology of flasque sheaves vanishes
If F is flasque, Čech H^p(U,F)=0 for every p>0 and every open cover 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: If F is flasque, Čech H^p(U,F)=0 for every p>0 and every open cover U. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, an incomplete proof, or a proper subset as the route for this ID.
Lemma 4.4 — natural comparison map
For every cover U and sheaf F there are natural functorial maps Čech Hp(U,F)→Hp(X,F).
Not formalized. none; no complete checked declaration under strict bundle semantics — The pinned Čech file constructs the complex but does not prove Hartshorne’s comparison map theorem.
Theorem 4.5 — Čech computes quasi-coherent cohomology on separated noetherian schemes
If X is noetherian separated, U is an affine open cover, and F is quasi-coherent, then Čech Hp(U,F)→Hp(X,F) is an isomorphism for all p≥0.
Not formalized. none; no complete checked declaration under strict bundle semantics — No pinned Čech-to-sheaf-cohomology comparison theorem for separated noetherian schemes was found.
Construction — graded cohomology module on projective space
For noetherian A, S=A[x_0,…,x_r], X=P^r_A, and any O_X-module F, set Γ_*(F)=⊕_{n∈Z}Γ(X,F(n)), a graded S-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 noetherian A, S=A[x_0,…,x_r], X=P^r_A, and any O_X-module F, set Γ_*(F)=⊕_{n∈Z}Γ(X,F(n)), a graded S-module. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, an incomplete proof, or a proper subset as the route for this ID.
Theorem 5.1 — cohomology of O(n) on projective space
For X=P^r_A, r≥1: Γ_*(O_X)≅S; H^i(X,O_X(n))=0 for 0<i<r; H^r(X,O_X(−r−1))≅A; and multiplication gives perfect pairings H0(O(n))×Hr(O(−n−r−1))→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 X=P^r_A, r≥1: Γ_*(O_X)≅S; H^i(X,O_X(n))=0 for 0<i<r; H^r(X,O_X(−r−1))≅A; and multiplication gives perfect pairings H0(O(n))×Hr(O(−n−r−1))→A. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, an incomplete proof, or a proper subset as the route for this ID.
Theorem 5.2 — Serre finiteness and vanishing
If X is projective over noetherian A, O_X(1) is very ample, and F coherent, then every H^i(X,F) is finite over A and H^i(X,F(n))=0 for all i>0 and 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_X(1) is very ample, and F coherent, then every H^i(X,F) is finite over A and H^i(X,F(n))=0 for all i>0 and n≫0. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, an incomplete proof, or a proper subset as the route for this ID.
Remark 5.2.1 — finiteness of global sections
The case i=0 of Serre finiteness says Γ(X,F) is a finite A-module for coherent F, recovering II.5.19.
Not formalized. none; no complete checked declaration 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 case i=0 of Serre finiteness says Γ(X,F) is a finite A-module for coherent F, recovering II.5.19. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, an incomplete proof, or a proper subset as the route for this ID.
Proposition 5.3 — cohomological criterion for ampleness
For X proper over noetherian A and invertible L, L is ample iff for every coherent F there is n_0 with Hi(X,F⊗Ln)=0 for every i>0 and 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: For X proper over noetherian A and invertible L, L is ample iff for every coherent F there is n_0 with Hi(X,F⊗Ln)=0 for every i>0 and n≥n_0. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, an incomplete proof, or a proper subset as the route for this ID.
Definition — global Ext and sheaf Ext
For a ringed space X and O_X-module F, Ext^i(F,−) is the right derived functor of Hom(F,−), and sheaf Ext^i(F,−) is the right derived functor of internal Hom(F,−).
Not formalized. none; no complete checked declaration under strict bundle semantics — Global Ext is formalized, but the row also requires internal sheaf Ext; no checked internal-Hom/sheaf-Ext derived interface exists.
Lemma 6.1 — restriction preserves injectives
If I is injective in Mod(X), then I|_U is injective in Mod(U) for every open U⊆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 I is injective in Mod(X), then I|_U is injective in Mod(U) for every open U⊆X. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, an incomplete proof, or a proper subset as the route for this ID.
Proposition 6.2 — sheaf Ext is local
For open U⊆X, sheaf Ext_X^i(F,G)|_U≅sheaf Ext_U^i(F|_U,G|_U) naturally.
Not formalized. none; no complete checked declaration 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 open U⊆X, sheaf Ext_X^i(F,G)|_U≅sheaf Ext_U^i(F|_U,G|_U) naturally. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, an incomplete proof, or a proper subset as the route for this ID.
Proposition 6.3 — Ext from OX
For every O_X-module G, sheaf Ext^0(O_X,G)=G, sheaf Ext^i(O_X,G)=0 for i>0, and global Exti(O_X,G)≅Hi(X,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: For every O_X-module G, sheaf Ext^0(O_X,G)=G, sheaf Ext^i(O_X,G)=0 for i>0, and global Exti(O_X,G)≅Hi(X,G). Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, an incomplete proof, or a proper subset as the route for this ID.
Proposition 6.4 — long exact Ext sequence in the first variable
A short exact sequence 0→F′→F→F″→0 induces long exact sequences Exti(F″,G)→Exti(F,G)→Ext^i(F′,G)→… and likewise for sheaf Ext.
Not formalized. none; no complete checked declaration 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 short exact sequence 0→F′→F→F″→0 induces long exact sequences Exti(F″,G)→Exti(F,G)→Ext^i(F′,G)→… and likewise for sheaf Ext. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, an incomplete proof, or a proper subset as the route for this ID.
Proposition 6.5 — computing sheaf Ext from a locally free resolution
If L_•→F is a resolution by locally free finite-rank sheaves, then sheaf Exti(F,G)≅hi(Hom(L_•,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: If L_•→F is a resolution by locally free finite-rank sheaves, then sheaf Exti(F,G)≅hi(Hom(L_•,G)). Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, an incomplete proof, or a proper subset as the route for this ID.
Example 6.5.1 — coherent sheaves on quasi-projective schemes admit locally free resolutions
On a scheme quasi-projective over a noetherian affine base, every coherent sheaf is a quotient of a locally free sheaf and hence admits a locally free resolution usable in Proposition 6.5.
Not formalized. none; no complete checked declaration 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 scheme quasi-projective over a noetherian affine base, every coherent sheaf is a quotient of a locally free sheaf and hence admits a locally free resolution usable in Proposition 6.5. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, an incomplete proof, or a proper subset as the route for this ID.
Caution 6.5.2 — no general projective-resolution derived functor on Mod(X)
The preceding exactness/computation does not make sheaf Ext a right derived functor in its first variable: Mod(X) generally does not have enough projectives.
Not formalized. none; no complete checked declaration 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/computation does not make sheaf Ext a right derived functor in its first variable: Mod(X) generally does not have enough projectives. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, an incomplete proof, or a proper subset as the route for this ID.
Lemma 6.6 — tensoring an injective by a vector bundle
If L is locally free of finite rank and I injective, then L⊗I is injective.
Not formalized. none; no complete checked declaration under strict bundle semantics — As of 2026-09-06, no checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: If L is locally free of finite rank and I injective, then L⊗I is injective. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, an incomplete proof, or a proper subset as the route for this ID.
Proposition 6.7 — Ext and locally free twists
For locally free finite-rank L with dual L∨, Exti(F⊗L,G)≅Exti(F,L∨⊗G); for sheaf Ext this also identifies with sheaf Ext^i(F,G)⊗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 locally free finite-rank L with dual L∨, Exti(F⊗L,G)≅Exti(F,L∨⊗G); for sheaf Ext this also identifies with sheaf Ext^i(F,G)⊗L∨. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, an incomplete proof, or a proper subset as the route for this ID.
Proposition 6.8 — stalks of sheaf Ext
If X is noetherian, F coherent, G arbitrary, and x∈X, then (sheaf Ext_X^i(F,G))x≅Ext^i{O_{X,x}}(F_x,G_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, F coherent, G arbitrary, and x∈X, then (sheaf Ext_X^i(F,G))x≅Ext^i{O_{X,x}}(F_x,G_x). Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, an incomplete proof, or a proper subset as the route for this ID.
Proposition 6.9 — global Ext from sheaf Ext after twisting
For projective X over noetherian A with very ample O(1), coherent F,G, and fixed i, Ext^i(F,G(n))≅Γ(X,sheaf Ext^i(F,G(n))) 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: For projective X over noetherian A with very ample O(1), coherent F,G, and fixed i, Ext^i(F,G(n))≅Γ(X,sheaf Ext^i(F,G(n))) for all n≫0. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, an incomplete proof, or a proper subset as the route for this ID.
Remark 6.9.1 — global-to-local Ext spectral sequence
On a general ringed space, global Ext and sheaf Ext are related by a spectral sequence.
Not formalized. none; no complete checked declaration 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 general ringed space, global Ext and sheaf Ext are related by a spectral sequence. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, an incomplete proof, or a proper subset as the route for this ID.
Definition — projective resolution and projective dimension
A projective resolution of an A-module M is an exact complex of projective modules ending in M; pd(M) is the least possible finite length, or +∞ if none exists.
Formalized. Mathlib/CategoryTheory/Abelian/Projective/Resolution.lean::ProjectiveResolution; Mathlib/CategoryTheory/Abelian/Projective/Dimension.lean::projectiveDimension — Pinned Mathlib realizes the complete source interface: A projective resolution of an A-module M is an exact complex of projective modules ending in M; pd(M) is the least possible finite length, or +∞ if none exists.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d
Proposition 6.10A — Ext detects projectivity and projective dimension
M is projective iff Ext^1_A(M,N)=0 for all N; pd(M)≤n iff Ext^i_A(M,N)=0 for every i>n and every N.
Formalized. Mathlib/CategoryTheory/Abelian/Projective/Dimension.lean::projective_iff_subsingleton_ext_one, hasProjectiveDimensionLT_iff — Pinned Mathlib realizes the complete source interface: M is projective iff Ext^1_A(M,N)=0 for all N; pd(M)≤n iff Ext^i_A(M,N)=0 for every i>n and every N.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d
Proposition 6.11A — projective dimension over a regular local ring
If A is regular local, then pd(M)≤dim A for every A-module M, and for its residue field k one has pd(k)=dim A.
Not formalized. none; no complete checked declaration under strict bundle semantics — Projective dimension is formalized, but the regular-local-ring global-dimension theorem in this row was not found.
Proposition 6.12A — Auslander–Buchsbaum formula
If A is a regular local ring of dimension n and M is finitely generated, then pd_A(M)+depth_A(M)=n.
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked Auslander–Buchsbaum formula at the pin was found.
Theorem 7.1 — duality on projective space
For X=P^n_k with canonical sheaf ω_X: H^n(X,ω_X)≅k; Hom(F,ω_X) pairs perfectly with H^n(X,F); and Exti(F,ω_X)≅H{n−i}(X,F)^∨ naturally for coherent 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 X=P^n_k with canonical sheaf ω_X: H^n(X,ω_X)≅k; Hom(F,ω_X) pairs perfectly with H^n(X,F); and Exti(F,ω_X)≅H{n−i}(X,F)^∨ naturally for coherent F. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, an incomplete proof, or a proper subset as the route for this ID.
Remark 7.1.1 — intrinsic normalization of projective-space duality
Writing the duality theorem with the canonical sheaf makes the trace generator natural under changes of homogeneous coordinates; Hartshorne exhibits an invariant Čech cocycle generator.
Not formalized. none; no complete checked declaration under strict bundle semantics — As of 2026-09-06, no checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: Writing the duality theorem with the canonical sheaf makes the trace generator natural under changes of homogeneous coordinates; Hartshorne exhibits an invariant Čech cocycle generator. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, an incomplete proof, or a proper subset as the route for this ID.
Definition — dualizing sheaf and trace
For proper n-dimensional X/k, a dualizing sheaf is coherent ω_X^∘ with trace t:Hn(X,ω_X∘)→k such that Hom(F,ω_X∘)→Hn(X,F)^∨ is an isomorphism for every coherent 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 proper n-dimensional X/k, a dualizing sheaf is coherent ω_X^∘ with trace t:Hn(X,ω_X∘)→k such that Hom(F,ω_X∘)→Hn(X,F)^∨ is an isomorphism for every coherent F. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, an incomplete proof, or a proper subset as the route for this ID.
Proposition 7.2 — uniqueness of a dualizing sheaf
A dualizing sheaf with trace, if it exists, is unique up to a unique isomorphism compatible with the trace.
Not formalized. none; no complete checked declaration 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 dualizing sheaf with trace, if it exists, is unique up to a unique isomorphism compatible with the trace. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, an incomplete proof, or a proper subset as the route for this ID.
Lemma 7.3 — low Ext vanishing for a projective closed subscheme
If X⊂P^N_k is closed of codimension r, then sheaf Ext_P^i(O_X,ω_P)=0 for every i<r.
Not formalized. none; no complete checked declaration under strict bundle semantics — As of 2026-09-06, no checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: If X⊂P^N_k is closed of codimension r, then sheaf Ext_P^i(O_X,ω_P)=0 for every i<r. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, an incomplete proof, or a proper subset as the route for this ID.
Lemma 7.4 — Ext representation of the candidate dualizing sheaf
With X⊂P^N as above and ω_X^∘=sheaf Ext_P^r(O_X,ω_P), there is a functorial isomorphism Hom_X(F,ω_X∘)≅Ext_Pr(F,ω_P) for every O_X-module 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: With X⊂P^N as above and ω_X^∘=sheaf Ext_P^r(O_X,ω_P), there is a functorial isomorphism Hom_X(F,ω_X∘)≅Ext_Pr(F,ω_P) for every O_X-module F. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, an incomplete proof, or a proper subset as the route for this ID.
Proposition 7.5 — projective schemes have dualizing sheaves
Every projective scheme over a field has a dualizing sheaf, obtained from a projective embedding X⊂P^N as sheaf Ext_P^r(O_X,ω_P) with the trace induced by projective-space duality.
Not formalized. none; no complete checked declaration 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 projective scheme over a field has a dualizing sheaf, obtained from a projective embedding X⊂P^N as sheaf Ext_P^r(O_X,ω_P) with the trace induced by projective-space duality. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, an incomplete proof, or a proper subset as the route for this ID.
Theorem 7.6 — Serre duality for projective schemes
For projective n-dimensional X over algebraically closed k with dualizing ω and very ample O(1), there are natural θi:Exti(F,ω)→H{n−i}(F)∨; X is Cohen–Macaulay equidimensional iff the equivalent negative-twist vanishing holds, iff every θ^i 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: For projective n-dimensional X over algebraically closed k with dualizing ω and very ample O(1), there are natural θi:Exti(F,ω)→H{n−i}(F)∨; X is Cohen–Macaulay equidimensional iff the equivalent negative-twist vanishing holds, iff every θ^i is an isomorphism. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, an incomplete proof, or a proper subset as the route for this ID.
Remark 7.6.1 — duality for nonsingular and lci schemes
Nonsingular schemes and local complete intersections are Cohen–Macaulay, so the duality maps θ^i of Theorem 7.6 are isomorphisms in these cases.
Not formalized. none; no complete checked declaration under strict bundle semantics — As of 2026-09-06, no checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: Nonsingular schemes and local complete intersections are Cohen–Macaulay, so the duality maps θ^i of Theorem 7.6 are isomorphisms in these cases. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, an incomplete proof, or a proper subset as the route for this ID.
Corollary 7.7 — duality for locally free sheaves
On a projective Cohen–Macaulay equidimensional n-scheme, every locally free F satisfies Hi(X,F)≅H{n−i}(X,F∨⊗ω_X)^∨ naturally.
Not formalized. none; no complete checked declaration 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 Cohen–Macaulay equidimensional n-scheme, every locally free F satisfies Hi(X,F)≅H{n−i}(X,F∨⊗ω_X)^∨ naturally. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, an incomplete proof, or a proper subset as the route for this ID.
Corollary 7.8 — Enriques–Severi–Zariski lemma
If X is normal projective of dimension at least two, then for every locally free F, H^1(X,F(−q))=0 for q≫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 normal projective of dimension at least two, then for every locally free F, H^1(X,F(−q))=0 for q≫0. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, an incomplete proof, or a proper subset as the route for this ID.
Corollary 7.9 — connectedness of ample divisors
If X is integral normal projective of dimension at least two over algebraically closed k, the support of an effective ample divisor is connected.
Not formalized. none; no complete checked declaration under strict bundle semantics — As of 2026-09-06, no checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: If X is integral normal projective of dimension at least two over algebraically closed k, the support of an effective ample divisor is connected. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, an incomplete proof, or a proper subset as the route for this ID.
Remark 7.9.1 — Bertini sections are irreducible in dimension at least two
Combining connectedness with regularity shows the hyperplane sections occurring in Bertini are irreducible as well as nonsingular when dim X≥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: Combining connectedness with regularity shows the hyperplane sections occurring in Bertini are irreducible as well as nonsingular when dim X≥2. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, an incomplete proof, or a proper subset as the route for this ID.
Construction — Koszul complex
For f_1,…,f_r∈A, K_•(f_1,…,f_r) is the exterior algebra on a free rank-r module with the standard contraction differential; for M set K_•(f;M)=K_•(f)⊗_A M.
Not formalized. none; no complete checked declaration under strict bundle semantics — Mathlib has regular-sequence infrastructure, but RegularSequence.lean explicitly lists Koszul regular sequences as TODO and no Koszul complex is defined.
Proposition 7.10A — Koszul homology of a regular sequence
If f_1,…,f_r is an M-regular sequence, then H_i(K_•(f;M))=0 for i>0 and H_0≅M/(f_1,…,f_r)M.
Not formalized. none; no complete checked declaration under strict bundle semantics — No Koszul complex exists at the pin, so its regular-sequence homology theorem is unmatched.
Theorem 7.11 — dualizing sheaf of a local complete intersection
If X⊂P^N_k is an lci of codimension r with ideal I, then ω_X^∘≅ω_P|_X⊗(∧r(I/I²))∨; in particular ω_X^∘ is 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: If X⊂P^N_k is an lci of codimension r with ideal I, then ω_X^∘≅ω_P|_X⊗(∧r(I/I²))∨; in particular ω_X^∘ is invertible. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, an incomplete proof, or a proper subset as the route for this ID.
Corollary 7.12 — dualizing equals canonical on nonsingular projective varieties
For a projective nonsingular variety, the dualizing sheaf is isomorphic to the canonical 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: For a projective nonsingular variety, the dualizing sheaf is isomorphic to the canonical sheaf. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, an incomplete proof, or a proper subset as the route for this ID.
Remark 7.12.1 — Serre duality with canonical sheaf
For projective nonsingular X, Theorem 7.6 and Corollary 7.7 hold with the canonical sheaf; in particular H^n(X,ω_X)≅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 projective nonsingular X, Theorem 7.6 and Corollary 7.7 hold with the canonical sheaf; in particular H^n(X,ω_X)≅k. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, an incomplete proof, or a proper subset as the route for this ID.
Remark 7.12.2 — arithmetic equals geometric genus for smooth projective curves
For a projective nonsingular curve, H^1(O_X) and H^0(ω_X) are dual, hence p_a=p_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: For a projective nonsingular curve, H^1(O_X) and H^0(ω_X) are dual, hence p_a=p_g. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, an incomplete proof, or a proper subset as the route for this ID.
Remark 7.12.3 — geometric genus and irregularity of a smooth projective surface
For a projective nonsingular surface, p_g=h^2(O_X), p_g≥p_a, and q=p_g−p_a=h^1(O_X) is the irregularity.
Not formalized. none; no complete checked declaration 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 projective nonsingular surface, p_g=h^2(O_X), p_g≥p_a, and q=p_g−p_a=h^1(O_X) is the irregularity. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, an incomplete proof, or a proper subset as the route for this ID.
Corollary 7.13 — duality for differential forms
If X is a nonsingular projective n-fold and Ωp=∧pΩ_{X/k}, then Hq(X,Ωp)≅H{n−q}(X,Ω{n−p})^∨ naturally.
Not formalized. none; no complete checked declaration 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 nonsingular projective n-fold and Ωp=∧pΩ_{X/k}, then Hq(X,Ωp)≅H{n−q}(X,Ω{n−p})^∨ naturally. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, an incomplete proof, or a proper subset as the route for this ID.
Remark 7.13.1 — Hodge numbers as biregular invariants
The numbers h^{p,q}=dim Hq(X,Ωp) are biregular invariants of a nonsingular projective 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: The numbers h^{p,q}=dim Hq(X,Ωp) are biregular invariants of a nonsingular projective variety. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, an incomplete proof, or a proper subset as the route for this ID.
Remark 7.14 — residues and curve duality
For complete nonsingular curves, residues provide an explicit construction of the trace map and an alternative proof of duality.
Not formalized. none; no complete checked declaration 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 complete nonsingular curves, residues provide an explicit construction of the trace map and an alternative proof of duality. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, an incomplete proof, or a proper subset as the route for this ID.
Theorem 7.14.1 — existence of residues
For each closed P on a complete nonsingular curve with function field K there is a unique k-linear res_P:Ω_{K/k}→k vanishing on regular differentials, killing f^n df for n≠−1, and sending f^{-1}df to v_P(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 each closed P on a complete nonsingular curve with function field K there is a unique k-linear res_P:Ω_{K/k}→k vanishing on regular differentials, killing f^n df for n≠−1, and sending f^{-1}df to v_P(f). Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, an incomplete proof, or a proper subset as the route for this ID.
Theorem 7.14.2 — residue theorem
For every rational differential τ on a complete nonsingular curve, the finite sum Σ_P res_P(τ) over closed points is zero.
Not formalized. none; no complete checked declaration under strict bundle semantics — As of 2026-09-06, no checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: For every rational differential τ on a complete nonsingular curve, the finite sum Σ_P res_P(τ) over closed points is zero. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, an incomplete proof, or a proper subset as the route for this ID.
Construction — duality trace from the sum of residues
Using the flasque resolution of O_X by the constant function-field sheaf and its quotient, tensoring with Ω_X identifies H^1(X,Ω_X) as a quotient of ⊕_P Ω_K/Ω_P; the sum of residues descends to the Serre-duality trace H^1(X,Ω_X)→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: Using the flasque resolution of O_X by the constant function-field sheaf and its quotient, tensoring with Ω_X identifies H^1(X,Ω_X) as a quotient of ⊕_P Ω_K/Ω_P; the sum of residues descends to the Serre-duality trace H^1(X,Ω_X)→k. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, an incomplete proof, or a proper subset as the route for this ID.
Remark 7.15 — Kodaira vanishing theorem
For smooth projective X/C of dimension n and ample L, H^i(X,L⊗ω_X)=0 for i>0, equivalently by Serre duality Hi(X,L{-1})=0 for i<n; Hartshorne notes characteristic-p counterexamples.
Not formalized. none; no complete checked declaration 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 X/C of dimension n and ample L, H^i(X,L⊗ω_X)=0 for i>0, equivalently by Serre duality Hi(X,L{-1})=0 for i<n; Hartshorne notes characteristic-p counterexamples. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, an incomplete proof, or a proper subset as the route for this ID.
Definition — higher direct images
For continuous f:X→Y, R^i f_:Ab(X)→Ab(Y) is the ith right derived functor of the left exact direct-image functor f_.
Not formalized. none; no complete checked declaration under strict bundle semantics — Right derived functors and sheaf pushforward are separately formalized, but no checked higher-direct-image functor package for topological sheaves was found.
Proposition 8.1 — local cohomology description of R^i f
R^i f_*F is the sheaf associated to the presheaf V↦Hi(f{-1}V,F|_{f^{-1}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: R^i f_*F is the sheaf associated to the presheaf V↦Hi(f{-1}V,F|_{f^{-1}V}). Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, an incomplete proof, or a proper subset as the route for this ID.
Corollary 8.2 — restriction of higher direct images
For open V⊆Y and f′:f^{-1}V→V, (R^i f_F)|V≅R^i f′**(F|_{f^{-1}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 open V⊆Y and f′:f^{-1}V→V, (R^i f_F)|V≅R^i f′**(F|_{f^{-1}V}). Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, an incomplete proof, or a proper subset as the route for this ID.
Corollary 8.3 — flasque sheaves are f-acyclic
If F is flasque on X, then R^i f_*F=0 for every i>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 F is flasque on X, then R^i f_*F=0 for every i>0. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, an incomplete proof, or a proper subset as the route for this ID.
Proposition 8.4 — higher direct images in module categories
For a morphism of ringed spaces, R^i f_* may be computed as the derived functors of f_*:Mod(X)→Mod(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 morphism of ringed spaces, R^i f_* may be computed as the derived functors of f_*:Mod(X)→Mod(Y). Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, an incomplete proof, or a proper subset as the route for this ID.
Proposition 8.5 — affine-target description
If X is noetherian, Y=Spec A, f:X→Y, and F quasi-coherent, then R^i f_*F≅~H^i(X,F).
Not formalized. none; no complete checked declaration under strict bundle semantics — The Atlas statement bank has an affine-pushforward analogue, but its proof is by sorry; it is not an acceptable implementation route.
Corollary 8.6 — higher direct images preserve quasi-coherence
If X is noetherian and f:X→Y is a scheme morphism, then R^i f_*F is quasi-coherent for every quasi-coherent 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 X is noetherian and f:X→Y is a scheme morphism, then R^i f_*F is quasi-coherent for every quasi-coherent F. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, an incomplete proof, or a proper subset as the route for this ID.
Proposition 8.7 — Čech computation of higher direct images
For f between separated noetherian schemes, quasi-coherent F, and an affine open cover U of X, R^p f_F≅h^p(f_C^•(U,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 f between separated noetherian schemes, quasi-coherent F, and an affine open cover U of X, R^p f_F≅h^p(f_C^•(U,F)). Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, an incomplete proof, or a proper subset as the route for this ID.
Theorem 8.8 — projective direct-image finiteness and vanishing
For projective f:X→Y of noetherian schemes, very ample O_X(1), and coherent F: f^f_F(n)→F(n) is surjective for n≫0; every R^i f_F is coherent; and R^i f_F(n)=0 for i>0,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 projective f:X→Y of noetherian schemes, very ample O_X(1), and coherent F: f^f_F(n)→F(n) is surjective for n≫0; every R^i f_F is coherent; and R^i f_F(n)=0 for i>0,n≫0. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, an incomplete proof, or a proper subset as the route for this ID.
Remark 8.8.1 — proper direct-image coherence
The coherence assertion for R^i f_* remains true for proper morphisms of noetherian schemes; Hartshorne notes Grauert’s analytic analogue.
Not formalized. none; no complete checked declaration 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 coherence assertion for R^i f_* remains true for proper morphisms of noetherian schemes; Hartshorne notes Grauert’s analytic analogue. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, an incomplete proof, or a proper subset as the route for this ID.
Definition — flat module and flat algebra
An A-module M is flat when N↦M⊗_A N is exact; a ring map A→B is flat when B is flat as an A-module.
Formalized. Mathlib/RingTheory/Flat/Basic.lean::Module.Flat, Module.Flat.iff_lTensor_exact — Pinned Mathlib realizes the complete source interface: An A-module M is flat when N↦M⊗_A N is exact; a ring map A→B is flat when B is flat as an A-module.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d
Proposition 9.1A — criteria and stability for flat modules
Flatness is equivalent to injectivity a⊗M→M for every finitely generated ideal a; it is preserved by base extension and transitivity, is local at primes, behaves in short exact sequences as stated, and over a local noetherian ring a finite module is flat iff free.
Not formalized. none; no complete checked declaration under strict bundle semantics — As of 2026-09-06, no checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: Flatness is equivalent to injectivity a⊗M→M for every finitely generated ideal a; it is preserved by base extension and transitivity, is local at primes, behaves in short exact sequences as stated, and over a local noetherian ring a finite module is flat iff free. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, an incomplete proof, or a proper subset as the route for this ID.
Example 9.1.1 — localization is flat
Every localization S^{-1}A is flat over A; if a B-module M is A-flat, then S^{-1}M is also A-flat.
Formalized. Mathlib/RingTheory/Flat/Localization.lean::IsLocalization.flat — Pinned Mathlib realizes the complete source interface: Every localization S^{-1}A is flat over A; if a B-module M is A-flat, then S^{-1}M is also A-flat.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d
Example 9.1.2 — noetherian adic completion is flat
For noetherian A and ideal a, the a-adic completion  is a flat A-algebra.
Formalized. Mathlib/RingTheory/AdicCompletion/AsTensorProduct.lean::AdicCompletion.flat_of_isNoetherian — Pinned Mathlib realizes the complete source interface: For noetherian A and ideal a, the a-adic completion  is a flat A-algebra.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d
Example 9.1.3 — flat modules over a PID are torsion-free modules
For a PID A, an A-module is flat iff torsion-free.
Formalized. Mathlib/RingTheory/Flat/TorsionFree.lean::Module.Flat.flat_iff_torsion_eq_bot_of_isBezout; Submodule.isTorsionFree_iff_torsion_eq_bot — Pinned Mathlib proves flat iff torsion-free over every Bézout domain, hence in particular over a PID, exactly the source statement.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d
Definition — sheaf flat over a base and flat morphism
For f:X→Y and O_X-module F, F is flat over Y at x when F_x is flat over O_{Y,f(x)}; it is flat over Y if so everywhere. X is flat over Y when O_X is.
Not formalized. none; no complete checked declaration under strict bundle semantics — Mathlib formalizes flat modules and flat scheme morphisms, but this row also defines flatness of an arbitrary sheaf over a base morphism; no complete combined interface was found.
Proposition 9.2 — stability and affine criteria for scheme flatness
Open immersions are flat; flatness of sheaves is preserved by base change and transitivity; for Spec B→Spec A, M~ is flat over Spec A iff M is A-flat; on noetherian X, coherent F is flat over X iff locally free.
Not formalized. none; no complete checked declaration under strict bundle semantics — As of 2026-09-06, no checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: Open immersions are flat; flatness of sheaves is preserved by base change and transitivity; for Spec B→Spec A, M~ is flat over Spec A iff M is A-flat; on noetherian X, coherent F is flat over X iff locally free. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, an incomplete proof, or a proper subset as the route for this ID.
Proposition 9.3 — cohomology commutes with flat base extension
In a cartesian square obtained from a separated finite-type morphism f:X→Y of noetherian schemes by flat u:Y′→Y, for quasi-coherent F there are natural isomorphisms uR^i f_F≅Ri g_(v^F) for all 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: In a cartesian square obtained from a separated finite-type morphism f:X→Y of noetherian schemes by flat u:Y′→Y, for quasi-coherent F there are natural isomorphisms uR^i f_F≅Ri g_(v^F) for all i. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, an incomplete proof, or a proper subset as the route for this ID.
Remark 9.3.1 — natural base-change map without flatness
For arbitrary base change there is still a natural comparison uR^i f_F→Ri g_(v^F), though it need not be 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: For arbitrary base change there is still a natural comparison uR^i f_F→Ri g_(v^F), though it need not be an isomorphism. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, an incomplete proof, or a proper subset as the route for this ID.
Corollary 9.4 — cohomology of a fibre as tensor with its residue field
Under Proposition 9.3 with Y affine, for y∈Y and induced F_y on X_y, Hi(X_y,F_y)≅Hi(X,F⊗k(y)) naturally for all 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: Under Proposition 9.3 with Y affine, for y∈Y and induced F_y on X_y, Hi(X_y,F_y)≅Hi(X,F⊗k(y)) naturally for all i. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, an incomplete proof, or a proper subset as the route for this ID.
Definition/convention — flat family of schemes
A flat family is a family of fibres of a flat morphism; Hartshorne adopts flatness as the scheme-theoretic condition expressing a continuously varying algebraic family.
Not formalized. none; no complete checked declaration 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 flat family is a family of fibres of a flat morphism; Hartshorne adopts flatness as the scheme-theoretic condition expressing a continuously varying algebraic family. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, an incomplete proof, or a proper subset as the route for this ID.
Proposition 9.5 — dimension formula for flat morphisms
For flat f:X→Y of schemes finite type over a field and x∈X with y=f(x), dim_x X_y=dim_x X−dim_y 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 flat f:X→Y of schemes finite type over a field and x∈X with y=f(x), dim_x X_y=dim_x X−dim_y Y. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, an incomplete proof, or a proper subset as the route for this ID.
Corollary 9.6 — equidimensional total space versus fibres
If f:X→Y is flat finite type over a field and Y irreducible, then all irreducible components of X have dimension dim Y+n iff every irreducible component of every fibre has dimension n.
Not formalized. none; no complete checked declaration under strict bundle semantics — As of 2026-09-06, no checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: If f:X→Y is flat finite type over a field and Y irreducible, then all irreducible components of X have dimension dim Y+n iff every irreducible component of every fibre has dimension n. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, an incomplete proof, or a proper subset as the route for this ID.
Definition — associated point of a scheme
A point x∈X is associated if the maximal ideal of O_{X,x} is an associated prime of zero, equivalently every element of that maximal ideal is a zero divisor.
Not formalized. none; no complete checked declaration under strict bundle semantics — As of 2026-09-06, no checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: A point x∈X is associated if the maximal ideal of O_{X,x} is an associated prime of zero, equivalently every element of that maximal ideal is a zero divisor. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, an incomplete proof, or a proper subset as the route for this ID.
Proposition 9.7 — flatness over a regular integral curve
If Y is regular integral of dimension one, f:X→Y is flat iff every associated point of X maps to the generic point of Y; for reduced X this means every irreducible component dominates Y.
Not formalized. none; no complete checked declaration under strict bundle semantics — As of 2026-09-06, no checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: If Y is regular integral of dimension one, f:X→Y is flat iff every associated point of X maps to the generic point of Y; for reduced X this means every irreducible component dominates Y. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, an incomplete proof, or a proper subset as the route for this ID.
Example 9.7.1 — normalization of a nodal curve is not flat
The normalization map of a nodal curve is not flat: its finite pushforward has rank one generically but needs two generators at the node, hence is not locally free there.
Not formalized. none; no complete checked declaration 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 normalization map of a nodal curve is not flat: its finite pushforward has rank one generically but needs two generators at the node, hence is not locally free there. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, an incomplete proof, or a proper subset as the route for this ID.
Example 9.7.2 — dominance over a regular higher-dimensional base does not imply flatness
Blowing up a point of A² gives a dominant map between nonsingular schemes that is not flat because the exceptional fibre has dimension too large.
Not formalized. none; no complete checked declaration under strict bundle semantics — As of 2026-09-06, no checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: Blowing up a point of A² gives a dominant map between nonsingular schemes that is not flat because the exceptional fibre has dimension too large. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, an incomplete proof, or a proper subset as the route for this ID.
Proposition 9.8 — unique flat limit over a missing point of a regular curve
If Y is regular integral one-dimensional, P∈Y closed, and X⊂P^n_{Y−P} is closed and flat over Y−P, then its scheme-theoretic closure in P^n_Y is the unique closed subscheme extending X and flat over Y.
Not formalized. none; no complete checked declaration under strict bundle semantics — As of 2026-09-06, no checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: If Y is regular integral one-dimensional, P∈Y closed, and X⊂P^n_{Y−P} is closed and flat over Y−P, then its scheme-theoretic closure in P^n_Y is the unique closed subscheme extending X and flat over Y. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, an incomplete proof, or a proper subset as the route for this ID.
Remark 9.8.1 — valuative properness of the Hilbert scheme
Proposition 9.8 is the essential valuative “pass to the limit” statement showing connected components of the Hilbert scheme of subschemes of projective space are proper.
Not formalized. none; no complete checked declaration under strict bundle semantics — As of 2026-09-06, no checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: Proposition 9.8 is the essential valuative “pass to the limit” statement showing connected components of the Hilbert scheme of subschemes of projective space are proper. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, an incomplete proof, or a proper subset as the route for this ID.
Example 9.8.2 — flat families can acquire reducible or nonreduced special fibres
The earlier degenerations ay=x² and xy=t are flat families whose general fibres are integral but whose special fibres are respectively nonreduced and reducible.
Not formalized. none; no complete checked declaration 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 earlier degenerations ay=x² and xy=t are flat families whose general fibres are integral but whose special fibres are respectively nonreduced and reducible. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, an incomplete proof, or a proper subset as the route for this ID.
Example 9.8.3 — projection as a flat limit
Scaling one coordinate of a projective subscheme produces a trivial flat family over A¹{0}; Proposition 9.8 extends it uniquely over 0, where the support is the projection from the scaling 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: Scaling one coordinate of a projective subscheme produces a trivial flat family over A¹{0}; Proposition 9.8 extends it uniquely over 0, where the support is the projection from the scaling center. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, an incomplete proof, or a proper subset as the route for this ID.
Example 9.8.4 — twisted cubic degenerates to a nodal cubic with an embedded point
For a projected twisted cubic, the unique flat limit has support the nodal plane cubic but carries a nonzero square-zero embedded element at its node; the nilpotent records the lost transverse direction.
Not formalized. none; no complete checked declaration 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 projected twisted cubic, the unique flat limit has support the nodal plane cubic but carries a nonzero square-zero embedded element at its node; the nilpotent records the lost transverse direction. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, an incomplete proof, or a proper subset as the route for this ID.
Example 9.8.5 — algebraic families of Cartier divisors and flatness
For effective Cartier D on X×T with T a nonsingular curve, fibrewise intersections D_t are defined when local equations remain nonzerodivisors; these form an algebraic family of divisors, and D→T is flat iff every D_t is defined.
Not formalized. none; no complete checked declaration under strict bundle semantics — As of 2026-09-06, no checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: For effective Cartier D on X×T with T a nonsingular curve, fibrewise intersections D_t are defined when local equations remain nonzerodivisors; these form an algebraic family of divisors, and D→T is flat iff every D_t is defined. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, an incomplete proof, or a proper subset as the route for this ID.
Theorem 9.9 — flatness criterion by Hilbert polynomial
For integral noetherian T and closed X⊂P^n_T, X is flat over T iff the Hilbert polynomial of the fibre X_t is independent of t.
Not formalized. none; no complete checked declaration 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 noetherian T and closed X⊂P^n_T, X is flat over T iff the Hilbert polynomial of the fibre X_t is independent of t. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, an incomplete proof, or a proper subset as the route for this ID.
Corollary 9.10 — dimension, degree, and arithmetic genus are constant in projective flat families
For connected noetherian T and closed X⊂P^n_T flat over T, fibre dimension, degree, and arithmetic genus are independent of t.
Not formalized. none; no complete checked declaration 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 connected noetherian T and closed X⊂P^n_T flat over T, fibre dimension, degree, and arithmetic genus are independent of t. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, an incomplete proof, or a proper subset as the route for this ID.
Definition — algebraic family of varieties
For surjective f:X→T of varieties over algebraically closed k, the reduced fibres X_(t) form an algebraic family when each is irreducible of expected dimension and the scheme-theoretic fibre is reduced at its generic point (multiplicity 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: For surjective f:X→T of varieties over algebraically closed k, the reduced fibres X_(t) form an algebraic family when each is irreducible of expected dimension and the scheme-theoretic fibre is reduced at its generic point (multiplicity one). Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, an incomplete proof, or a proper subset as the route for this ID.
Example 9.10.1 — reduced fibres can lose flat invariants
Taking reduced fibres in Example 9.8.4 gives an algebraic family of varieties whose arithmetic genus jumps from 0 to 1; the nilpotent embedded point in the flat scheme fibre is exactly what restores constancy.
Not formalized. none; no complete checked declaration under strict bundle semantics — As of 2026-09-06, no checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: Taking reduced fibres in Example 9.8.4 gives an algebraic family of varieties whose arithmetic genus jumps from 0 to 1; the nilpotent embedded point in the flat scheme fibre is exactly what restores constancy. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, an incomplete proof, or a proper subset as the route for this ID.
Theorem 9.11 — algebraic families of normal varieties over a smooth curve are flat
An algebraic family of normal varieties parametrized by a nonsingular curve over algebraically closed k is a flat family of 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: An algebraic family of normal varieties parametrized by a nonsingular curve over algebraically closed k is a flat family of schemes. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, an incomplete proof, or a proper subset as the route for this ID.
Lemma 9.12 — Hironaka lemma
Let A be a local noetherian finite-type domain over a field and t∈A. If tA has one minimal associated prime p, t generates the maximal ideal of A_p, and A/p is normal, then p=tA and A is normal.
Not formalized. none; no complete checked declaration under strict bundle semantics — As of 2026-09-06, no checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: Let A be a local noetherian finite-type domain over a field and t∈A. If tA has one minimal associated prime p, t generates the maximal ideal of A_p, and A/p is normal, then p=tA and A is normal. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, an incomplete proof, or a proper subset as the route for this ID.
Corollary 9.13 — Igusa constancy theorem
For an algebraic family of normal projective varieties parametrized by a variety T, the Hilbert polynomial, hence arithmetic genus, is independent of t.
Not formalized. none; no complete checked declaration 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 algebraic family of normal projective varieties parametrized by a variety T, the Hilbert polynomial, hence arithmetic genus, is independent of t. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, an incomplete proof, or a proper subset as the route for this ID.
Example 9.13.1 — infinitesimal deformation over dual numbers
For D=k[t]/(t²), an infinitesimal deformation of finite-type X_0/k is a D-flat scheme X′ with X′⊗_D k≅X_0; tangent vectors to a base of a global flat family produce such deformations by base change.
Not formalized. none; no complete checked declaration 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=k[t]/(t²), an infinitesimal deformation of finite-type X_0/k is a D-flat scheme X′ with X′⊗_D k≅X_0; tangent vectors to a base of a global flat family produce such deformations by base change. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, an incomplete proof, or a proper subset as the route for this ID.
Example 9.13.2 — infinitesimal deformations of a nonsingular scheme are classified by H¹(TX)
For nonsingular X over algebraically closed k, infinitesimal deformations up to isomorphism correspond to H^1(X,T_X); flatness identifies a deformation with an infinitesimal extension by 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 nonsingular X over algebraically closed k, infinitesimal deformations up to isomorphism correspond to H^1(X,T_X); flatness identifies a deformation with an infinitesimal extension by O_X. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, an incomplete proof, or a proper subset as the route for this ID.
Remark 9.13.3 — deformation-theory tangent and obstruction spaces
Hartshorne records the deformation-theoretic principle that first-order deformations are controlled by H^1(T_X), automorphisms by H^0(T_X), and obstructions live in H^2(T_X) in the nonsingular case.
Not formalized. none; no complete checked declaration under strict bundle semantics — As of 2026-09-06, no checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: Hartshorne records the deformation-theoretic principle that first-order deformations are controlled by H^1(T_X), automorphisms by H^0(T_X), and obstructions live in H^2(T_X) in the nonsingular case. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, an incomplete proof, or a proper subset as the route for this ID.
Definition — smooth morphism of relative dimension n
For finite-type k-schemes, f:X→Y is smooth of relative dimension n when it is flat, corresponding irreducible components differ in dimension by n, and dim_{k(x)}(Ω_{X/Y}⊗k(x))=n at every x.
Not formalized. none; no complete checked declaration under strict bundle semantics — Mathlib has AlgebraicGeometry.Smooth, but the checked API defines smoothness through formal smoothness/finite presentation rather than Hartshorne’s flat-plus-differential-dimension criterion, and no equivalence theorem to this exact row was found.
Example 10.0.1 — relative affine and projective spaces are smooth
A^n_Y and P^n_Y are smooth of relative dimension n over every finite-type k-scheme 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: A^n_Y and P^n_Y are smooth of relative dimension n over every finite-type k-scheme Y. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, an incomplete proof, or a proper subset as the route for this ID.
Example 10.0.2 — differential criterion on an integral source
When X is integral, the differential-rank condition in smoothness is equivalent to Ω_{X/Y} being locally free of rank 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: When X is integral, the differential-rank condition in smoothness is equivalent to Ω_{X/Y} being locally free of rank n. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, an incomplete proof, or a proper subset as the route for this ID.
Example 10.0.3 — smooth over an algebraically closed field equals regular
Over algebraically closed k, X is smooth of dimension n over Spec k iff X is regular of dimension n; for irreducible separated X this is equivalent to being 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: Over algebraically closed k, X is smooth of dimension n over Spec k iff X is regular of dimension n; for irreducible separated X this is equivalent to being a nonsingular variety. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, an incomplete proof, or a proper subset as the route for this ID.
Proposition 10.1 — stability of smooth morphisms
Open immersions are smooth of relative dimension 0; smoothness and relative dimension are preserved by base change; relative dimensions add under composition and fibre products.
Not formalized. none; no complete checked declaration under strict bundle semantics — As of 2026-09-06, no checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: Open immersions are smooth of relative dimension 0; smoothness and relative dimension are preserved by base change; relative dimensions add under composition and fibre products. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, an incomplete proof, or a proper subset as the route for this ID.
Theorem 10.2 — smoothness via geometrically regular fibres
A finite-type morphism f is smooth of relative dimension n iff f is flat and every geometric fibre is regular and equidimensional of dimension 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: A finite-type morphism f is smooth of relative dimension n iff f is flat and every geometric fibre is regular and equidimensional of dimension n. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, an incomplete proof, or a proper subset as the route for this ID.
Lemma 10.3A — one-element local criterion for flatness
For a local map A→B of noetherian local rings, finite B-module M, and nonunit nonzerodivisor t∈A, M is A-flat iff t is M-regular and M/tM is flat over A/tA.
Not formalized. none; no complete checked declaration 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, finite B-module M, and nonunit nonzerodivisor t∈A, M is A-flat iff t is M-regular and M/tM is flat over A/tA. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, an incomplete proof, or a proper subset as the route for this ID.
Proposition 10.4 — tangent-space criterion for smoothness between nonsingular varieties
For f:X→Y between nonsingular varieties over algebraically closed k and n=dim X−dim Y, the following are equivalent: f smooth of relative dimension n; Ω_{X/Y} locally free rank n; every closed-point tangent map T_xX→T_{f(x)}Y 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 f:X→Y between nonsingular varieties over algebraically closed k and n=dim X−dim Y, the following are equivalent: f smooth of relative dimension n; Ω_{X/Y} locally free rank n; every closed-point tangent map T_xX→T_{f(x)}Y is surjective. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, an incomplete proof, or a proper subset as the route for this ID.
Lemma 10.5 — generic smoothness on the source in characteristic zero
A dominant morphism of integral finite-type schemes over algebraically closed characteristic-zero k is smooth on some nonempty open subset of the source.
Not formalized. none; no complete checked declaration under strict bundle semantics — Pinned generic smooth-locus theorems concern the structural morphism over a perfect field, not an arbitrary dominant morphism X→Y; the full generic-smoothness theorem is unmatched.
Example 10.5.1 — Frobenius is nowhere smooth
In characteristic p, Frobenius P1→P1 has relative dimension 0 but Ω_{X/Y} has rank 1 because d(t^p)=0, so it is nowhere smooth.
Not formalized. none; no complete checked declaration under strict bundle semantics — As of 2026-09-06, no checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: In characteristic p, Frobenius P1→P1 has relative dimension 0 but Ω_{X/Y} has rank 1 because d(t^p)=0, so it is nowhere smooth. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, an incomplete proof, or a proper subset as the route for this ID.
Proposition 10.6 — dimension bound for images of low-rank tangent loci
In characteristic zero, for f:X→Y finite type and X_r the closed points where rank T_{f,x}≤r, one has dim closure(f(X_r))≤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: In characteristic zero, for f:X→Y finite type and X_r the closed points where rank T_{f,x}≤r, one has dim closure(f(X_r))≤r. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, an incomplete proof, or a proper subset as the route for this ID.
Corollary 10.7 — generic smoothness
If f:X→Y is a morphism of varieties over algebraically closed characteristic-zero k with X nonsingular, there is a nonempty open V⊆Y such that f:f^{-1}(V)→V is smooth.
Not formalized. none; no complete checked declaration 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 a morphism of varieties over algebraically closed characteristic-zero k with X nonsingular, there is a nonempty open V⊆Y such that f:f^{-1}(V)→V is smooth. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, an incomplete proof, or a proper subset as the route for this ID.
Definitions — group variety action and homogeneous space
A group variety is a variety with multiplication and inversion inducing a group on k-points; an action is a morphism G×X→X inducing a group homomorphism G(k)→Aut X; a homogeneous space has a transitive G(k)-action.
Not formalized. none; no complete checked declaration 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 group variety is a variety with multiplication and inversion inducing a group on k-points; an action is a morphism G×X→X inducing a group homomorphism G(k)→Aut X; a homogeneous space has a transitive G(k)-action. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, an incomplete proof, or a proper subset as the route for this ID.
Remark 10.7.1 — a group variety acts transitively on itself
Every group variety is a homogeneous space under left multiplication.
Not formalized. none; no complete checked declaration 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 group variety is a homogeneous space under left multiplication. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, an incomplete proof, or a proper subset as the route for this ID.
Example 10.7.2 — projective space is homogeneous under PGL
P^n_k is a homogeneous space under the standard PGL action.
Not formalized. none; no complete checked declaration 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_k is a homogeneous space under the standard PGL action. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, an incomplete proof, or a proper subset as the route for this ID.
Example 10.7.3 — homogeneous spaces are nonsingular
Every homogeneous space over algebraically closed k is nonsingular because a nonempty nonsingular open exists and transitivity transports it to 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: Every homogeneous space over algebraically closed k is nonsingular because a nonempty nonsingular open exists and transitivity transports it to every closed point. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, an incomplete proof, or a proper subset as the route for this ID.
Theorem 10.8 — Kleiman transversality
Let homogeneous X with group G be over algebraically closed characteristic-zero k, and let nonsingular Y,Z map to X. For σ in a nonempty open of G, Y^σ×_X Z is nonsingular and, if nonempty, has dimension dim Y+dim Z−dim 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: Let homogeneous X with group G be over algebraically closed characteristic-zero k, and let nonsingular Y,Z map to X. For σ in a nonempty open of G, Y^σ×_X Z is nonsingular and, if nonempty, has dimension dim Y+dim Z−dim X. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, an incomplete proof, or a proper subset as the route for this ID.
Corollary 10.9 — Bertini for base-point-free systems
On a nonsingular projective variety over algebraically closed characteristic-zero k, a general member of a base-point-free linear system is nonsingular, though it may be reducible.
Not formalized. none; no complete checked declaration 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 nonsingular projective variety over algebraically closed characteristic-zero k, a general member of a base-point-free linear system is nonsingular, though it may be reducible. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, an incomplete proof, or a proper subset as the route for this ID.
Remark 10.9.1 — connectedness makes general members irreducible
If the image of the linear-system map has dimension at least two, later connectedness implies general members are irreducible as well as 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: If the image of the linear-system map has dimension at least two, later connectedness implies general members are irreducible as well as nonsingular. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, an incomplete proof, or a proper subset as the route for this ID.
Remark 10.9.2 — projectivity is unnecessary for finite-dimensional systems
For a finite-dimensional linear system, projectivity of X is unnecessary; with base locus Σ on a projective X, a general member can have singularities only at Σ.
Not formalized. none; no complete checked declaration 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 finite-dimensional linear system, projectivity of X is unnecessary; with base locus Σ on a projective X, a general member can have singularities only at Σ. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, an incomplete proof, or a proper subset as the route for this ID.
Remark 10.9.3 — Bertini can fail in characteristic p
Characteristic-p Frobenius yields a linear system whose every divisor is a point with multiplicity p, showing the characteristic-zero Bertini statement can fail.
Not formalized. none; no complete checked declaration under strict bundle semantics — As of 2026-09-06, no checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: Characteristic-p Frobenius yields a linear system whose every divisor is a point with multiplicity p, showing the characteristic-zero Bertini statement can fail. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, an incomplete proof, or a proper subset as the route for this ID.
Remark 10.9.4 — comparison with the earlier hyperplane Bertini theorem
Hartshorne compares the linear-system Bertini theorem with II.8.18, the earlier hyperplane-section form.
Not formalized. none; no complete checked declaration under strict bundle semantics — As of 2026-09-06, no checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: Hartshorne compares the linear-system Bertini theorem with II.8.18, the earlier hyperplane-section form. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, an incomplete proof, or a proper subset as the route for this ID.
Construction — infinitesimal neighbourhoods of a projective fibre
For projective f:X→Y, coherent F, y∈Y, and n≥1, set X_n=X×Y Spec(O{Y,y}/m_y^n) and F_n=v^*F; X_1 is the fibre and higher X_n are nilpotent thickenings with the same underlying space.
Not formalized. none; no complete checked declaration under strict bundle semantics — Generic fibres, pullbacks and quotient thickenings are formalized separately, but no checked interface packages Hartshorne’s projective-fibre infinitesimal-neighbourhood construction with all clauses.
Construction — completion-to-formal-cohomology comparison map
The base-change maps R^i f_F⊗O_y/m_yn→Hi(X_n,F_n) form inverse systems, yielding a natural map from the completed stalk (R^i f_F)_y^ to lim←H^i(X_n,F_n).
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked formal-functions theorem exists at P or H.
Theorem 11.1 — theorem on formal functions
For projective f:X→Y of noetherian schemes, coherent F, and y∈Y, the natural map (R^i f_*F)_y→lim←Hi(X_n,F_n) is an isomorphism for every i≥0.
Not formalized. none; no complete checked declaration under strict bundle semantics — As of 2026-09-06, no checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: For projective f:X→Y of noetherian schemes, coherent F, and y∈Y, the natural map (R^i f_*F)_y→lim←Hi(X_n,F_n) is an isomorphism for every i≥0. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, an incomplete proof, or a proper subset as the route for this ID.
Remark 11.1.1 — formal functions for proper morphisms
Grothendieck proves the formal-functions theorem 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: Grothendieck proves the formal-functions theorem more generally for proper morphisms. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, an incomplete proof, or a proper subset as the route for this ID.
Remark 11.1.2 — degree-zero formal functions
For i=0 the inverse limit is Γ(X,F) on the formal completion along X_y; for F=O_X it is the ring of formal-regular (holomorphic) functions along the fibre.
Not formalized. none; no complete checked declaration 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 i=0 the inverse limit is Γ(X,F) on the formal completion along X_y; for F=O_X it is the ring of formal-regular (holomorphic) functions along the fibre. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, an incomplete proof, or a proper subset as the route for this ID.
Remark 11.1.3 — cohomology on the formal completion
One can define Hi(X,F^) on the formal scheme and identify it with both quantities in the formal-functions theorem.
Not formalized. none; no complete checked declaration under strict bundle semantics — As of 2026-09-06, no checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: One can define Hi(X,F^) on the formal scheme and identify it with both quantities in the formal-functions theorem. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, an incomplete proof, or a proper subset as the route for this ID.
Corollary 11.2 — higher direct images vanish above fibre dimension
If f:X→Y is projective noetherian and r=max_y dim X_y, then R^i f_*F=0 for every coherent F and i>r.
Not formalized. none; no complete checked declaration under strict bundle semantics — As of 2026-09-06, no checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: If f:X→Y is projective noetherian and r=max_y dim X_y, then R^i f_*F=0 for every coherent F and i>r. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, an incomplete proof, or a proper subset as the route for this ID.
Corollary 11.3 — fOX=OY forces connected fibres
If projective f:X→Y of noetherian schemes satisfies f_*O_X=O_Y, then every fibre f^{-1}(y) is connected.
Not formalized. none; no complete checked declaration under strict bundle semantics — As of 2026-09-06, no checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: If projective f:X→Y of noetherian schemes satisfies f_*O_X=O_Y, then every fibre f^{-1}(y) is connected. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, an incomplete proof, or a proper subset as the route for this ID.
Corollary 11.4 — Zariski Main Theorem, connected-fibre form
If f:X→Y is birational projective between noetherian integral schemes and Y is normal, then every fibre is connected.
Not formalized. none; no complete checked declaration under strict bundle semantics — As of 2026-09-06, no checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: If f:X→Y is birational projective between noetherian integral schemes and Y is normal, then every fibre is connected. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, an incomplete proof, or a proper subset as the route for this ID.
Corollary 11.5 — Stein factorization
Every projective morphism f:X→Y of noetherian schemes factors X→Y′→Y with the first map projective with connected fibres and the second finite; one takes Y′=Spec_Y f_*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: Every projective morphism f:X→Y of noetherian schemes factors X→Y′→Y with the first map projective with connected fibres and the second finite; one takes Y′=Spec_Y f_*O_X. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, an incomplete proof, or a proper subset as the route for this ID.
Definition — fibre-cohomology δ-functors T^i
For noetherian A, projective f:X→Spec A, and coherent F flat over A, define Ti(M)=Hi(X,F⊗_A M) for every A-module M.
Not formalized. none; no complete checked declaration 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, projective f:X→Spec A, and coherent F flat over A, define Ti(M)=Hi(X,F⊗_A M) for every A-module M. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, an incomplete proof, or a proper subset as the route for this ID.
Proposition 12.1 — T^i form a δ-functor
Each T^i is additive and covariant and exact in the middle; together the T^i and cohomological connecting maps form a δ-functor.
Not formalized. none; no complete checked declaration under strict bundle semantics — As of 2026-09-06, no checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: Each T^i is additive and covariant and exact in the middle; together the T^i and cohomological connecting maps form a δ-functor. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, an incomplete proof, or a proper subset as the route for this ID.
Proposition 12.2 — finite free complex representing fibre cohomology
There exists a bounded-above complex L^• of finitely generated free A-modules such that Ti(M)≅hi(L^•⊗_A M) naturally for every A-module M and all i, compatibly as δ-functors.
Not formalized. none; no complete checked declaration under strict bundle semantics — As of 2026-09-06, no checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: There exists a bounded-above complex L^• of finitely generated free A-modules such that Ti(M)≅hi(L^•⊗_A M) naturally for every A-module M and all i, compatibly as δ-functors. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, an incomplete proof, or a proper subset as the route for this ID.
Lemma 12.3 — finite free replacement of a flat complex
A bounded-above complex C^• with finite cohomology admits a bounded-above finite-free complex L^• quasi-isomorphic to it; if every C^i is flat, tensoring with any module preserves the induced cohomology isomorphisms.
Not formalized. none; no complete checked declaration 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 bounded-above complex C^• with finite cohomology admits a bounded-above finite-free complex L^• quasi-isomorphic to it; if every C^i is flat, tensoring with any module preserves the induced cohomology isomorphisms. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, an incomplete proof, or a proper subset as the route for this ID.
Construction — W^i of the representing complex
For a complex N^• set Wi(N)=coker(d{i−1}:N{i−1}→Ni); then 0→hi(N)→Wi(N)→N^{i+1} is exact. For §12 write Wi=Wi(L^•).
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked semicontinuity/cohomology-base-change complex theorem matching Hartshorne’s setup was found.
Proposition 12.4 — characterization of left exact T^i
The following are equivalent: T^i is left exact; W^i is projective over A; and there is a finite A-module Q such that T^i(M)≅Hom_A(Q,M) naturally for all M.
Not formalized. none; no complete checked declaration 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 following are equivalent: T^i is left exact; W^i is projective over A; and there is a finite A-module Q such that T^i(M)≅Hom_A(Q,M) naturally for all M. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, an incomplete proof, or a proper subset as the route for this ID.
Remark 12.4.1 — finite representability is stronger than abstract Hom-representability
A left-exact functor on A-modules commuting with direct sums is Hom(Q,−) for some Q, but Q need not be finite even if the functor preserves finite generation; Proposition 12.4 supplies a finite Q here.
Not formalized. none; no complete checked declaration 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 left-exact functor on A-modules commuting with direct sums is Hom(Q,−) for some Q, but Q need not be finite even if the functor preserves finite generation; Proposition 12.4 supplies a finite Q here. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, an incomplete proof, or a proper subset as the route for this ID.
Proposition 12.5 — characterization of right exact T^i
There is a natural φ_M:Ti(A)⊗M→Ti(M); T^i is right exact iff φ_M is an isomorphism for every M, equivalently iff φ_M is surjective for every M.
Not formalized. none; no complete checked declaration under strict bundle semantics — As of 2026-09-06, no checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: There is a natural φ_M:Ti(A)⊗M→Ti(M); T^i is right exact iff φ_M is an isomorphism for every M, equivalently iff φ_M is surjective for every M. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, an incomplete proof, or a proper subset as the route for this ID.
Corollary 12.6 — characterization of exact T^i
T^i is exact iff it is right exact and the finite A-module T^i(A) 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: T^i is exact iff it is right exact and the finite A-module T^i(A) is projective. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, an incomplete proof, or a proper subset as the route for this ID.
Construction — local functors Ty^i
For y↔︎p∈Spec A, restrict T^i to A_p-modules, equivalently use L_p^•; flat base change identifies this with the T^i functor for X×Y Spec O{Y,y}→Spec O_{Y,y}.
Not formalized. none; no complete checked declaration under strict bundle semantics — As of 2026-09-06, no checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: For y↔︎p∈Spec A, restrict T^i to A_p-modules, equivalently use L_p^•; flat base change identifies this with the T^i functor for X×Y Spec O{Y,y}→Spec O_{Y,y}. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, an incomplete proof, or a proper subset as the route for this ID.
Proposition 12.7 — exactness properties are open on the base
If T^i is left exact, right exact, or exact at y_0∈Y, the same property holds at every point in some open neighborhood of 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: If T^i is left exact, right exact, or exact at y_0∈Y, the same property holds at every point in some open neighborhood of y_0. Strict bundle semantics reject a specialization, one clause/example of a bundled row, an unbridged analogue, an incomplete proof, or a proper subset as the route for this ID.
Definition — upper semicontinuous integer-valued function
A function φ:Y→Z is upper semicontinuous when near every y its values are ≤φ(y); equivalently, each locus {y:φ(y)≥n} is closed.
Formalized. Mathlib/Topology/Semicontinuity/Defs.lean::UpperSemicontinuous; Mathlib/Topology/Semicontinuity/Basic.lean::upperSemicontinuous_iff_isClosed_preimage — Pinned Mathlib realizes the complete source interface: A function φ:Y→Z is upper semicontinuous when near every y its values are ≤φ(y); equivalently, each locus {y:φ(y)≥n} is closed.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d
Remark 12.7.1 — closed-level-set criterion for upper semicontinuity
An integer-valued function is upper semicontinuous iff every superlevel set {y∈Y:φ(y)≥n} is closed.
Formalized. Mathlib/Topology/Semicontinuity/Basic.lean::upperSemicontinuous_iff_isClosed_preimage — Pinned Mathlib realizes the complete source interface: An integer-valued function is upper semicontinuous iff every superlevel set {y∈Y:φ(y)≥n} is closed.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d
Example 12.7.2 — fibre dimension of a coherent sheaf is upper semicontinuous
For coherent F on a noetherian scheme Y, y↦dim_{k(y)}(F⊗k(y)), equivalently the minimal number of generators of F_y, is upper semicontinuous.
Not formalized. none; no complete checked declaration under strict bundle semantics — Generic upper semicontinuity is formalized, but the coherent-sheaf fibre-dimension theorem is not.
Theorem 12.8 — semicontinuity theorem
For projective f:X→Y of noetherian schemes and coherent F flat over Y, hi(y,F)=dim_{k(y)}Hi(X_y,F_y) is upper semicontinuous on Y for every i≥0.
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked proper-flat Euler-characteristic constancy theorem was found.
Corollary 12.9 — Grauert theorem under constant fibre cohomology
If additionally Y is integral and h^i(y,F) is constant, then R^i f_F is locally free and the natural map R^i f_F⊗k(y)→H^i(X_y,F_y) is an isomorphism for every y.
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked Hilbert-polynomial constancy theorem for flat projective families was found.
Example 12.9.1 — flat integral curves have constant h^0 and h^1
For a flat family of integral projective curves over algebraically closed k, h^0(O)=1 and constancy of arithmetic genus forces h^1(O) to be constant as well.
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked cohomology-and-base-change theorem was found.
Example 12.9.2 — fibre cohomology jumps at an embedded-point degeneration
In Example 9.8.4, both h^0 and h^1 of O jump upward at the special fibre because of the embedded nilpotent structure and the cubic reduced support.
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked Grauert/base-change local-freeness theorem was found.
Example 12.9.3 — constancy in smooth complex projective families
For an algebraic family of nonsingular projective varieties over C, all h^i(O_{X_t}) are constant; Hartshorne notes this uses degeneration of the Hodge spectral sequence.
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked cohomology/base-change surjectivity criterion was found.
Proposition 12.10 — fibrewise surjectivity implies local right exactness
If for some i,y the natural Ti(A)⊗k(y)→Ti(k(y)) is surjective, then T^i is right exact at y; the converse follows from Proposition 12.5.
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked Stein-factorization theorem was found.
Theorem 12.11 — cohomology and base change
For projective f:X→Y noetherian and coherent F flat over Y: if φi(y):Ri f_F⊗k(y)→H^i(X_y,F_y) is surjective, it is an isomorphism and remains so near y; assuming this, φ^{i−1}(y) is surjective iff R^i f_F is locally free near y.
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked connected-fibres/open-and-closed consequence from Stein factorization was found.