isAffine_affineCover — Mathlib

English

Each member of an affine open cover is affine.

Русский

Каждый компонент аффинного открытого покрытия является аффинной схемой.

LaTeX

$$$$ \forall X:\text{AlgebraicGeometry.Scheme},\forall i:\ X.\text{affineOpenCover}.I_0,\ \text{IsAffine}((X.\text{affineOpenCover}.X\,i)). $$$$

Lean4

instance isAffine_affineCover (X : Scheme) (i : X.affineCover.I₀) : IsAffine (X.affineCover.X i) :=
  isAffine_Spec _

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