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

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) : IsOpen U → IsCompact U → IsCompact (⇑f ⁻¹' U)

  The preimage of a 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), IsOpen U → IsCompact U → IsCompact (⇑f ⁻¹' U)

theorem AlgebraicGeometry.quasiCompact_iff_isSpectralMap {X Y : Scheme} {f : X ⟶ Y} : QuasiCompact f ↔ IsSpectralMap ⇑f

theorem AlgebraicGeometry.Scheme.Hom.isSpectralMap {X Y : Scheme} (f : X ⟶ Y) [QuasiCompact f] : IsSpectralMap ⇑f

theorem AlgebraicGeometry.Scheme.Hom.isCompact_preimage {X Y : Scheme} (f : X ⟶ Y) [QuasiCompact f] {U : Y.Opens} (hU : IsCompact ↑U) : IsCompact ↑((TopologicalSpace.Opens.map f.base).obj U)

@[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.isCompact_and_isOpen_iff_finite_and_eq_biUnion_affineOpens {X : Scheme} {U : Set ↥X} : IsCompact U ∧ IsOpen U ↔ ∃ (s : Set ↑X.affineOpens), s.Finite ∧ U = ⋃ i ∈ s, ↑↑i

theorem AlgebraicGeometry.isCompact_iff_finite_and_eq_biUnion_affineOpens {X : Scheme} {U : X.Opens} : IsCompact ↑U ↔ ∃ (s : Set ↑X.affineOpens), s.Finite ∧ U = ⨆ i ∈ s, ↑i

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

theorem AlgebraicGeometry.quasiCompact_iff_forall_isAffineOpen {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_2 : IsAffine x) => CompactSpace ↥X

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

instance AlgebraicGeometry.instQuasiCompactToSpecΓOfCompactSpaceCarrierCarrierCommRingCat {X : Scheme} [CompactSpace ↥X] : QuasiCompact X.toSpecΓ

theorem AlgebraicGeometry.QuasiCompact.compactSpace_of_compactSpace {X Y : Scheme} (f : X ⟶ Y) [QuasiCompact f] [CompactSpace ↥Y] : CompactSpace ↥X

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

instance AlgebraicGeometry.instIsMultiplicativeSchemeQuasiCompact : CategoryTheory.MorphismProperty.IsMultiplicative @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)

instance AlgebraicGeometry.instQuasiCompactMorphismRestrict {X Y : Scheme} (f : X ⟶ Y) (V : Y.Opens) [QuasiCompact f] : QuasiCompact (f ∣_ V)

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

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

theorem AlgebraicGeometry.compactSpace_iff_exists {X : Scheme} : CompactSpace ↥X ↔ ∃ (R : CommRingCat) (f : Spec R ⟶ X), Function.Surjective ⇑f

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

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

Stacks Tag 01K9

theorem AlgebraicGeometry.compact_open_induction_on {X : Scheme} {P : X.Opens → Prop} (S : X.Opens) (hS : IsCompact ↑S) (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] (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_univ_iff_subset_nilradical_of_isCompact {X : Scheme} {U : X.Opens} (hU : IsCompact ↑U) (s : Set ↑(X.presheaf.obj (Opposite.op U))) : X.zeroLocus s = Set.univ ↔ 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_univ_iff_subset_nilradical {X : Scheme} [CompactSpace ↥X] (s : Set ↑(X.presheaf.obj (Opposite.op ⊤))) : X.zeroLocus s = Set.univ ↔ 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).