Documentation

Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact

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 UIsCompact UIsCompact (f.val.base ⁻¹' U)

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 UIsCompact UIsCompact (f.val.base ⁻¹' U)

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

Instances
    theorem AlgebraicGeometry.QuasiCompact.isCompact_preimage {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} {f : X Y} [self : AlgebraicGeometry.QuasiCompact f] (U : Set Y.toPresheafedSpace) :
    IsOpen UIsCompact UIsCompact (f.val.base ⁻¹' U)

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

    The AffineTargetMorphismProperty corresponding to QuasiCompact, asserting that the domain is a quasi-compact scheme.

    Equations
    Instances For
      theorem AlgebraicGeometry.isCompact_open_iff_eq_finset_affine_union {X : AlgebraicGeometry.Scheme} (U : Set X.toPresheafedSpace) :
      IsCompact U IsOpen U ∃ (s : Set X.affineOpens), s.Finite U = is, 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 { unop := })), s.Finite U = is, (X.basicOpen i)
      theorem AlgebraicGeometry.isCompact_basicOpen (X : AlgebraicGeometry.Scheme) {U : TopologicalSpace.Opens X.toPresheafedSpace} (hU : IsCompact U) (f : (X.presheaf.obj { unop := U })) :
      IsCompact (X.basicOpen f)
      theorem AlgebraicGeometry.QuasiCompact.affine_openCover_tfae {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} (f : X Y) :
      [AlgebraicGeometry.QuasiCompact f, ∃ (𝒰 : Y.OpenCover) (_ : ∀ (i : 𝒰.J), AlgebraicGeometry.IsAffine (𝒰.obj i)), ∀ (i : 𝒰.J), CompactSpace (CategoryTheory.Limits.pullback f (𝒰.map i)).toPresheafedSpace, ∀ (𝒰 : Y.OpenCover) [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)].TFAE
      theorem AlgebraicGeometry.QuasiCompact.openCover_tfae {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} (f : X Y) :
      [AlgebraicGeometry.QuasiCompact f, ∃ (𝒰 : Y.OpenCover), ∀ (i : 𝒰.J), AlgebraicGeometry.QuasiCompact CategoryTheory.Limits.pullback.snd, ∀ (𝒰 : Y.OpenCover) (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)].TFAE
      theorem AlgebraicGeometry.QuasiCompact.affine_openCover_iff {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} (𝒰 : Y.OpenCover) [∀ (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} (𝒰 : Y.OpenCover) (f : X Y) :
      AlgebraicGeometry.QuasiCompact f ∀ (i : 𝒰.J), AlgebraicGeometry.QuasiCompact CategoryTheory.Limits.pullback.snd
      theorem AlgebraicGeometry.compact_open_induction_on {X : AlgebraicGeometry.Scheme} {P : TopologicalSpace.Opens X.toPresheafedSpaceProp} (S : TopologicalSpace.Opens X.toPresheafedSpace) (hS : IsCompact S.carrier) (h₁ : P ) (h₂ : ∀ (S : TopologicalSpace.Opens X.toPresheafedSpace), IsCompact S.carrier∀ (U : X.affineOpens), P SP (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 { unop := U })) (f : (X.presheaf.obj { unop := 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 { unop := U })) (f : (X.presheaf.obj { unop := 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.