English
If X is integral, for open sets U ⊂ V with a nonempty U, the restriction map Γ(V, O_X) → Γ(U, O_X) is injective.
Русский
Если X целостна, то ограничение секций на открытых подмножествах с непустым U инъективно.
LaTeX
$$$\text{IsIntegral}(X) \Rightarrow \forall U \subseteq V, (\text{Nonempty } U) \Rightarrow \operatorname{Injective}(\Gamma(V, \mathcal{O}_X) \to \Gamma(U, \mathcal{O}_X))$$$
Lean4
theorem map_injective_of_isIntegral [IsIntegral X] {U V : X.Opens} (i : U ⟶ V) [H : Nonempty U] :
Function.Injective (X.presheaf.map i.op) :=
by
rw [injective_iff_map_eq_zero]
intro x hx
rw [← basicOpen_eq_bot_iff] at hx ⊢
rw [Scheme.basicOpen_res] at hx
revert hx
contrapose!
simp_rw [Ne, ← Opens.not_nonempty_iff_eq_bot, Classical.not_not]
apply nonempty_preirreducible_inter U.isOpen (RingedSpace.basicOpen _ _).isOpen
simpa using H
