to_basicOpen — Mathlib

English

On a basic open set basicOpen(r) in Spec(R), the ring of sections of the structure sheaf is the localization of R away from r.

Русский

На базовом открытом множества basicOpen(r) в Spec(R) кольцо секций 𝒪 над ним является локализацией кольца R away от r.

LaTeX

$$$\\mathcal{O}_{\\mathrm{Spec}\\,R}(\\mathrm{basicOpen}(r)) \\cong R_{\\{r\\}}$ (localization Away $r$)$$

Lean4

/-- Sections of the structure sheaf of Spec R on a basic open as localization of R -/
instance to_basicOpen (r : R) : IsLocalization.Away r ((structureSheaf R).val.obj (op <| PrimeSpectrum.basicOpen r)) :=
  by
  convert
    (IsLocalization.isLocalization_iff_of_ringEquiv (S := Localization.Away r) _
          (basicOpenIso R r).symm.commRingCatIsoToRingEquiv).mp
      Localization.isLocalization
  apply Algebra.algebra_ext
  intro x
  congr 1
  exact (localization_toBasicOpen R r).symm

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