English
If P is local at the source and the scheme is quasi-compact, there exists a morphism from an affine scheme dominating X that satisfies P.
Русский
Если P локально относительно источника и схема является квазик-компактной, существует морфизм от аффинной схемы, задающий над X доминантность и удовлетворяющий P.
LaTeX
$$$\\exists Y\\;\\exists p: Y\\to X\\; (\\text{Surjective }p)\\wedge P(p)\\wedge IsAffine(Y)$$$
Lean4
/-- If `P` is local at the source, every quasi-compact scheme is dominated by an
affine scheme via `p : Y ⟶ X` such that `p` satisfies `P`.
-/
theorem exists_hom_isAffine_of_isZariskiLocalAtSource (X : Scheme.{u}) [CompactSpace X] [IsZariskiLocalAtSource P]
[P.ContainsIdentities] : ∃ (Y : Scheme.{u}) (p : Y ⟶ X), Surjective p ∧ P p ∧ IsAffine Y :=
by
let 𝒰 := X.affineCover.finiteSubcover
let p : ∐ (fun i : 𝒰.I₀ ↦ 𝒰.X i) ⟶ X := Sigma.desc (fun i ↦ 𝒰.f i)
refine ⟨_, p, ⟨fun x ↦ ?_⟩, ?_, inferInstance⟩
· obtain ⟨i, x, rfl⟩ := X.affineCover.finiteSubcover.exists_eq x
use (Sigma.ι (fun i ↦ X.affineCover.finiteSubcover.X i) i).base x
rw [← Scheme.comp_base_apply, Sigma.ι_desc]
· rw [IsZariskiLocalAtSource.iff_of_openCover (P := P) (sigmaOpenCover _)]
exact fun i ↦ by simpa [p] using IsZariskiLocalAtSource.of_isOpenImmersion _
