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 morphisms
Definition
A morphism is quasi-compact if is quasi-compact for every quasi-compact open . It is quasi-separated if, for affine opens lying over a common affine open of , the intersection is quasi-compact. This affine criterion is the definition used here, before the diagonal construction is available.
Depends on
Used by
- Euler characteristic in a proper flat family is locally constant Corollary
- The affine line with doubled origin is not separated Corollary
- Upper semicontinuity of fibre cohomology dimensions Corollary
- An infinite disjoint union is locally but not globally finite type Counterexample
- Global generation does not imply very ampleness Counterexample
- Quasi-separatedness in pushforward cannot be omitted Counterexample
- Fpqc covering morphisms Definition
- Quasi-projective morphisms before Proj Definition
- Relative ampleness over an arbitrary base Definition
- Relative very ampleness in the finite projective-space convention Definition
- Separated morphism of schemes Definition
- The empty morphism is finite, proper and projective Example
- A quasi-compact image stable under specialization is closed Lemma
- A quasi-compact immersion with nonclosed image has a boundary specialization Lemma
- Chow lemma for proper Noetherian schemes Lemma
- Closed gluing of two projective three-spaces is proper Lemma
- Composite of a finite morphism and a proper morphism is proper Lemma
- Constructible subsets stable under generalisation are open in an affine spectrum Lemma
- Eventual generation of coherent projective twists Lemma
- Finite projective complex for proper flat coherent cohomology Lemma
- Finite-stage descent of finitely presented schemes and their morphisms Lemma
- Flat field extension commutes with coherent cohomology Lemma
- Fpqc covers are universally submersive Lemma
- Fpqc descent of properness components Lemma
- Higher direct images localize over an affine base Lemma
- Noetherian approximation of proper flat finitely presented sheaf data Lemma
- Projective space is of finite type over its base Lemma
- Properness survives composition Lemma
- Quasi-compactness is local on the target and survives base change Lemma
- Quasi-separatedness and the diagonal Lemma
- Relative very ampleness implies relative ampleness Lemma
- Schematic closure and agreement on a dense open Lemma
- SNC projective compactifications of smooth quasiprojective varieties Lemma
- Structure sheaf of a quasi-compact quasi-separated morphism is affine-local Lemma
- The product of two projective lines is an integral smooth projective surface Lemma
- Torsors under the additive group over an affine scheme are trivial Lemma
- Valuation lifts detect universal closedness Lemma
- Cohomology and base change for proper flat coherent families Theorem
- Finite coherent cohomology for proper schemes Theorem
- Generic flatness for finite type morphisms over Noetherian integral bases Theorem
…and 5 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, Section 19 (standard reference, not scraped)