globalSectionsIso — Mathlib

English

There exists a canonical ring isomorphism between R and the global sections of the structure sheaf over the entire space.

Русский

Существует канонический изоморфизм колец между R и глобальными секциями 𝒪ₓ над всей пространством.

LaTeX

$$$\\text{globalSectionsIso} : \\mathrm{CommRing}~R \\cong \\Gamma(\\mathrm{Spec}(R), \\mathcal{O}_{\\mathrm{Spec}(R)})$$$

Lean4

/-- The ring isomorphism between the ring `R` and the global sections `Γ(X, 𝒪ₓ)`. -/
@[simps! inv]
def globalSectionsIso : CommRingCat.of R ≅ (structureSheaf R).1.obj (op ⊤) :=
  asIso (toOpen R ⊤)

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