English
If U and V are affine opens in X and x lies in U ∩ V, then there exist f ∈ Γ(X, U) and g ∈ Γ(X, V) such that X.basicOpen f = X.basicOpen g and x ∈ X.basicOpen f. This provides a common basic open around x.
Русский
Пусть U и V — аффинные открытые подмножества X, и пусть x ∈ U ∩ V. Тогда существуют f ∈ Γ(X, U) и g ∈ Γ(X, V) такие, что X.basicOpen f = X.basicOpen g и x ∈ X.basicOpen f. Это дает общее базовое открытое вокруг x.
LaTeX
$$$\forall V:\, X.Opens,\ h_V:\ IsAffineOpen V,\ \forall x:\, X,\ hx:\ x\in U\cap V,\ \exists f:\Gamma(X,U)\,\exists g:\Gamma(X,V),\ X.basicOpen f = X.basicOpen g\land x\in X.basicOpen f$$$
Lean4
theorem _root_.AlgebraicGeometry.exists_basicOpen_le_affine_inter {V : X.Opens} (hV : IsAffineOpen V) (x : X)
(hx : x ∈ U ⊓ V) : ∃ (f : Γ(X, U)) (g : Γ(X, V)), X.basicOpen f = X.basicOpen g ∧ x ∈ X.basicOpen f :=
by
obtain ⟨f, hf₁, hf₂⟩ := hU.exists_basicOpen_le ⟨x, hx.2⟩ hx.1
obtain ⟨g, hg₁, hg₂⟩ := hV.exists_basicOpen_le ⟨x, hf₂⟩ hx.2
obtain ⟨f', hf'⟩ := basicOpen_basicOpen_is_basicOpen hU f (X.presheaf.map (homOfLE hf₁ : _ ⟶ V).op g)
replace hf' := (hf'.trans (RingedSpace.basicOpen_res _ _ _)).trans (inf_eq_right.mpr hg₁)
exact ⟨f', g, hf', hf'.symm ▸ hg₂⟩
