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

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.

Instances

source

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)

source

theorem AlgebraicGeometry.quasiCompact_iff_spectral {X Y : Scheme} (f : X ⟶ Y) :

QuasiCompact f ↔ IsSpectralMap ⇑(CategoryTheory.ConcreteCategory.hom f.base)

source

@[instance 900]

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

QuasiCompact f

source

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

QuasiCompact (CategoryTheory.CategoryStruct.comp f g)

source

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

source

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)

source

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)

source

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

IsCompact ↑(X.basicOpen f)

source

instance AlgebraicGeometry.instHasAffinePropertyQuasiCompactCompactSpaceCarrierCarrierCommRingCat :

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

source

theorem AlgebraicGeometry.quasiCompact_over_affine_iff {X Y : Scheme} (f : X ⟶ Y) [IsAffine Y] :

QuasiCompact f ↔ CompactSpace ↑↑X.toPresheafedSpace

source

theorem AlgebraicGeometry.compactSpace_iff_quasiCompact (X : Scheme) :

CompactSpace ↑↑X.toPresheafedSpace ↔ QuasiCompact (CategoryTheory.Limits.terminal.from X)

source

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

CompactSpace ↑↑X.toPresheafedSpace

source

instance AlgebraicGeometry.quasiCompact_isStableUnderComposition :

CategoryTheory.MorphismProperty.IsStableUnderComposition @QuasiCompact

source

instance AlgebraicGeometry.quasiCompact_isStableUnderBaseChange :

CategoryTheory.MorphismProperty.IsStableUnderBaseChange @QuasiCompact

source

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

QuasiCompact (CategoryTheory.Limits.pullback.fst f g)

source

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

QuasiCompact (CategoryTheory.Limits.pullback.snd f g)

source

theorem AlgebraicGeometry.compactSpace_iff_exists {X : Scheme} :

CompactSpace ↑↑X.toPresheafedSpace ↔ ∃ (R : CommRingCat) (f : Spec R ⟶ X), Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom f.base)

source

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

source

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

source

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

source

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

source

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.

source

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.

source

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.

source

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

source

theorem AlgebraicGeometry.Scheme.zeroLocus_eq_univ_iff_subset_nilradical {X : Scheme} [CompactSpace ↑↑X.toPresheafedSpace] (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).

source

@[deprecated AlgebraicGeometry.Scheme.zeroLocus_eq_univ_iff_subset_nilradical_of_isCompact (since := "2025-04-05")]

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 = Set.univ ↔ s ⊆ ↑(nilradical ↑(X.presheaf.obj (Opposite.op U)))

Alias of AlgebraicGeometry.Scheme.zeroLocus_eq_univ_iff_subset_nilradical_of_isCompact.

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

source

@[deprecated AlgebraicGeometry.Scheme.zeroLocus_eq_univ_iff_subset_nilradical (since := "2025-04-05")]

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

X.zeroLocus s = Set.univ ↔ s ⊆ ↑(nilradical ↑(X.presheaf.obj (Opposite.op ⊤)))

Alias of AlgebraicGeometry.Scheme.zeroLocus_eq_univ_iff_subset_nilradical.

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

Documentation

Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact

Quasi-compact morphisms #