English
For an open subset U of a scheme X, U is compact if and only if there exist a ring R and a morphism f: Spec R → X with range equal to U.
Русский
Для открытого подмножества U схемы X: U компактна тогда и только тогда существует кольцо R и морфизм f: Spec R → X, чье образующее множество совпадает с U.
LaTeX
$$$\\text{IsCompact}(U) \\iff \\exists R, \\exists f: \\Spec R \\to X,\\; \\operatorname{range} f^{\\mathrm{base}} = U$$$
Lean4
theorem isCompact_iff_exists {U : X.Opens} : IsCompact (U : Set X) ↔ ∃ R, ∃ f : Spec R ⟶ X, Set.range f.base = U :=
by
refine isCompact_iff_compactSpace.trans ((compactSpace_iff_exists (X := U)).trans ?_)
refine ⟨fun ⟨R, f, hf⟩ ↦ ⟨R, f ≫ U.ι, by simp [hf.range_comp]⟩, fun ⟨R, f, hf⟩ ↦ ?_⟩
refine ⟨R, IsOpenImmersion.lift U.ι f (by simp [hf]), ?_⟩
rw [← Set.range_eq_univ]
apply show Function.Injective (U.ι.base '' ·) from Set.image_val_injective
simp only [Set.image_univ, Scheme.Opens.range_ι]
rwa [← Set.range_comp, ← TopCat.coe_comp, ← Scheme.comp_base, IsOpenImmersion.lift_fac]
