stalkFunctionFieldAlgebra — Mathlib

English

Let X be integral and U a nonempty open. The map Γ(X,U) → k(X) is injective.

Русский

Пусть X целый, U непустое открытое. Отображение Γ(X,U) → k(X) инъективно.

LaTeX

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

Lean4

noncomputable instance stalkFunctionFieldAlgebra [IrreducibleSpace X] (x : X) :
    Algebra (X.presheaf.stalk x) X.functionField := by
  -- TODO: can we write this normally after the refactor finishes?

  apply RingHom.toAlgebra
  exact (X.presheaf.stalkSpecializes ((genericPoint_spec X).specializes trivial)).hom

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