isoSpec_hom — Mathlib

English

For an affine open U in X, the forward morphism in the canonical isomorphism U ≅ Spec Γ(X, U) coincides with the canonical map U → Spec Γ(X, U) induced by global sections.

Русский

Для аффинного открытого множества U внутри X переходной морфизм в каноническом изоморфизме U ≅ Spec Γ(X, U) совпадает с каноническим отображением U → Spec Γ(X, U), полученным из глобальных секций.

LaTeX

$$hU.isoSpec.hom = U.toSpecΓ$$

Lean4

theorem isoSpec_hom : hU.isoSpec.hom = U.toSpecΓ :=
  rfl

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