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)
:
class
AlgebraicGeometry.QuasiCompact
{X : AlgebraicGeometry.Scheme}
{Y : AlgebraicGeometry.Scheme}
(f : X ⟶ Y)
:
- isCompact_preimage : ∀ (U : Set ↑↑Y.toPresheafedSpace), IsOpen U → IsCompact U → IsCompact (↑f.val.base ⁻¹' U)
Preimage of compact open set under a quasi-compact morphism between schemes is compact.
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.
Instances
theorem
AlgebraicGeometry.quasiCompact_iff_spectral
{X : AlgebraicGeometry.Scheme}
{Y : AlgebraicGeometry.Scheme}
(f : X ⟶ Y)
:
AlgebraicGeometry.QuasiCompact f ↔ IsSpectralMap ↑f.val.base
The AffineTargetMorphismProperty
corresponding to QuasiCompact
, asserting that the
domain is a quasi-compact scheme.
Instances For
instance
AlgebraicGeometry.quasiCompactOfIsIso
{X : AlgebraicGeometry.Scheme}
{Y : AlgebraicGeometry.Scheme}
(f : X ⟶ Y)
[CategoryTheory.IsIso f]
:
instance
AlgebraicGeometry.quasiCompactComp
{X : AlgebraicGeometry.Scheme}
{Y : AlgebraicGeometry.Scheme}
{Z : AlgebraicGeometry.Scheme}
(f : X ⟶ Y)
(g : Y ⟶ Z)
[AlgebraicGeometry.QuasiCompact f]
[AlgebraicGeometry.QuasiCompact g]
:
theorem
AlgebraicGeometry.isCompact_open_iff_eq_finset_affine_union
{X : AlgebraicGeometry.Scheme}
(U : Set ↑↑X.toPresheafedSpace)
:
IsCompact U ∧ IsOpen U ↔ ∃ s, Set.Finite s ∧ U = ⋃ (i : ↑(AlgebraicGeometry.Scheme.affineOpens X)) (_ : i ∈ s), ↑↑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.Finite s ∧ U = ⋃ (i : ↑(X.presheaf.obj (Opposite.op ⊤))) (_ : i ∈ s), ↑(AlgebraicGeometry.Scheme.basicOpen X i)
theorem
AlgebraicGeometry.quasiCompact_iff_forall_affine
{X : AlgebraicGeometry.Scheme}
{Y : AlgebraicGeometry.Scheme}
(f : X ⟶ Y)
:
AlgebraicGeometry.QuasiCompact f ↔ ∀ (U : TopologicalSpace.Opens ↑↑Y.toPresheafedSpace),
AlgebraicGeometry.IsAffineOpen U → IsCompact (↑f.val.base ⁻¹' ↑U)
@[simp]
theorem
AlgebraicGeometry.QuasiCompact.affineProperty_toProperty
{X : AlgebraicGeometry.Scheme}
{Y : AlgebraicGeometry.Scheme}
(f : X ⟶ Y)
:
theorem
AlgebraicGeometry.isCompact_basicOpen
(X : AlgebraicGeometry.Scheme)
{U : TopologicalSpace.Opens ↑↑X.toPresheafedSpace}
(hU : IsCompact ↑U)
(f : ↑(X.presheaf.obj (Opposite.op U)))
:
theorem
AlgebraicGeometry.QuasiCompact.affine_openCover_tfae
{X : AlgebraicGeometry.Scheme}
{Y : AlgebraicGeometry.Scheme}
(f : X ⟶ Y)
:
List.TFAE
[AlgebraicGeometry.QuasiCompact f,
∃ 𝒰 x,
∀ (i : 𝒰.J),
CompactSpace
↑↑(CategoryTheory.Limits.pullback f
(AlgebraicGeometry.Scheme.OpenCover.map 𝒰
i)).toLocallyRingedSpace.toSheafedSpace.toPresheafedSpace,
∀ (𝒰 : AlgebraicGeometry.Scheme.OpenCover Y)
[inst : ∀ (i : 𝒰.J), AlgebraicGeometry.IsAffine (AlgebraicGeometry.Scheme.OpenCover.obj 𝒰 i)] (i : 𝒰.J),
CompactSpace
↑↑(CategoryTheory.Limits.pullback f
(AlgebraicGeometry.Scheme.OpenCover.map 𝒰 i)).toLocallyRingedSpace.toSheafedSpace.toPresheafedSpace,
∀ {U : AlgebraicGeometry.Scheme} (g : U ⟶ Y) [inst : AlgebraicGeometry.IsAffine U]
[inst : AlgebraicGeometry.IsOpenImmersion g],
CompactSpace ↑↑(CategoryTheory.Limits.pullback f g).toLocallyRingedSpace.toSheafedSpace.toPresheafedSpace,
∃ ι U x x, ∀ (i : ι), CompactSpace ↑(↑f.val.base ⁻¹' (U i).carrier)]
theorem
AlgebraicGeometry.QuasiCompact.openCover_tfae
{X : AlgebraicGeometry.Scheme}
{Y : AlgebraicGeometry.Scheme}
(f : X ⟶ Y)
:
List.TFAE
[AlgebraicGeometry.QuasiCompact f,
∃ 𝒰, ∀ (i : 𝒰.J), AlgebraicGeometry.QuasiCompact CategoryTheory.Limits.pullback.snd,
∀ (𝒰 : AlgebraicGeometry.Scheme.OpenCover Y) (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,
∃ ι U x, ∀ (i : ι), AlgebraicGeometry.QuasiCompact (f ∣_ U i)]
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)
theorem
AlgebraicGeometry.QuasiCompact.affine_openCover_iff
{X : AlgebraicGeometry.Scheme}
{Y : AlgebraicGeometry.Scheme}
(𝒰 : AlgebraicGeometry.Scheme.OpenCover Y)
[∀ (i : 𝒰.J), AlgebraicGeometry.IsAffine (AlgebraicGeometry.Scheme.OpenCover.obj 𝒰 i)]
(f : X ⟶ Y)
:
AlgebraicGeometry.QuasiCompact f ↔ ∀ (i : 𝒰.J),
CompactSpace
↑↑(CategoryTheory.Limits.pullback f
(AlgebraicGeometry.Scheme.OpenCover.map 𝒰 i)).toLocallyRingedSpace.toSheafedSpace.toPresheafedSpace
theorem
AlgebraicGeometry.QuasiCompact.openCover_iff
{X : AlgebraicGeometry.Scheme}
{Y : AlgebraicGeometry.Scheme}
(𝒰 : AlgebraicGeometry.Scheme.OpenCover Y)
(f : X ⟶ Y)
:
AlgebraicGeometry.QuasiCompact f ↔ ∀ (i : 𝒰.J), AlgebraicGeometry.QuasiCompact CategoryTheory.Limits.pullback.snd
instance
AlgebraicGeometry.instQuasiCompactPullbackSchemeInstCategorySchemeInstHasPullbackSchemeInstCategorySchemeFst
{X : AlgebraicGeometry.Scheme}
{Y : AlgebraicGeometry.Scheme}
{Z : AlgebraicGeometry.Scheme}
(f : X ⟶ Z)
(g : Y ⟶ Z)
[AlgebraicGeometry.QuasiCompact g]
:
AlgebraicGeometry.QuasiCompact CategoryTheory.Limits.pullback.fst
instance
AlgebraicGeometry.instQuasiCompactPullbackSchemeInstCategorySchemeInstHasPullbackSchemeInstCategorySchemeSnd
{X : AlgebraicGeometry.Scheme}
{Y : AlgebraicGeometry.Scheme}
{Z : AlgebraicGeometry.Scheme}
(f : X ⟶ Z)
(g : Y ⟶ Z)
[AlgebraicGeometry.QuasiCompact f]
:
AlgebraicGeometry.QuasiCompact CategoryTheory.Limits.pullback.snd
theorem
AlgebraicGeometry.compact_open_induction_on
{X : AlgebraicGeometry.Scheme}
{P : TopologicalSpace.Opens ↑↑X.toPresheafedSpace → Prop}
(S : TopologicalSpace.Opens ↑↑X.toPresheafedSpace)
(hS : IsCompact S.carrier)
(h₁ : P ⊥)
(h₂ : (S : TopologicalSpace.Opens ↑↑X.toPresheafedSpace) →
IsCompact S.carrier → (U : ↑(AlgebraicGeometry.Scheme.affineOpens X)) → 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 : TopologicalSpace.Opens ↑↑X.toPresheafedSpace}
(hU : AlgebraicGeometry.IsAffineOpen U)
(x : ↑(X.presheaf.obj (Opposite.op U)))
(f : ↑(X.presheaf.obj (Opposite.op U)))
(H : TopCat.Presheaf.restrictOpen x (AlgebraicGeometry.Scheme.basicOpen X f) = 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 (Opposite.op U)))
(f : ↑(X.presheaf.obj (Opposite.op U)))
(H : TopCat.Presheaf.restrictOpen x (AlgebraicGeometry.Scheme.basicOpen X f) = 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
.