Alphabeta MathHow 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.
Quasi-compact and quasi-separated schemes
Definition
A scheme is quasi-compact if is quasi-compact. It is quasi-separated if the intersection of every two affine open subschemes is quasi-compact. These conditions are properties of the indicated underlying open covers; they do not mean that is separated.
Depends on
Used by
- Global generation does not imply very ampleness Counterexample
- Quasi-separatedness in pushforward cannot be omitted Counterexample
- Absolute ampleness by affine section opens Definition
- Constructible subsets of a scheme Definition
- Quasi-compact and quasi-separated morphisms Definition
- The cotangent complex of a morphism of schemes Definition
- A quasi-compact image stable under specialization is closed Lemma
- A quasi-compact immersion with nonclosed image has a boundary specialization Lemma
- Affine neighbourhood containing component generic points Lemma
- Blowups of integral projective complex schemes are projective Lemma
- Chow lemma for proper Noetherian schemes Lemma
- Closed gluing of two projective three-spaces is proper Lemma
- Constructible subsets stable under generalisation are open in an affine spectrum Lemma
- Extend a quasi-coherent section after multiplying by a power Lemma
- Finite projective complex for proper flat coherent cohomology Lemma
- Finite type is affine-local on source and target Lemma
- Finite-stage descent of finitely presented schemes and their morphisms Lemma
- Fpqc covers are universally submersive Lemma
- Fpqc descent of properness components Lemma
- High-degree section module is finite graded Lemma
- Integral quasi-coherent algebras over qcqs bases are unions of finite subalgebras Lemma
- Pushforward and vanishing for an affine point blowup Lemma
- Quasi-separatedness and the diagonal Lemma
- The quotient by a maximal line subbundle is locally free Lemma
- Affine schemes are quasi-separated Theorem
- Coherent higher direct images under proper morphisms Theorem
- Finite coherent cohomology for proper schemes Theorem
- High powers of an ample line bundle embed a proper scheme Theorem
- Projective n-space has quasi-coherent cohomological dimension at most n Theorem
- Quasi-coherence of pushforward for qcqs morphisms Theorem
- Serre global-generation criterion for ampleness Theorem
Dependency tree · two levels
4 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, Section 19 (standard reference, not scraped)