# mathlib3documentation

algebraic_geometry.morphisms.quasi_compact

# Quasi-compact morphisms #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 (quasi_compact_iff_forall_affine).

@[class]
structure algebraic_geometry.quasi_compact {X Y : algebraic_geometry.Scheme} (f : X Y) :
Prop

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.

Instances of this typeclass

The affine_target_morphism_property corresponding to quasi_compact, asserting that the domain is a quasi-compact scheme.

Equations
@[protected, instance]
@[protected, instance]
@[simp]
theorem algebraic_geometry.quasi_compact.affine_open_cover_tfae {X Y : algebraic_geometry.Scheme} (f : X Y) :
[, (𝒰 : Y.open_cover) [_inst_1 : (i : 𝒰.J), , , (𝒰 : Y.open_cover) [_inst_2 : (i : 𝒰.J), (i : 𝒰.J), , {U : algebraic_geometry.Scheme} (g : U Y) [_inst_3 : [_inst_4 : , , {ι : Type u} (U : (hU : supr U = ) (hU' : (i : ι), , (i : ι), compact_space ((f.val.base) ⁻¹' (U i).carrier)].tfae
theorem algebraic_geometry.quasi_compact.open_cover_tfae {X Y : algebraic_geometry.Scheme} (f : X Y) :
[, , , , , {ι : Type u} (U : (hU : supr U = ), (i : ι), algebraic_geometry.quasi_compact (f ∣_ U i)].tfae
@[protected, instance]
@[protected, instance]
theorem algebraic_geometry.compact_open_induction_on (hS : is_compact S.carrier) (h₁ : P ) (h₂ : (S : , (U : (X.affine_opens)), P S P (S U)) :
P S

If 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 n.