basicOpen_of_isUnit — Mathlib

English

Let X be a ringed space and U an open subset. If f is a unit in the ring of sections over U, then the basic open defined by f coincides with U; equivalently, D(f) = U.

Русский

Пусть X — кольцевое пространство, U — открытое подмножество. Пусть f — единица в кольце секций над U. Тогда базовая открытая, заданная f, совпадает с U; то есть D(f) = U.

LaTeX

$$$X$ is a ringed space, $U$ an open subset of $X$, and $f \in \mathcal{O}_X(U)^{\times}$. Then $X\text{.basicOpen}(f) = U$.$$

Lean4

theorem basicOpen_of_isUnit {U : Opens X} {f : X.presheaf.obj (op U)} (hf : IsUnit f) : X.basicOpen f = U :=
  by
  apply le_antisymm
  · exact X.basicOpen_le f
  intro x hx
  rw [SetLike.mem_coe, X.mem_basicOpen f x hx]
  exact RingHom.isUnit_map _ hf

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