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 {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) : AlgebraicGeometry.QuasiCompact f ↔ ∀ (U : Set ↑↑Y.toPresheafedSpace), IsOpen U → IsCompact U → IsCompact (↑f.val.base ⁻¹' U)

class AlgebraicGeometry.QuasiCompact {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) : Prop

• 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.

theorem AlgebraicGeometry.quasiCompact_iff_spectral {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) : AlgebraicGeometry.QuasiCompact f ↔ IsSpectralMap ↑f.val.base

def AlgebraicGeometry.QuasiCompact.affineProperty : AlgebraicGeometry.AffineTargetMorphismProperty

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

instance AlgebraicGeometry.quasiCompactOfIsIso {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [CategoryTheory.IsIso f] : AlgebraicGeometry.QuasiCompact f

instance AlgebraicGeometry.quasiCompactComp {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} {Z : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (g : Y ⟶ Z) [AlgebraicGeometry.QuasiCompact f] [AlgebraicGeometry.QuasiCompact g] : AlgebraicGeometry.QuasiCompact (CategoryTheory.CategoryStruct.comp f g)

theorem AlgebraicGeometry.isCompact_open_iff_eq_finset_affine_union {X : AlgebraicGeometry.Scheme} (U : Set ↑↑X.toPresheafedSpace) : IsCompact U ∧ IsOpen U ↔ ∃ s, Set.Finite s ∧ U = ⋃ (i : ↑(AlgebraicGeometry.Scheme.affineOpens X)) (_ : i ∈ s), ↑↑i

theorem AlgebraicGeometry.isCompact_open_iff_eq_basicOpen_union {X : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsAffine X] (U : Set ↑↑X.toPresheafedSpace) : IsCompact U ∧ IsOpen U ↔ ∃ s, Set.Finite s ∧ U = ⋃ (i : ↑(X.presheaf.obj (Opposite.op ⊤))) (_ : i ∈ s), ↑(AlgebraicGeometry.Scheme.basicOpen X i)

theorem AlgebraicGeometry.quasiCompact_iff_forall_affine {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) : AlgebraicGeometry.QuasiCompact f ↔ ∀ (U : TopologicalSpace.Opens ↑↑Y.toPresheafedSpace), AlgebraicGeometry.IsAffineOpen U → IsCompact (↑f.val.base ⁻¹' ↑U)

@[simp]

theorem AlgebraicGeometry.QuasiCompact.affineProperty_toProperty {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) : AlgebraicGeometry.AffineTargetMorphismProperty.toProperty AlgebraicGeometry.QuasiCompact.affineProperty f ↔ AlgebraicGeometry.IsAffine Y ∧ CompactSpace ↑↑X.toPresheafedSpace

theorem AlgebraicGeometry.quasiCompact_iff_affineProperty {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) : AlgebraicGeometry.QuasiCompact f ↔ AlgebraicGeometry.targetAffineLocally AlgebraicGeometry.QuasiCompact.affineProperty f

theorem AlgebraicGeometry.quasiCompact_eq_affineProperty : @AlgebraicGeometry.QuasiCompact = AlgebraicGeometry.targetAffineLocally AlgebraicGeometry.QuasiCompact.affineProperty

theorem AlgebraicGeometry.isCompact_basicOpen (X : AlgebraicGeometry.Scheme) {U : TopologicalSpace.Opens ↑↑X.toPresheafedSpace} (hU : IsCompact ↑U) (f : ↑(X.presheaf.obj (Opposite.op U))) : IsCompact ↑(AlgebraicGeometry.Scheme.basicOpen X f)

theorem AlgebraicGeometry.QuasiCompact.affineProperty_isLocal : AlgebraicGeometry.AffineTargetMorphismProperty.IsLocal AlgebraicGeometry.QuasiCompact.affineProperty

theorem AlgebraicGeometry.QuasiCompact.affine_openCover_tfae {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) : List.TFAE [AlgebraicGeometry.QuasiCompact f, ∃ 𝒰 x, ∀ (i : 𝒰.J), CompactSpace ↑↑(CategoryTheory.Limits.pullback f (AlgebraicGeometry.Scheme.OpenCover.map 𝒰 i)).toLocallyRingedSpace.toSheafedSpace.toPresheafedSpace, ∀ (𝒰 : AlgebraicGeometry.Scheme.OpenCover Y) [inst : ∀ (i : 𝒰.J), AlgebraicGeometry.IsAffine (AlgebraicGeometry.Scheme.OpenCover.obj 𝒰 i)] (i : 𝒰.J), CompactSpace ↑↑(CategoryTheory.Limits.pullback f (AlgebraicGeometry.Scheme.OpenCover.map 𝒰 i)).toLocallyRingedSpace.toSheafedSpace.toPresheafedSpace, ∀ {U : AlgebraicGeometry.Scheme} (g : U ⟶ Y) [inst : AlgebraicGeometry.IsAffine U] [inst : AlgebraicGeometry.IsOpenImmersion g], CompactSpace ↑↑(CategoryTheory.Limits.pullback f g).toLocallyRingedSpace.toSheafedSpace.toPresheafedSpace, ∃ ι U x x, ∀ (i : ι), CompactSpace ↑(↑f.val.base ⁻¹' (U i).carrier)]

theorem AlgebraicGeometry.QuasiCompact.is_local_at_target : AlgebraicGeometry.PropertyIsLocalAtTarget @AlgebraicGeometry.QuasiCompact

theorem AlgebraicGeometry.QuasiCompact.openCover_tfae {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) : List.TFAE [AlgebraicGeometry.QuasiCompact f, ∃ 𝒰, ∀ (i : 𝒰.J), AlgebraicGeometry.QuasiCompact CategoryTheory.Limits.pullback.snd, ∀ (𝒰 : AlgebraicGeometry.Scheme.OpenCover Y) (i : 𝒰.J), AlgebraicGeometry.QuasiCompact CategoryTheory.Limits.pullback.snd, ∀ (U : TopologicalSpace.Opens ↑↑Y.toPresheafedSpace), AlgebraicGeometry.QuasiCompact (f ∣_ U), ∀ {U : AlgebraicGeometry.Scheme} (g : U ⟶ Y) [inst : AlgebraicGeometry.IsOpenImmersion g], AlgebraicGeometry.QuasiCompact CategoryTheory.Limits.pullback.snd, ∃ ι U x, ∀ (i : ι), AlgebraicGeometry.QuasiCompact (f ∣_ U i)]

theorem AlgebraicGeometry.quasiCompact_over_affine_iff {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [AlgebraicGeometry.IsAffine Y] : AlgebraicGeometry.QuasiCompact f ↔ CompactSpace ↑↑X.toPresheafedSpace

theorem AlgebraicGeometry.compactSpace_iff_quasiCompact (X : AlgebraicGeometry.Scheme) : CompactSpace ↑↑X.toPresheafedSpace ↔ AlgebraicGeometry.QuasiCompact (CategoryTheory.Limits.terminal.from X)

theorem AlgebraicGeometry.QuasiCompact.affine_openCover_iff {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} (𝒰 : AlgebraicGeometry.Scheme.OpenCover Y) [∀ (i : 𝒰.J), AlgebraicGeometry.IsAffine (AlgebraicGeometry.Scheme.OpenCover.obj 𝒰 i)] (f : X ⟶ Y) : AlgebraicGeometry.QuasiCompact f ↔ ∀ (i : 𝒰.J), CompactSpace ↑↑(CategoryTheory.Limits.pullback f (AlgebraicGeometry.Scheme.OpenCover.map 𝒰 i)).toLocallyRingedSpace.toSheafedSpace.toPresheafedSpace

theorem AlgebraicGeometry.QuasiCompact.openCover_iff {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} (𝒰 : AlgebraicGeometry.Scheme.OpenCover Y) (f : X ⟶ Y) : AlgebraicGeometry.QuasiCompact f ↔ ∀ (i : 𝒰.J), AlgebraicGeometry.QuasiCompact CategoryTheory.Limits.pullback.snd

theorem AlgebraicGeometry.quasiCompact_respectsIso : CategoryTheory.MorphismProperty.RespectsIso @AlgebraicGeometry.QuasiCompact

theorem AlgebraicGeometry.quasiCompact_stableUnderComposition : CategoryTheory.MorphismProperty.StableUnderComposition @AlgebraicGeometry.QuasiCompact

theorem AlgebraicGeometry.QuasiCompact.affineProperty_stableUnderBaseChange : AlgebraicGeometry.AffineTargetMorphismProperty.StableUnderBaseChange AlgebraicGeometry.QuasiCompact.affineProperty

theorem AlgebraicGeometry.quasiCompact_stableUnderBaseChange : CategoryTheory.MorphismProperty.StableUnderBaseChange @AlgebraicGeometry.QuasiCompact

instance AlgebraicGeometry.instQuasiCompactPullbackSchemeInstCategorySchemeInstHasPullbackSchemeInstCategorySchemeFst {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} {Z : AlgebraicGeometry.Scheme} (f : X ⟶ Z) (g : Y ⟶ Z) [AlgebraicGeometry.QuasiCompact g] : AlgebraicGeometry.QuasiCompact CategoryTheory.Limits.pullback.fst

instance AlgebraicGeometry.instQuasiCompactPullbackSchemeInstCategorySchemeInstHasPullbackSchemeInstCategorySchemeSnd {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} {Z : AlgebraicGeometry.Scheme} (f : X ⟶ Z) (g : Y ⟶ Z) [AlgebraicGeometry.QuasiCompact f] : AlgebraicGeometry.QuasiCompact CategoryTheory.Limits.pullback.snd

theorem AlgebraicGeometry.compact_open_induction_on {X : AlgebraicGeometry.Scheme} {P : TopologicalSpace.Opens ↑↑X.toPresheafedSpace → Prop} (S : TopologicalSpace.Opens ↑↑X.toPresheafedSpace) (hS : IsCompact S.carrier) (h₁ : P ⊥) (h₂ : (S : TopologicalSpace.Opens ↑↑X.toPresheafedSpace) → IsCompact S.carrier → (U : ↑(AlgebraicGeometry.Scheme.affineOpens X)) → P S → P (S ⊔ ↑U)) : P S

theorem AlgebraicGeometry.exists_pow_mul_eq_zero_of_res_basicOpen_eq_zero_of_isAffineOpen (X : AlgebraicGeometry.Scheme) {U : TopologicalSpace.Opens ↑↑X.toPresheafedSpace} (hU : AlgebraicGeometry.IsAffineOpen U) (x : ↑(X.presheaf.obj (Opposite.op U))) (f : ↑(X.presheaf.obj (Opposite.op U))) (H : TopCat.Presheaf.restrictOpen x (AlgebraicGeometry.Scheme.basicOpen X f) = 0) : ∃ n, f ^ n * x = 0

theorem AlgebraicGeometry.exists_pow_mul_eq_zero_of_res_basicOpen_eq_zero_of_isCompact (X : AlgebraicGeometry.Scheme) {U : TopologicalSpace.Opens ↑↑X.toPresheafedSpace} (hU : IsCompact U.carrier) (x : ↑(X.presheaf.obj (Opposite.op U))) (f : ↑(X.presheaf.obj (Opposite.op U))) (H : TopCat.Presheaf.restrictOpen x (AlgebraicGeometry.Scheme.basicOpen X 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.