mem_basicOpen' — Mathlib

English

Let X be a scheme, U an open subset of X, and f a section over U. For a bundled point x of U, x lies in the basic open set defined by f precisely when the germ of f at x is a unit in the local ring at x.

Русский

Пусть X — схема, U — открытое подмножество X, и f — секция над U. Для объединённой точки x в U условие x ∈ X.basicOpen(f) эквивалентно тому, что его герм f_x является единицей в локальном кольце $\mathcal{O}_{X,x}$.

LaTeX

$$$\\uparrow x \\in X.basicOpen f \\iff \\operatorname{IsUnit}\\left( X.presheaf.germ U x x.2 f\\right)$$$

Lean4

/-- A variant of `mem_basicOpen` for bundled `x : U`. -/
@[simp]
theorem mem_basicOpen' (x : U) : ↑x ∈ X.basicOpen f ↔ IsUnit (X.presheaf.germ U x x.2 f) :=
  RingedSpace.mem_basicOpen _ _ _ _

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