English
A scheme X is compact if and only if there exist a ring R and a surjective morphism Spec R → X from some Spec of a ring.
Русский
Схема X компактна тогда и только тогда, когда существует кольцо R и сюръективный морфизм Spec R → X с виду Spec кольца.
LaTeX
$$$\\text{CompactSpace}(X) \\iff \\exists R,\\; \\exists f: \\Spec R \\to X,\\; \\text{Function.Surjective}(f^{\\mathrm{base}})$$$
Lean4
theorem compactSpace_iff_exists : CompactSpace X ↔ ∃ R, ∃ f : Spec R ⟶ X, Function.Surjective f.base :=
by
refine ⟨fun h ↦ ?_, fun ⟨R, f, hf⟩ ↦ ⟨hf.range_eq ▸ isCompact_range f.continuous⟩⟩
let 𝒰 : X.OpenCover := X.affineCover.finiteSubcover
refine ⟨Γ(∐ 𝒰.X, ⊤), (∐ 𝒰.X).isoSpec.inv ≫ Sigma.desc 𝒰.f, ?_⟩
refine Function.Surjective.comp (g := (Sigma.desc 𝒰.f).base) (fun x ↦ ?_) (∐ 𝒰.X).isoSpec.inv.surjective
obtain ⟨y, hy⟩ := 𝒰.covers x
exact ⟨(Sigma.ι 𝒰.X (𝒰.idx x)).base y, by rw [← Scheme.comp_base_apply, Sigma.ι_desc, hy]⟩
