instIsAffineXSchemeCoverOfIsIsoIsOpenImmersionId

English

For any affine X, the affine cover obtained from the iso-id construction by an open immersion consists of affine parts.

Русский

Для аффинной X аффинное покрытие, полученное из изоморфизма-идентичности через открытое вложение, состоит из аффинных частей.

LaTeX

$$$$ \forall X:\text{Affine }, (i:\text{(Scheme.coverOfIsIso (id X))}.I_0) \Rightarrow \mathrm{IsAffine}(((\text{Scheme.coverOfIsIso (id X)}).X) i). $$$$

Lean4

instance {X} [IsAffine X] (i) : IsAffine ((Scheme.coverOfIsIso (P := @IsOpenImmersion) (𝟙 X)).X i) := by dsimp;
  infer_instance

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