ΓSpecIso_inv

Mathlib.AlgebraicGeometry.Scheme

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

English

The inverse of ΓSpecIso is StructureSheaf.toOpen R ⊤.

Русский

Обратное ΓSpecIso равно StructureSheaf.toOpen R ⊤.

LaTeX

$$$ (\GammaSpecIso R).\mathrm{inv} = \mathrm{StructureSheaf.toOpen} R \top. $$$

Lean4

theorem ΓSpecIso_inv : (ΓSpecIso R).inv = StructureSheaf.toOpen R ⊤ :=
  rfl

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

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

Разделы

Аффилиация

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