# 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 (quasiCompact_iff_forall_affine).

theorem AlgebraicGeometry.quasiCompact_iff (f : X Y) :
∀ (U : Set Y.toPresheafedSpace), IsCompact (f.val.base ⁻¹' U)

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.

• isCompact_preimage : ∀ (U : Set Y.toPresheafedSpace), IsCompact (f.val.base ⁻¹' U)

Preimage of compact open set under a quasi-compact morphism between schemes is compact.

Instances
theorem AlgebraicGeometry.QuasiCompact.isCompact_preimage {f : X Y} [self : ] (U : Set Y.toPresheafedSpace) :
IsCompact (f.val.base ⁻¹' U)

Preimage of compact open set under a quasi-compact morphism between schemes is compact.

The AffineTargetMorphismProperty corresponding to QuasiCompact, asserting that the domain is a quasi-compact scheme.

Equations
Instances For
@[instance 900]
Equations
• =
instance AlgebraicGeometry.quasiCompactComp (f : X Y) (g : Y Z) :
Equations
• =
theorem AlgebraicGeometry.isCompact_open_iff_eq_finset_affine_union (U : Set X.toPresheafedSpace) :
∃ (s : Set X.affineOpens), s.Finite U = is, i
theorem AlgebraicGeometry.isCompact_open_iff_eq_basicOpen_union (U : Set X.toPresheafedSpace) :
∃ (s : Set (X.presheaf.obj { unop := })), s.Finite U = is, (X.basicOpen i)
theorem AlgebraicGeometry.quasiCompact_iff_forall_affine (f : X Y) :
∀ (U : TopologicalSpace.Opens Y.toPresheafedSpace), IsCompact (f.val.base ⁻¹' U)
@[simp]
theorem AlgebraicGeometry.QuasiCompact.affineProperty_toProperty (f : X Y) :
f CompactSpace X.toPresheafedSpace
theorem AlgebraicGeometry.isCompact_basicOpen {U : TopologicalSpace.Opens X.toPresheafedSpace} (hU : ) (f : (X.presheaf.obj { unop := U })) :
IsCompact (X.basicOpen f)
theorem AlgebraicGeometry.QuasiCompact.affine_openCover_tfae (f : X Y) :
[, ∃ (𝒰 : Y.OpenCover) (_ : ∀ (i : 𝒰.J), AlgebraicGeometry.IsAffine (𝒰.obj i)), ∀ (i : 𝒰.J), CompactSpace (CategoryTheory.Limits.pullback f (𝒰.map i)).toPresheafedSpace, ∀ (𝒰 : Y.OpenCover) [inst : ∀ (i : 𝒰.J), AlgebraicGeometry.IsAffine (𝒰.obj i)] (i : 𝒰.J), CompactSpace (CategoryTheory.Limits.pullback f (𝒰.map i)).toPresheafedSpace, ∀ {U : AlgebraicGeometry.Scheme} (g : U Y) [inst : ] [inst : ], CompactSpace .toPresheafedSpace, ∃ (ι : Type u) (U : ιTopologicalSpace.Opens Y.toPresheafedSpace) (_ : iSup U = ) (_ : ∀ (i : ι), ), ∀ (i : ι), CompactSpace (f.val.base ⁻¹' (U i).carrier)].TFAE
theorem AlgebraicGeometry.QuasiCompact.openCover_tfae (f : X Y) :
[, ∃ (𝒰 : Y.OpenCover), ∀ (i : 𝒰.J), AlgebraicGeometry.QuasiCompact CategoryTheory.Limits.pullback.snd, ∀ (𝒰 : Y.OpenCover) (i : 𝒰.J), AlgebraicGeometry.QuasiCompact CategoryTheory.Limits.pullback.snd, ∀ (U : TopologicalSpace.Opens Y.toPresheafedSpace), , ∀ {U : AlgebraicGeometry.Scheme} (g : U Y) [inst : ], AlgebraicGeometry.QuasiCompact CategoryTheory.Limits.pullback.snd, ∃ (ι : Type u) (U : ιTopologicalSpace.Opens Y.toPresheafedSpace) (_ : iSup U = ), ∀ (i : ι), AlgebraicGeometry.QuasiCompact (f ∣_ U i)].TFAE
theorem AlgebraicGeometry.quasiCompact_over_affine_iff (f : X Y) :
CompactSpace X.toPresheafedSpace
theorem AlgebraicGeometry.QuasiCompact.affine_openCover_iff (𝒰 : Y.OpenCover) [∀ (i : 𝒰.J), AlgebraicGeometry.IsAffine (𝒰.obj i)] (f : X Y) :
∀ (i : 𝒰.J), CompactSpace (CategoryTheory.Limits.pullback f (𝒰.map i)).toPresheafedSpace
theorem AlgebraicGeometry.QuasiCompact.openCover_iff (𝒰 : Y.OpenCover) (f : X Y) :
∀ (i : 𝒰.J), AlgebraicGeometry.QuasiCompact CategoryTheory.Limits.pullback.snd
instance AlgebraicGeometry.instQuasiCompactFstScheme (f : X Z) (g : Y Z) :
AlgebraicGeometry.QuasiCompact CategoryTheory.Limits.pullback.fst
Equations
• =
instance AlgebraicGeometry.instQuasiCompactSndScheme (f : X Z) (g : Y Z) :
AlgebraicGeometry.QuasiCompact CategoryTheory.Limits.pullback.snd
Equations
• =
theorem AlgebraicGeometry.compact_open_induction_on {P : TopologicalSpace.Opens X.toPresheafedSpaceProp} (S : TopologicalSpace.Opens X.toPresheafedSpace) (hS : IsCompact S.carrier) (h₁ : P ) (h₂ : ∀ (S : TopologicalSpace.Opens X.toPresheafedSpace), IsCompact S.carrier∀ (U : X.affineOpens), P SP (S U)) :
P S
theorem AlgebraicGeometry.exists_pow_mul_eq_zero_of_res_basicOpen_eq_zero_of_isAffineOpen {U : TopologicalSpace.Opens X.toPresheafedSpace} (hU : ) (x : (X.presheaf.obj { unop := U })) (f : (X.presheaf.obj { unop := U })) (H : TopCat.Presheaf.restrictOpen x (X.basicOpen f) = 0) :
∃ (n : ), f ^ n * x = 0
theorem AlgebraicGeometry.exists_pow_mul_eq_zero_of_res_basicOpen_eq_zero_of_isCompact {U : TopologicalSpace.Opens X.toPresheafedSpace} (hU : IsCompact U.carrier) (x : (X.presheaf.obj { unop := U })) (f : (X.presheaf.obj { unop := U })) (H : TopCat.Presheaf.restrictOpen x (X.basicOpen f) = 0) :
∃ (n : ), f ^ n * x = 0

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.