English
A quasicompact, locally closed subscheme of a quasi-affine scheme is itself quasi-affine.
Русский
Квазикомпактная локально открытая подпосхема квази-аффинной схемы сама по себе квази-аффинна.
LaTeX
$$$$\\text{If } Y \\text{ is quasi-affine and } X \\subseteq Y \\text{ is a quasicompact locally closed subscheme, then } X \\text{ is quasi-affine}.$$$$
Lean4
/-- Any quasicompact locally closed subscheme of an quasi-affine scheme is quasi-affine. -/
@[stacks 0BCK]
theorem of_isImmersion [Y.IsQuasiAffine] [IsImmersion f] [CompactSpace X] : X.IsQuasiAffine :=
by
wlog hY : IsAffine Y
· refine @this _ _ (f ≫ Y.toSpecΓ) ?_ ?_ _ ?_ <;> clear this <;> infer_instance
have : QuasiCompact f := by rwa [quasiCompact_over_affine_iff]
have : IsAffine f.image := HasAffineProperty.iff_of_isAffine.mp (inferInstanceAs (IsAffineHom f.imageι))
exact .of_isOpenImmersion f.toImage
