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

class AlgebraicGeometry.QuasiCompact {X Y : 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 (⇑(CategoryTheory.ConcreteCategory.hom f.base) ⁻¹' U)

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

theorem AlgebraicGeometry.quasiCompact_iff {X Y : Scheme} (f : X ⟶ Y) : QuasiCompact f ↔ ∀ (U : Set ↑↑Y.toPresheafedSpace), IsOpen U → IsCompact U → IsCompact (⇑(CategoryTheory.ConcreteCategory.hom f.base) ⁻¹' U)

theorem AlgebraicGeometry.quasiCompact_iff_spectral {X Y : Scheme} (f : X ⟶ Y) : QuasiCompact f ↔ IsSpectralMap ⇑(CategoryTheory.ConcreteCategory.hom f.base)

@[instance 900]

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

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

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

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

theorem AlgebraicGeometry.quasiCompact_iff_forall_affine {X Y : Scheme} (f : X ⟶ Y) : QuasiCompact f ↔ ∀ (U : Y.Opens), IsAffineOpen U → IsCompact ↑((TopologicalSpace.Opens.map f.base).obj U)

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

instance AlgebraicGeometry.instHasAffinePropertyQuasiCompactCompactSpaceCarrierCarrierCommRingCat : HasAffineProperty @QuasiCompact fun (X x : Scheme) (x_1 : X ⟶ x) (x : IsAffine x) => CompactSpace ↑↑X.toPresheafedSpace

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

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

instance AlgebraicGeometry.quasiCompact_isStableUnderComposition : CategoryTheory.MorphismProperty.IsStableUnderComposition @QuasiCompact

instance AlgebraicGeometry.quasiCompact_isStableUnderBaseChange : CategoryTheory.MorphismProperty.IsStableUnderBaseChange @QuasiCompact

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

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

theorem AlgebraicGeometry.compactSpace_iff_exists {X : Scheme} : CompactSpace ↑↑X.toPresheafedSpace ↔ ∃ (R : CommRingCat) (f : Spec R ⟶ X), Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom f.base)

theorem AlgebraicGeometry.isCompact_iff_exists {X : Scheme} {U : X.Opens} : IsCompact ↑U ↔ ∃ (R : CommRingCat) (f : Spec R ⟶ X), Set.range ⇑(CategoryTheory.ConcreteCategory.hom f.base) = ↑U

theorem AlgebraicGeometry.isClosedMap_iff_specializingMap {X Y : Scheme} (f : X ⟶ Y) [QuasiCompact f] : IsClosedMap ⇑(CategoryTheory.ConcreteCategory.hom f.base) ↔ SpecializingMap ⇑(CategoryTheory.ConcreteCategory.hom f.base)

Stacks Tag 01K9

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

theorem AlgebraicGeometry.exists_pow_mul_eq_zero_of_res_basicOpen_eq_zero_of_isAffineOpen (X : Scheme) {U : X.Opens} (hU : IsAffineOpen U) (x 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 : Scheme) {U : X.Opens} (hU : IsCompact U.carrier) (x 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.

theorem AlgebraicGeometry.Scheme.isNilpotent_iff_basicOpen_eq_bot_of_isCompact {X : Scheme} {U : X.Opens} (hU : IsCompact ↑U) (f : ↑(X.presheaf.obj (Opposite.op U))) : IsNilpotent f ↔ X.basicOpen f = ⊥

A section over a compact open of a scheme is nilpotent if and only if its associated basic open is empty.

theorem AlgebraicGeometry.Scheme.isNilpotent_iff_basicOpen_eq_bot {X : Scheme} [CompactSpace ↑↑X.toPresheafedSpace] (f : ↑(X.presheaf.obj (Opposite.op ⊤))) : IsNilpotent f ↔ X.basicOpen f = ⊥

A global section of a quasi-compact scheme is nilpotent if and only if its associated basic open is empty.

theorem AlgebraicGeometry.Scheme.zeroLocus_eq_top_iff_subset_nilradical_of_isCompact {X : Scheme} {U : X.Opens} (hU : IsCompact ↑U) (s : Set ↑(X.presheaf.obj (Opposite.op U))) : X.zeroLocus s = ⊤ ↔ s ⊆ ↑(nilradical ↑(X.presheaf.obj (Opposite.op U)))

The zero locus of a set of sections over a compact open of a scheme is X if and only if s is contained in the nilradical of Γ(X, U).

theorem AlgebraicGeometry.Scheme.zeroLocus_eq_top_iff_subset_nilradical {X : Scheme} [CompactSpace ↑↑X.toPresheafedSpace] (s : Set ↑(X.presheaf.obj (Opposite.op ⊤))) : X.zeroLocus s = ⊤ ↔ s ⊆ ↑(nilradical ↑(X.presheaf.obj (Opposite.op ⊤)))

The zero locus of a set of sections over a compact open of a scheme is X if and only if s is contained in the nilradical of Γ(X, U).