English
Given V ⊂ X and x ∈ V with x in some affine open U, there exists a basic open f ∈ Γ(X,U) such that X.basicOpen f ≤ V and x ∈ X.basicOpen f.
Русский
Существуют базовые открытые области f, удовлетворяющие включенности и содержат x.
LaTeX
$$$\exists f \in Γ(X,U)\; (X.basicOpen f \le V) \land (x \in X.basicOpen f)$$$
Lean4
theorem exists_basicOpen_le {V : X.Opens} (x : V) (h : ↑x ∈ U) :
∃ f : Γ(X, U), X.basicOpen f ≤ V ∧ ↑x ∈ X.basicOpen f :=
by
have : IsAffine _ := hU
obtain ⟨_, ⟨_, ⟨r, rfl⟩, rfl⟩, h₁, h₂⟩ :=
(isBasis_basicOpen U).exists_subset_of_mem_open (x.2 : (⟨x, h⟩ : U) ∈ _) ((Opens.map U.inclusion').obj V).isOpen
have :
U.ι ''ᵁ (U.toScheme.basicOpen r) = X.basicOpen (X.presheaf.map (eqToHom U.isOpenEmbedding_obj_top.symm).op r) :=
by
refine (Scheme.image_basicOpen U.ι r).trans ?_
rw [Scheme.basicOpen_res_eq]
simp only [Scheme.Opens.toScheme_presheaf_obj, Scheme.Opens.ι_appIso, Iso.refl_inv, CommRingCat.id_apply]
use X.presheaf.map (eqToHom U.isOpenEmbedding_obj_top.symm).op r
rw [← this]
exact ⟨Set.image_subset_iff.mpr h₂, ⟨_, h⟩, h₁, rfl⟩
