isIso_to_global — Mathlib

English

The ring of global sections of the structure sheaf over the whole Spec(R) is canonically isomorphic to R.

Русский

Кольцо глобальных секций 𝒪_X над всем Spec(R) канонически изоморфно R.

LaTeX

$$$\\mathcal{O}_X(\\top) \\;\\cong\\; R$$$

Lean4

instance isIso_to_global : IsIso (toOpen R ⊤) :=
  by
  let hom := CommRingCat.ofHom (algebraMap R (Localization.Away (1 : R)))
  haveI : IsIso hom := (IsLocalization.atOne R (Localization.Away (1 : R))).toRingEquiv.toCommRingCatIso.isIso_hom
  rw [to_global_factors R]
  infer_instance

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