mathlib3 documentation

algebraic_geometry.morphisms.quasi_compact

Quasi-compact morphisms #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

source
theorem algebraic_geometry.quasi_compact_iff {X Y : algebraic_geometry.Scheme} (f : X ⟶ Y) :
algebraic_geometry.quasi_compact f ↔ ∀ (U : set ↥(Y.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.carrier)), is_open U → is_compact U → is_compact (⇑(f.val.base) ⁻¹' U)
source
@[class]
structure algebraic_geometry.quasi_compact {X Y : algebraic_geometry.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.

Instances of this typeclass
source
theorem algebraic_geometry.quasi_compact_iff_spectral {X Y : algebraic_geometry.Scheme} (f : X ⟶ Y) :
algebraic_geometry.quasi_compact f ↔ is_spectral_map ⇑(f.val.base)
source
def algebraic_geometry.quasi_compact.affine_property  :
algebraic_geometry.affine_target_morphism_property

The affine_target_morphism_property corresponding to quasi_compact, asserting that the domain is a quasi-compact scheme.

Equations
source
@[protected, instance]
def algebraic_geometry.quasi_compact_of_is_iso {X Y : algebraic_geometry.Scheme} (f : X ⟶ Y) [category_theory.is_iso f] :
algebraic_geometry.quasi_compact f
source
@[protected, instance]
def algebraic_geometry.quasi_compact_comp {X Y Z : algebraic_geometry.Scheme} (f : X ⟶ Y) (g : Y ⟶ Z) [algebraic_geometry.quasi_compact f] [algebraic_geometry.quasi_compact g] :
algebraic_geometry.quasi_compact (f ≫ g)
source
theorem algebraic_geometry.is_compact_open_iff_eq_finset_affine_union {X : algebraic_geometry.Scheme} (U : set ↥(X.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.carrier)) :
is_compact U ∧ is_open U ↔ ∃ (s : set ↥(X.affine_opens)), s.finite ∧ U = ⋃ (i : ↥(X.affine_opens)) (h : i ∈ s), ↑i
source
theorem algebraic_geometry.is_compact_open_iff_eq_basic_open_union {X : algebraic_geometry.Scheme} [algebraic_geometry.is_affine X] (U : set ↥(X.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.carrier)) :
is_compact U ∧ is_open U ↔ ∃ (s : set ↥(X.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.presheaf.obj (opposite.op ⊤))), s.finite ∧ U = ⋃ (i : ↥(X.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.presheaf.obj (opposite.op ⊤))) (h : i ∈ s), ↑(X.basic_open i)
source
theorem algebraic_geometry.quasi_compact_iff_forall_affine {X Y : algebraic_geometry.Scheme} (f : X ⟶ Y) :
algebraic_geometry.quasi_compact f ↔ ∀ (U : topological_space.opens ↥(Y.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.carrier)), algebraic_geometry.is_affine_open U → is_compact (⇑(f.val.base) ⁻¹' ↑U)
source
@[simp]
theorem algebraic_geometry.quasi_compact.affine_property_to_property {X Y : algebraic_geometry.Scheme} (f : X ⟶ Y) :
algebraic_geometry.quasi_compact.affine_property.to_property f ↔ algebraic_geometry.is_affine Y ∧ compact_space ↥(X.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.carrier)
source
theorem algebraic_geometry.quasi_compact_iff_affine_property {X Y : algebraic_geometry.Scheme} (f : X ⟶ Y) :
algebraic_geometry.quasi_compact f ↔ algebraic_geometry.target_affine_locally algebraic_geometry.quasi_compact.affine_property f
source
theorem algebraic_geometry.quasi_compact_eq_affine_property  :
algebraic_geometry.quasi_compact = algebraic_geometry.target_affine_locally algebraic_geometry.quasi_compact.affine_property
source
theorem algebraic_geometry.is_compact_basic_open (X : algebraic_geometry.Scheme) {U : topological_space.opens ↥(X.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.carrier)} (hU : is_compact ↑U) (f : ↥(X.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.presheaf.obj (opposite.op U))) :
is_compact ↑(X.basic_open f)
source
theorem algebraic_geometry.quasi_compact.affine_property_is_local  :
algebraic_geometry.quasi_compact.affine_property.is_local
source
theorem algebraic_geometry.quasi_compact.affine_open_cover_tfae {X Y : algebraic_geometry.Scheme} (f : X ⟶ Y) :
[algebraic_geometry.quasi_compact f, ∃ (𝒰 : Y.open_cover) [_inst_1 : ∀ (i : 𝒰.J), algebraic_geometry.is_affine (𝒰.obj i)], ∀ (i : 𝒰.J), compact_space ↥((category_theory.limits.pullback f (𝒰.map i)).to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.carrier), ∀ (𝒰 : Y.open_cover) [_inst_2 : ∀ (i : 𝒰.J), algebraic_geometry.is_affine (𝒰.obj i)] (i : 𝒰.J), compact_space ↥((category_theory.limits.pullback f (𝒰.map i)).to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.carrier), ∀ {U : algebraic_geometry.Scheme} (g : U ⟶ Y) [_inst_3 : algebraic_geometry.is_affine U] [_inst_4 : algebraic_geometry.is_open_immersion g], compact_space ↥((category_theory.limits.pullback f g).to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.carrier), ∃ {ι : Type u} (U : ι → topological_space.opens ↥(Y.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.carrier)) (hU : supr U = ⊤) (hU' : ∀ (i : ι), algebraic_geometry.is_affine_open (U i)), ∀ (i : ι), compact_space ↥(⇑(f.val.base) ⁻¹' (U i).carrier)].tfae
source
theorem algebraic_geometry.quasi_compact.is_local_at_target  :
algebraic_geometry.property_is_local_at_target algebraic_geometry.quasi_compact
source
theorem algebraic_geometry.quasi_compact.open_cover_tfae {X Y : algebraic_geometry.Scheme} (f : X ⟶ Y) :
[algebraic_geometry.quasi_compact f, ∃ (𝒰 : Y.open_cover), ∀ (i : 𝒰.J), algebraic_geometry.quasi_compact category_theory.limits.pullback.snd, ∀ (𝒰 : Y.open_cover) (i : 𝒰.J), algebraic_geometry.quasi_compact category_theory.limits.pullback.snd, ∀ (U : topological_space.opens ↥(Y.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.carrier)), algebraic_geometry.quasi_compact (f ∣_ U), ∀ {U : algebraic_geometry.Scheme} (g : U ⟶ Y) [_inst_1 : algebraic_geometry.is_open_immersion g], algebraic_geometry.quasi_compact category_theory.limits.pullback.snd, ∃ {ι : Type u} (U : ι → topological_space.opens ↥(Y.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.carrier)) (hU : supr U = ⊤), ∀ (i : ι), algebraic_geometry.quasi_compact (f ∣_ U i)].tfae
source
theorem algebraic_geometry.quasi_compact_over_affine_iff {X Y : algebraic_geometry.Scheme} (f : X ⟶ Y) [algebraic_geometry.is_affine Y] :
algebraic_geometry.quasi_compact f ↔ compact_space ↥(X.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.carrier)
source
theorem algebraic_geometry.compact_space_iff_quasi_compact (X : algebraic_geometry.Scheme) :
compact_space ↥(X.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.carrier) ↔ algebraic_geometry.quasi_compact (category_theory.limits.terminal.from X)
source
theorem algebraic_geometry.quasi_compact.affine_open_cover_iff {X Y : algebraic_geometry.Scheme} (𝒰 : Y.open_cover) [∀ (i : 𝒰.J), algebraic_geometry.is_affine (𝒰.obj i)] (f : X ⟶ Y) :
algebraic_geometry.quasi_compact f ↔ ∀ (i : 𝒰.J), compact_space ↥((category_theory.limits.pullback f (𝒰.map i)).to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.carrier)
source
theorem algebraic_geometry.quasi_compact.open_cover_iff {X Y : algebraic_geometry.Scheme} (𝒰 : Y.open_cover) (f : X ⟶ Y) :
algebraic_geometry.quasi_compact f ↔ ∀ (i : 𝒰.J), algebraic_geometry.quasi_compact category_theory.limits.pullback.snd
source
theorem algebraic_geometry.quasi_compact_respects_iso  :
category_theory.morphism_property.respects_iso algebraic_geometry.quasi_compact
source
theorem algebraic_geometry.quasi_compact_stable_under_composition  :
category_theory.morphism_property.stable_under_composition algebraic_geometry.quasi_compact
source
theorem algebraic_geometry.quasi_compact.affine_property_stable_under_base_change  :
algebraic_geometry.quasi_compact.affine_property.stable_under_base_change
source
theorem algebraic_geometry.quasi_compact_stable_under_base_change  :
category_theory.morphism_property.stable_under_base_change algebraic_geometry.quasi_compact
source
@[protected, instance]
def algebraic_geometry.category_theory.limits.pullback.fst.quasi_compact {X Y Z : algebraic_geometry.Scheme} (f : X ⟶ Z) (g : Y ⟶ Z) [algebraic_geometry.quasi_compact g] :
algebraic_geometry.quasi_compact category_theory.limits.pullback.fst
source
@[protected, instance]
def algebraic_geometry.category_theory.limits.pullback.snd.quasi_compact {X Y Z : algebraic_geometry.Scheme} (f : X ⟶ Z) (g : Y ⟶ Z) [algebraic_geometry.quasi_compact f] :
algebraic_geometry.quasi_compact category_theory.limits.pullback.snd
source
theorem algebraic_geometry.compact_open_induction_on {X : algebraic_geometry.Scheme} {P : topological_space.opens ↥(X.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.carrier) → Prop} (S : topological_space.opens ↥(X.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.carrier)) (hS : is_compact S.carrier) (h₁ : P ⊥) (h₂ : ∀ (S : topological_space.opens ↥(X.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.carrier)), is_compact S.carrier → ∀ (U : ↥(X.affine_opens)), P S → P (S ⊔ ↑U)) :
P S
source
theorem algebraic_geometry.exists_pow_mul_eq_zero_of_res_basic_open_eq_zero_of_is_affine_open (X : algebraic_geometry.Scheme) {U : topological_space.opens ↥(X.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.carrier)} (hU : algebraic_geometry.is_affine_open U) (x f : ↥(X.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.presheaf.obj (opposite.op U))) (H : Top.presheaf.restrict_open x (X.basic_open f) _ = 0) :
∃ (n : ℕ), f ^ n * x = 0
source
theorem algebraic_geometry.exists_pow_mul_eq_zero_of_res_basic_open_eq_zero_of_is_compact (X : algebraic_geometry.Scheme) {U : topological_space.opens ↥(X.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.carrier)} (hU : is_compact U.carrier) (x f : ↥(X.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.presheaf.obj (opposite.op U))) (H : Top.presheaf.restrict_open x (X.basic_open 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.