English
Let X be a scheme and U an affine open subset of X. For any section g on the basic open X.basicOpen f (with f ∈ Γ(X, U)), there exists a section f′ on U such that the basic open defined by f′ on X coincides with the basic open defined by g on X.
Русский
Пусть X — схема, U — аффинное открытое подмножество X. Для любой секции g на открытом базисе X.basicOpen f (где f ∈ Γ(X, U)) существует секция f′ на U такая, что X.basicOpen f′ = X.basicOpen g.
LaTeX
$$$\forall g\in Γ(X, X.basicOpen f),\ \exists f'\in Γ(X, U): X.basicOpen f' = X.basicOpen g$$$
Lean4
theorem basicOpen_basicOpen_is_basicOpen (g : Γ(X, X.basicOpen f)) : ∃ f' : Γ(X, U), X.basicOpen f' = X.basicOpen g :=
by
have := isLocalization_basicOpen hU f
obtain ⟨x, ⟨_, n, rfl⟩, rfl⟩ := IsLocalization.surj'' (Submonoid.powers f) g
use f * x
rw [Algebra.smul_def, Scheme.basicOpen_mul, Scheme.basicOpen_mul, RingHom.algebraMap_toAlgebra, Scheme.basicOpen_res]
refine (inf_eq_left.mpr (inf_le_left.trans_eq (Scheme.basicOpen_of_isUnit _ ?_).symm)).symm
exact Submonoid.leftInv_le_isUnit _ (IsLocalization.toInvSubmonoid (Submonoid.powers f) (Γ(X, X.basicOpen f)) _).prop
