English
Given a diagram of rings with a finite-type map, there exists a larger open set V inside U and an induced lift of the diagram to Γ(X,V) that agrees on germs.
Русский
Для диаграммы колец с отображением конечного типа существует больший открытый множество V внутри U и соответствующий подъём диаграммы в Γ(X,V), совпадающий по герам.
LaTeX
$$$\exists V\; (\text{hxV})\; (\phi') \; (i) \; V \le U \; \land\; \operatorname{range}(\phi') \subseteq \ldots$$$
Lean4
theorem exists_le_and_germ_injective (X : Scheme.{u}) (x : X) [X.IsGermInjectiveAt x] (V : X.Opens) (hxV : x ∈ V) :
∃ (U : X.Opens) (hx : x ∈ U), IsAffineOpen U ∧ U ≤ V ∧ Function.Injective (X.presheaf.germ U x hx) :=
by
obtain ⟨U, hx, hU, H⟩ := Scheme.IsGermInjectiveAt.cond (x := x)
obtain ⟨f, hf, hxf⟩ := hU.exists_basicOpen_le ⟨x, hxV⟩ hx
exact ⟨X.basicOpen f, hxf, hU.basicOpen f, hf, injective_germ_basicOpen U hU x hx f hxf H⟩
