isAffine_of_isAffineHom — Mathlib

English

If every basicOpen is affine and the span of sections covers the space, then the scheme is affine.

Русский

Если все базовые открытые являются аффинными и покрытия охватывают схему, то схема аффинна.

LaTeX

$$$isAffine_of_isAffineOpen_basicOpen$$

Lean4

theorem isAffine_of_isAffineHom [IsAffineHom f] [IsAffine Y] : IsAffine X :=
  (HasAffineProperty.iff_of_isAffine (P := @IsAffineHom) (f := f)).mp inferInstance

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