germToFunctionField_injective — Mathlib

English

Let X be integral and U a nonempty open subset. The canonical map Γ(X,U) → k(X) given by germ at the generic point is injective.

Русский

Пусть X целый, U непустое открытое множество. Каноничный переход Γ(X,U) → k(X), задаваемый Germ в общем пункте, инъективен.

LaTeX

$$$\forall X\,[\operatorname{IsIntegral}(X)],\ U,\ (\text{Nonempty }U)\Rightarrow \operatorname{germToFunctionField}(X,U)\text{ is injective}.$$$

Lean4

theorem germToFunctionField_injective [IsIntegral X] (U : X.Opens) [Nonempty U] :
    Function.Injective (X.germToFunctionField U) :=
  germ_injective_of_isIntegral _ _ _

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