germ_injective_of_isIntegral — Mathlib

English

If X is integral, for any open U and x ∈ U the natural germ map from Γ(U, O_X) to the stalk O_{X,x} is injective.

Русский

Пусть X целый, U — открытое множество и x ∈ U. Тогда естественный герм-марков из Γ(U, O_X) в локальный стержень O_{X,x} инъективен.

LaTeX

$$$\forall U\subseteq X,\ x\in U:\; \text{If } [\operatorname{IsIntegral}(X)],\; s,t\in \Gamma(U,\mathcal{O}_X)\; (s|_x=t|_x)\Rightarrow s=t.$$$

Lean4

theorem germ_injective_of_isIntegral [IsIntegral X] {U : X.Opens} (x : X) (hx : x ∈ U) :
    Function.Injective (X.presheaf.germ U x hx) :=
  by
  rw [injective_iff_map_eq_zero]
  intro y hy
  rw [← (X.presheaf.germ U x hx).hom.map_zero] at hy
  obtain ⟨W, hW, iU, iV, e⟩ := X.presheaf.germ_eq _ hx hx _ _ hy
  cases Subsingleton.elim iU iV
  haveI : Nonempty W := ⟨⟨_, hW⟩⟩
  exact map_injective_of_isIntegral X iU e

Похожие утверждения