isAffine_affineScheme

Mathlib.AlgebraicGeometry.AffineScheme

URI: https://scilib.ai/kg/mathlib#AlgebraicGeometry.isAffine_affineScheme

English

For any commutative ring R, Spec R is an affine scheme.

Русский

Для любых кольцевых колец R спектр Spec R является аффинной схемой.

LaTeX

$$$\\mathrm{IsAffine}(\\mathrm{Spec}(R))$$$

Lean4

instance isAffine_affineScheme (X : AffineScheme.{u}) : IsAffine X.obj :=
  ⟨Functor.essImage.unit_isIso X.property⟩

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

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

Разделы

Аффилиация

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