Included proof routes and precise boundaries

Course contents

These exact earlier lesson sources accompany the selected lessons. Each consuming text retains its required hypotheses and result locators.

Exact supporting proofs

• Stacks 00P4: full selected statement and proof, editable source and GNU FDL notice.
• Stacks 0564: full selected statement and proof, editable source and GNU FDL notice.
• Stacks 00PY: full selected statement and proof, editable source and GNU FDL notice.
• Stacks 00Q2: full selected statement and proof, editable source and GNU FDL notice.

Lesson boundaries

AG-FSE-03. Sections 1–5 and Proposition 6.1 supply the written unramifiedness and universally-injective monomorphism results used by the selected lessons. The full lesson is supplementary: Theorem 6.2 still requires the stronger finite-morphism criterion (02LS) and scheme-level relative integral completion (03GW). Those proofs are not supplied by the included algebraic Zariski Main result.

AG-FSE-06. Lemma 1.1, Section 5 (including Theorem 5.3) and Lemma 6.1 supply the written lifting, thickening-equivalence and one-square-presentation results used by AG-FSE-07. The full lesson is supplementary: unrestricted formal-smoothness locality in Section 3 needs arbitrary-rank projectivity descent (05A9), not finite-projectivity descent. The named quasi-coherent and cohomological prerequisites of its broader arguments are outside this collection.

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.