quasiCompact_iff_forall_affine — Mathlib

English

Quasi-compactness of a morphism is equivalent to a condition checked on all affine open subschemes of the target.

Русский

Квази-компактность морфизма эквивалентна условию, проверяемому на всех аффинных открытых под Scheme-мишени.

LaTeX

$$$QuasiCompact(f) \iff ∀U : Y.Opens, IsAffineOpen U \rightarrow IsCompact((f|_{f^{-1}(U)}) : X|_{U})$$$

Lean4

theorem quasiCompact_iff_forall_affine : QuasiCompact f ↔ ∀ U : Y.Opens, IsAffineOpen U → IsCompact (f ⁻¹ᵁ U : Set X) :=
  by
  rw [quasiCompact_iff]
  refine ⟨fun H U hU => H U U.isOpen hU.isCompact, ?_⟩
  intro H U hU hU'
  obtain ⟨S, hS, rfl⟩ := (isCompactOpen_iff_eq_finset_affine_union U).mp ⟨hU', hU⟩
  simp only [Set.preimage_iUnion]
  exact Set.Finite.isCompact_biUnion hS (fun i _ => H i i.prop)

Похожие утверждения