Quasi-compact morphisms

A morphism is quasi-compact if its restrictions to the members of a finite open cover of its source are quasi-compact. This allows quasi-compact morphisms to be glued along open subschemes. Finiteness is essential: an infinite union of quasi-compact pieces need not be quasi-compact.

Every point of the target of a quasi-compact morphism of schemes has an open neighbourhood whose preimage is quasi-compact (Scheme.Hom.exists_isOpen_mem_isCompact_preimage): an affine open neighbourhood will do.

A morphism of S-schemes from a scheme with quasi-compact structure map to one with quasi-separated structure map is quasi-compact (AlgebraicGeometry.quasiCompact_left_of_quasiCompact_hom).

theorem AlgebraicGeometry.QuasiCompact.of_openCover {X Y : Scheme} (f : X ⟶ Y) (𝒰 : X.OpenCover) [Finite 𝒰.I₀] (H : ∀ (i : 𝒰.I₀), QuasiCompact (CategoryTheory.CategoryStruct.comp (𝒰.f i) f)) : QuasiCompact f

A morphism is quasi-compact if its restrictions to a finite open cover of the source are quasi-compact.

theorem AlgebraicGeometry.Scheme.Hom.exists_isOpen_mem_isCompact_preimage {X Y : Scheme} (f : X ⟶ Y) [QuasiCompact f] (y : ↥Y) : ∃ (U : Set ↥Y), IsOpen U ∧ y ∈ U ∧ IsCompact (⇑f ⁻¹' U)

Every point of the target of a quasi-compact morphism has an open neighbourhood, for instance an affine one, whose preimage is quasi-compact.

theorem AlgebraicGeometry.quasiCompact_left_of_quasiCompact_hom {S : Scheme} {T U : CategoryTheory.Over S} (f : T ⟶ U) [QuasiCompact T.hom] [QuasiSeparated U.hom] : QuasiCompact (CategoryTheory.Over.Hom.left f)

A morphism of S-schemes from a scheme with quasi-compact structure map to one with quasi-separated structure map has quasi-compact underlying map.