Quasi-compact morphisms #
A morphism of schemes is quasi-compact if the preimages of quasi-compact open sets are quasi-compact.
It suffices to check that preimages of affine open sets are compact
- isCompact_preimage : ∀ (U : Set ↑↑Y.toPresheafedSpace), IsOpen U → IsCompact U → IsCompact (↑f.val.base ⁻¹' U)
Preimage of compact open set under a quasi-compact morphism between schemes is compact.
A morphism is "quasi-compact" if the underlying map of topological spaces is, i.e. if the preimages of quasi-compact open sets are quasi-compact.
x : Γ(X, U) is zero on
D(f) for some
f : Γ(X, U), and
U is quasi-compact, then
f ^ n * x = 0 for some