basicOpen_res_eq — Mathlib

English

Let X be a scheme and f ∈ Γ(X,U). Then membership x ∈ X.basicOpen f is equivalent to the germ of f at x being a unit in the local ring at x.

Русский

Пусть X — схема и f ∈ Γ(X,U). Тогда принадлежность точки x базовому открытому f эквивалентна тому, что герм f в x является единицей в локальном кольце в точке x.

LaTeX

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

Lean4

@[simp 1100]
theorem basicOpen_res_eq (i : op U ⟶ op V) [IsIso i] : X.basicOpen (X.presheaf.map i f) = X.basicOpen f :=
  RingedSpace.basicOpen_res_eq _ i f

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