isAffineOpen_opensRange — Mathlib

English

If f is an open immersion from an affine X to Y, then the image opensRange f is affine.

Русский

Если f — открытое вложение от аффинного X в Y, то образ откр Range f — аффинный открытый.

LaTeX

$$$$ \mathrm{IsAffineOpen}(\mathrm{Scheme.Hom.opensRange}(f)). $$$$

Lean4

theorem isAffineOpen_opensRange {X Y : Scheme} [IsAffine X] (f : X ⟶ Y) [H : IsOpenImmersion f] :
    IsAffineOpen (Scheme.Hom.opensRange f) :=
  by
  refine .of_isIso (IsOpenImmersion.isoOfRangeEq f (Y.ofRestrict _) ?_).inv
  exact Subtype.range_val.symm

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