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

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), IsOpen U → IsCompact U → IsCompact (⇑f.val.base ⁻¹' U)

  Preimage of compact open set under a quasi-compact morphism between schemes is 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.

Equations

• AlgebraicGeometry.QuasiCompact.affineProperty x✝ = CompactSpace ↑↑X.toPresheafedSpace

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

Equations

• ⋯ = ⋯

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)

Equations

• ⋯ = ⋯

theorem AlgebraicGeometry.isCompact_open_iff_eq_finset_affine_union {X : AlgebraicGeometry.Scheme} (U : Set ↑↑X.toPresheafedSpace) : IsCompact U ∧ IsOpen U ↔ ∃ (s : Set ↑(AlgebraicGeometry.Scheme.affineOpens X)), Set.Finite s ∧ U = ⋃ 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 ↑(X.presheaf.obj (Opposite.op ⊤))), Set.Finite s ∧ U = ⋃ i ∈ s, ↑(X.basicOpen 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 ↑(X.basicOpen 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, ∃ (𝒰 : AlgebraicGeometry.Scheme.OpenCover Y) (_ : ∀ (i : 𝒰.J), AlgebraicGeometry.IsAffine (𝒰.obj i)), ∀ (i : 𝒰.J), CompactSpace ↑↑(CategoryTheory.Limits.pullback f (𝒰.map i)).toPresheafedSpace, ∀ (𝒰 : AlgebraicGeometry.Scheme.OpenCover Y) [inst : ∀ (i : 𝒰.J), AlgebraicGeometry.IsAffine (𝒰.obj i)] (i : 𝒰.J), CompactSpace ↑↑(CategoryTheory.Limits.pullback f (𝒰.map i)).toPresheafedSpace, ∀ {U : AlgebraicGeometry.Scheme} (g : U ⟶ Y) [inst : AlgebraicGeometry.IsAffine U] [inst : AlgebraicGeometry.IsOpenImmersion g], CompactSpace ↑↑(CategoryTheory.Limits.pullback f g).toPresheafedSpace, ∃ (ι : Type u) (U : ι → TopologicalSpace.Opens ↑↑Y.toPresheafedSpace) (_ : iSup U = ⊤) (_ : ∀ (i : ι), AlgebraicGeometry.IsAffineOpen (U i)), ∀ (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, ∃ (𝒰 : AlgebraicGeometry.Scheme.OpenCover Y), ∀ (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, ∃ (ι : Type u) (U : ι → TopologicalSpace.Opens ↑↑Y.toPresheafedSpace) (_ : iSup U = ⊤), ∀ (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 (𝒰.obj i)] (f : X ⟶ Y) : AlgebraicGeometry.QuasiCompact f ↔ ∀ (i : 𝒰.J), CompactSpace ↑↑(CategoryTheory.Limits.pullback f (𝒰.map i)).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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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 (X.basicOpen 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 (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.