basicOpen — Mathlib

English

For any ring R, the basic open subset of Spec R is affine.

Русский

Для кольца R базовая открытая подзадача в Spec R является афинной схемой.

LaTeX

$$$\text{Spec}_{\text{basicOpen}}(R)$ is affine$$

Lean4

theorem basicOpen : IsAffineOpen (X.basicOpen f) :=
  by
  rw [← hU.fromSpec_image_basicOpen, Scheme.Hom.isAffineOpen_iff_of_isOpenImmersion]
  convert isAffineOpen_opensRange (Spec.map (CommRingCat.ofHom <| algebraMap Γ(X, U) (Localization.Away f)))
  exact Opens.ext (PrimeSpectrum.localization_away_comap_range (Localization.Away f) f).symm

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