instIsAffineXSchemeAffineCover

Mathlib.AlgebraicGeometry.FunctionField

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

English

For any scheme X, each member of its affine open cover X.affineCover.X i is an affine scheme.

Русский

Для любой схемы X каждый элемент её афинного а покрытиа X.affineCover.X i является афинной схемой.

LaTeX

$$$\forall i,\; \operatorname{IsAffine}(X.affineCover.X i).$$$

Lean4

instance (x : X) : IsAffine (X.affineCover.X x) :=
  AlgebraicGeometry.isAffine_Spec _

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

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

Разделы

Аффилиация

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