LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedjudge pass (gpt-5.6-terra)audited 2026-09-07

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.

Quasi-compactness is local on the target and survives base change

Statement

For $f : X \to S$ , the following are equivalent: $f$ is quasi-compact; the inverse image of every affine open in $S$ is quasi-compact; some affine open cover of $S$ has quasi-compact inverse images. Moreover any arbitrary base change of a quasi-compact morphism is quasi-compact.

Facts & Assumptions

Given: The objects, hypotheses and conventions in the statement above.

[F1]

A morphism $f : X \to S$ is quasi-compact if $f^{- 1} (V)$ is quasi-compact for every quasi-compact open $V \subseteq S$ . It is quasi-separated if, for affine opens $U, U^{'} \subseteq X$ lying over a common affine open of $S$ , the intersection $U \cap U^{'}$ is quasi-compact. This affine criterion is the definition used here, before the diagonal construction is available. (Quasi-compact and quasi-separated morphisms)

[F2]

Every affine scheme is quasi-compact. (Every affine scheme is quasi-compact)

[F3]

Every diagram $X \to S \leftarrow Y$ of schemes has a fibre product. Given an affine cover $S = ⋃_{i} Spec A_{i}$ and affine covers $f^{- 1} (Spec A_{i}) = ⋃_{j} Spec B_{i j}$ and $g^{- 1} (Spec A_{i}) = ⋃_{k} Spec C_{i k}$ , the product has open affine cover $Spec (B_{i j} \otimes_{A_{i}} C_{i k}) .$ (Existence of all scheme fibre products)

Proof

1.1

By F1 and F2, quasi-compactness of $f$ implies the condition for every affine open, which implies the condition for any chosen affine cover. Suppose conversely that $S = ⋃ U_{i}$ is such a cover. For an arbitrary affine open $V \subset S$ , principal opens in the $U_{i}$ contained in $V$ cover $V$ . By F2 choose finitely many of them, say $W_{1}, \dots, W_{n}$ .

givenF1F2

2.1

For each $W_{j} = D_{U_{i}} (a)$ take a finite affine cover of the quasi-compact $f^{- 1} (U_{i})$ . Its intersection with $f^{- 1} (W_{j})$ is principal in each affine chart, being the nonvanishing locus of the image of $a$ , and is affine. Hence $f^{- 1} (W_{j})$ , and then $f^{- 1} (V)$ , is a finite union of affines, thus quasi-compact by F2. Every quasi-compact open of $S$ has a finite affine cover; its inverse image is consequently quasi-compact. This is exactly F1.

F1F2step 1.1

3.1

For $S^{'} \to S$ , cover $S^{'}$ by affines $V^{'}$ mapping into affines $U \subset S$ . A finite affine cover of $f^{- 1} (U)$ pulls back by F3 to a finite affine cover of the inverse image of $V^{'}$ . It is quasi-compact by F2. The criterion just proved gives quasi-compactness of the base-changed morphism. Empty covers, zero coordinate rings, and singleton covers are included. Composition of quasi-compact morphisms also follows directly from F1: pull back a quasi-compact open first by the second morphism and then by the first; both successive inverse images are quasi-compact.

F2F3step 2.1∎

Depends on

Used by

Dependency tree · two levels

10 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

Stacks 26.19.2–3 (standard reference, not scraped)