toSpecΓ_of

Mathlib.AlgebraicGeometry.GammaSpecAdjunction

URI: https://scilib.ai/kg/mathlib#AlgebraicGeometry.ΓSpec.toSpecΓ_of

← MathLib Explorer

English

The isomorphism between SpecΓ of a ring and an open subset of Spec.

Русский

Изоморфизм между SpecΓ кольца и открытым подмножество Spect кольца.

LaTeX

$$$toSpecΓ( R ) = toOpen(R)$.$$

Lean4

/-- `@[simp]`-normal form of `locallyRingedSpaceAdjunction_counit_app'`. -/
@[simp]
theorem toSpecΓ_of (R : Type u) [CommRing R] : AlgebraicGeometry.toSpecΓ (CommRingCat.of R) = toOpen R ⊤ :=
  rfl

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

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

Разделы

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

Аффилиация

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