English
Let P be a property of opens of schemes. If P holds for any open cover, is stable under images of open immersions, and holds for the top space of every affine scheme Spec R, then P holds for all opens of all schemes.
Русский
Пусть P — свойство открытых подмножеств схем. Если P сохраняется при покрытии открытыми множествами и при образах открытых вложений и если P верно для всего пространства любой аффинной схемы Spec R, то P верно для любых открытов любой схемы.
LaTeX
$$$P \text{ удовлетворяет трем условиям (h₁, h₂, h₃):} \, (h₁) \, (h₂) \, (h₃) \Rightarrow \forall X, U, P(U)$$$
Lean4
/-- To show that a statement `P` holds for all open subsets of all schemes, it suffices to show that
1. In any scheme `X`, if `P` holds for an open cover of `U`, then `P` holds for `U`.
2. For an open immersion `f : X ⟶ Y`, if `P` holds for the entire space of `X`, then `P` holds for
the image of `f`.
3. `P` holds for the entire space of an affine scheme.
-/
@[elab_as_elim]
theorem reduce_to_affine_global (P : ∀ {X : Scheme} (_ : X.Opens), Prop) {X : Scheme} (U : X.Opens)
(h₁ : ∀ (X : Scheme) (U : X.Opens), (∀ x : U, ∃ (V : _) (_ : x.1 ∈ V) (_ : V ⟶ U), P V) → P U)
(h₂ :
∀ (X Y) (f : X ⟶ Y) [IsOpenImmersion f], ∃ (U : X.Opens) (V : Y.Opens), U = ⊤ ∧ V = f.opensRange ∧ (P U → P V))
(h₃ : ∀ R : CommRingCat, P (X := Spec R) ⊤) : P U :=
by
apply h₁
intro x
obtain ⟨_, ⟨j, rfl⟩, hx, i⟩ :=
X.affineBasisCover_is_basis.exists_subset_of_mem_open (SetLike.mem_coe.2 x.prop) U.isOpen
let U' : Opens _ := ⟨_, (X.affineBasisCover.map_prop j).base_open.isOpen_range⟩
let i' : U' ⟶ U := homOfLE i
refine ⟨U', hx, i', ?_⟩
obtain ⟨_, _, rfl, rfl, h₂'⟩ := h₂ _ _ (X.affineBasisCover.f j)
apply h₂'
apply h₃
