instIsAffine

Mathlib.AlgebraicGeometry.AffineSpace

URI: https://scilib.ai/kg/mathlib#AlgebraicGeometry.AffineSpace.instIsAffine

English

If S is affine, then the affine space 𝔸(n; S) is an affine scheme (i.e., IsAffine 𝔸(n; S)).

Русский

Если база S аффинна, то аффинное пространство 𝔸(n; S) является аффинной схемой (IsAffine 𝔸(n; S)).

LaTeX

$$$[IsAffine\\ S] \\Rightarrow IsAffine(\\mathbb{A}(n; S)).$$$

Lean4

instance [IsAffine S] : IsAffine 𝔸(n; S) :=
  .of_isIso (isoOfIsAffine n S).hom

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

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

Разделы

Аффилиация

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