ΓSpecIso

Mathlib.AlgebraicGeometry.Scheme

URI: https://scilib.ai/kg/mathlib#AlgebraicGeometry.Scheme.ΓSpecIso

English

There is a canonical isomorphism between the global sections of Spec R and R itself.

Русский

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

LaTeX

$$$ \Gamma(\mathrm{Spec} R, \top) \cong R. $$$

Lean4

/-- The global sections of `Spec R` is isomorphic to `R`. -/
def ΓSpecIso : Γ(Spec R, ⊤) ≅ R :=
  SpecΓIdentity.app R

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru