isoSpec

Mathlib.AlgebraicGeometry.AffineScheme

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

← MathLib Explorer

English

For any affine scheme X, there is a canonical isomorphism X ≅ Spec(Γ(X)).

Русский

Для любой аффинной схемы X существует канонический изоморфизм X ≅ Spec(Γ(X)).

LaTeX

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

Lean4

/-- The canonical isomorphism `X ≅ Spec Γ(X)` for an affine scheme. -/
@[simps! -isSimp hom]
def isoSpec (X : Scheme) [IsAffine X] : X ≅ Spec Γ(X, ⊤) :=
  asIso X.toSpecΓ

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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