How statement and proof provenance work
The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.
- Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
- AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
- AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.
These labels describe origin, not correctness: citations and verification chips remain separate evidence.
Affine open subschemes
Definition
For a scheme and an open set , the open subscheme means . It is an affine open subscheme when this restricted locally ringed space is affine; thus “affine open” always includes its restricted structure sheaf, not merely an open subset of .
Depends on
Used by
- Euler characteristic in a proper flat family is locally constant Corollary
- Generic smoothness on the source Corollary
- Upper semicontinuity of fibre cohomology dimensions Corollary
- Affine morphisms Definition
- Affine-overlap separation condition Definition
- Integral schemes Definition
- Locally factorial scheme Definition
- Locally finite presentation morphisms Definition
- Locally finite type and finite type morphisms Definition
- Locally Noetherian and Noetherian schemes Definition
- Open immersions of schemes Definition
- Quasi-coherent ideal sheaves Definition
- Quasi-compact and quasi-separated morphisms Definition
- Quasi-compact and quasi-separated schemes Definition
- Regular points of locally Noetherian schemes Definition
- Two-affine projective line and its twists Definition
- Weil divisor normal noetherian scheme Definition
- A line-bundle section cuts an affine open inside an affine scheme Lemma
- A quasi-compact image stable under specialization is closed Lemma
- A regular point lies on one irreducible component Lemma
- Affine finite-type source immerses into relative projective space Lemma
- Affine neighbourhood containing component generic points Lemma
- An associated sheaf restricts to an associated sheaf on an affine open Lemma
- Chow lemma for proper Noetherian schemes Lemma
- Differentials, open restriction, and the chain rule Lemma
- Finite projective complex for proper flat coherent cohomology Lemma
- Flat field extension commutes with coherent cohomology Lemma
- Fpqc descent of properness components Lemma
- Intersections of affine opens admit principal affine covers Lemma
- Morphisms of schemes are local on compatible open covers Lemma
- Schematic closure and agreement on a dense open Lemma
- Tangent vectors at rational points are dual-number points Lemma
- Universal finite projective cohomology complex over any base Lemma
- Valuation lifts detect universal closedness Lemma
- Cohomology and base change for proper flat coherent families Theorem
- Dense regular loci on every component Theorem
- Finite coherent cohomology for proper schemes Theorem
- Generic smoothness over a dense target open Theorem
- Normalization of an integral finite-type curve by gluing affine integral closures Theorem
- Openness of the regular locus over a perfect field Theorem
…and 8 more results.
Dependency tree · two levels
6 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.
Sources
- The Stacks Project, Schemes, Definition 9.1 and Lemma 9.2 (standard reference, not scraped)