toBasicOpen — Mathlib

English

There is a canonical ring homomorphism from localization away f to the section ring on the basic open Spec.basicOpen f.

Русский

Существует канонический гомоморфизм из локализации away f в кольцо секций на базовом открытом множестве Spec.basicOpen f.

LaTeX

$$$toBasicOpen(R,f): Localization.Away f \\to (\\mathcal{O}_R) (\\operatorname{Spec}\\; \\text{basicOpen } f)$ is a ring homomorphism.$$

Lean4

/-- The canonical ring homomorphism interpreting `s ∈ R_f` as a section of the structure sheaf
on the basic open defined by `f ∈ R`. -/
def toBasicOpen (f : R) : Localization.Away f →+* (structureSheaf R).1.obj (op <| PrimeSpectrum.basicOpen f) :=
  IsLocalization.Away.lift f (isUnit_to_basicOpen_self R f)

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