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 : 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.base ⁻¹' U)

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

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.base ⁻¹' U)

theorem AlgebraicGeometry.QuasiCompact.isCompact_preimage {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} {f : X ⟶ Y} [self : AlgebraicGeometry.QuasiCompact f] (U : Set ↑↑Y.toPresheafedSpace) : IsOpen U → IsCompact U → IsCompact (⇑f.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.base

@[instance 900]

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

Equations

• ⋯ = ⋯

instance AlgebraicGeometry.quasiCompact_comp {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.isCompactOpen_iff_eq_finset_affine_union {X : AlgebraicGeometry.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 : AlgebraicGeometry.Scheme} [AlgebraicGeometry.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 : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) : AlgebraicGeometry.QuasiCompact f ↔ ∀ (U : Y.Opens), AlgebraicGeometry.IsAffineOpen U → IsCompact ↑((TopologicalSpace.Opens.map f.base).obj U)

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

@[reducible]

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

Equations

• AlgebraicGeometry.instHasAffinePropertyQuasiCompactCompactSpaceαTopologicalSpaceCarrierCommRingCat = ⋯

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)

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

Equations

• AlgebraicGeometry.quasiCompact_isStableUnderComposition = ⋯

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

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

theorem AlgebraicGeometry.compact_open_induction_on {X : AlgebraicGeometry.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 : AlgebraicGeometry.Scheme) {U : X.Opens} (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 : X.Opens} (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.

theorem AlgebraicGeometry.Scheme.isNilpotent_iff_basicOpen_eq_bot_of_isCompact {X : AlgebraicGeometry.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 : AlgebraicGeometry.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 : AlgebraicGeometry.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 : AlgebraicGeometry.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).