Included proof routes and precise boundaries

The finite-type approximation used by AG-FSE-06 is proved in the algebraic-spaces course; affine cohomology is proved in AG-QC. See the exact programme proof links below. These providers are not bundled in this selected download.

Limits of schemes and Noetherian approximation

Read the included lesson and its editable source. Used in AG-FSE-06.

Henselian local rings and henselization

Read the included lesson and its editable source. Used in AG-FSE-07.

Descending properties of schemes and morphisms

Read the included lesson and its editable source. Used in AG-FSE-07.

Exact supporting proofs

Stacks 00P4: full statement and independent CC0 proof, with editable programme source and exact proof-provider links.
Stacks 0564: full statement and independent CC0 proof, with editable programme source and exact proof-provider links.
Stacks 00PY: full statement and independent CC0 proof, with editable programme source and exact proof-provider links.
Stacks 00Q2: full statement and independent CC0 proof, with editable programme source and exact proof-provider links.

Further programme proof providers

Arbitrary-rank projectivity descent · Exact source edition
Stronger finite-fibre finiteness criterion · Exact source edition
Finite-type quasi-coherent approximation · Exact source edition
Affine-limit criterion · Exact source edition
Affine vanishing, Theorem 2.2 · Exact source edition
Serre criterion, Theorem 5.2 · Exact source edition
Relative integral completion, Theorem D5.2 · Exact source edition

These links identify existing programme proofs. Providers outside the selected download require access to their separate course or exact source edition. No full recursive proof-closure claim is made.

Lesson boundaries

AG-FSE-03. Sections 1–5 and Proposition 6.1 supply the unramifiedness and universally-injective monomorphism results used by the selected lessons. The full lesson also uses the stronger finite-morphism criterion (02LS), proved in AG-AS, and scheme-level relative integral completion (03GW), proved in AG-RG-S04 and used by AG-MO-12. These exact programme proofs are linked from the lesson. Some providers are outside this selected offline collection; the supplementary classification is a packaging boundary, not a claim that those proofs are unwritten.

AG-FSE-06. Lemma 1.1, Section 5 (including Theorem 5.3) and Lemma 6.1 supply the lifting, thickening-equivalence and one-square-presentation results used by AG-FSE-07. The full lesson uses arbitrary-rank projectivity descent (05A9), finite-type quasi-coherent approximation and the affine-limit criterion in AG-AS, and affine vanishing and Serre’s criterion in AG-QC. Their exact proofs are linked from the lesson. These providers are outside this selected offline collection; the supplementary classification does not assert missing proof writing.

AG-FSE-04 uses preliminary AG-CA-17 results through Lemma 7.5 and AG-CA-18 flatness. Its own Theorem 3.1 supplies the later AG-CA-17 Theorem 7.6; that later theorem is not its prerequisite.

The field-extension result 00P4 concerns neighbourhood dimension at a point. AG-CA-11 Theorem 5.1 concerns local-ring dimension. The 0564 module criterion applies with M=S. These finite inclusions do not assert recursive closure of every further source reference.