isIso_toSpecΓ

Mathlib.AlgebraicGeometry.Spec

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

English

The same isomorphism statement as above holds for all R, i.e., toSpecΓ R is an isomorphism.

Русский

То же утверждение об изоморфизме: toSpecΓ R является изоморфизмом для всякого R.

LaTeX

$$$\operatorname{IsIso}(\mathrm{toSpec}\Gamma(R)).$$$

Lean4

instance isIso_toSpecΓ (R : CommRingCat.{u}) : IsIso (toSpecΓ R) := by cases R; apply StructureSheaf.isIso_to_global

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

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

Разделы

Аффилиация

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