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)